Lambda the Ultimate

Programing Languiges like: ruby, (lisp/scheme), smalltalk, dylan, ect.; do not limit your expressivenes by removing features like Dynamic Typeing, Lambda, Higher Order Functions. whereas languiges digsinged for DOLTS like: Java; artifisaly limit your expressivenes by Weak Static Typeing System, Lack of lambda, lack of ability to pass in functions. As programing languiges inch towrds lisp, the Abstraction ceeling of an avreage languige gets higher and higher.

Like math puzzles and physics puzzles, there are many different kinds of programming puzzles. One way to classify programming puzzles is by the skills they exercise or the concepts they illustrate: knowledge of a language, designing a new algorithm, understanding a specification, etc.

On LtU, I'm interested in puzzles that are not specific to a language yet rely on a PL notion. Here's one attempt of mine, inspired by my student Jun Dai:

Your stair-climbing robot has a very simple low-level API: the "step" function takes no argument and attempts to climb one step as a side effect. Unfortunately, sometimes the attempt fails and the robot clumsily falls one step instead. The "step" function detects what happens and returns a boolean flag: true on success, false on failure. Write a function "step_up" that climbs one step up (by repeating "step" attempts if necessary). Assume that the robot is not already at the top of the stairs, and neither does it ever reach the bottom of the stairs. How small can you make "step_up"? Can you avoid using variables (even immutable ones) and numbers?

What do you think? What is your solution? How are the solutions related to each other? (If "step" fails with a fixed probability, then how many times does "step_up" expect to call "step"?)

More importantly, what is your favorite PL puzzle that is not (terribly) language-specific?

"... As the Erlang DCC is less than a quarter of the size of a similar C++/CORBA implementation, the product development in Erlang should be fast, and the code maintainable. We conclude that Erlang and associated libraries are suitable for the rapid development of maintainable and highly reliable distributed products."

Are High-level Languages suitable for Robust Telecoms Software? (pdf) also High-Level Techniques for Distributed Telecommunications Software

It would be of great interest to me to learn how to write a good paper for introducing a programming language formally (or at least semi-formally) which would be acceptable for publication in a reputable journal. Are there any tutorials, or good examples anyone can recommend I should follow as a template?

I also wonder if it is expected that every new programming language paper be accompanied by a proof of the soundness/unsoundness of the type system, or if I can by leaving that for another time (and perhaps another more capable person)?

Just introducing the basic semantics of the language with some rigour is in of itself a pretty signficiant challenge, considering that I have to resort to some pretty heavy techniques (for me at least) to describe the Cat type system (e.g. kind systems, parameteric polymorphism).

Hi y'all!

I have a language that I've been working on for a while that I intend to be lazy. At this point, the "flavor" of the language is pretty much set, but I'm still working out some of lower-level details, and I'm wondering about the implementation of laziness. Strict-evaluation is certainly easy to implement, since one never bothers to create thunks, but for non-strict evaluation, is there any literature on the practical elements that go into choosing how frequently to turn thunks into values? Do most implementations wait until they hit conditional forms or IO, or do they tend to put upper-bounds on how large a chain of thunks can get, or ... ?

thanks!

JimDesu

From this article:

A dominant theme of the past 50 years has been the growing understanding of how to create computer programs for specific tasks. A central theme of the next 50 will be the systematic exploration of the "computational universe" of all possible programs.

In recent years we have discovered that very small programs can produce immensely rich and complex behaviour. As we explore the computational universe this fact will become crucial to science, art, technology and our whole way of thinking. Today when we create things, we expect to do it by explicit human effort. Fifty years from now, it will more often be done by automatically mining the computational universe. Perhaps we will even find the ultimate model of our universe that way. No doubt many industries will be created from technology discovered in the computational universe - whether for programmable nanostructures, algorithmic drugs, mass-customised art or generative microeconomics.

Just as scientific concepts such as momentum and natural selection are commonplace in our thinking today, so in 50 years will be concepts like computational irreducibility and the principle of computational equivalence. I expect the children of 50 years from now will learn cellular automata before they learn algebra.

J. Grundy, T. Melham, and J. O'Leary, A reflective functional language for hardware design and theorem proving, Journal of Functional Programming, 16(2):157-196, March 2006.

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself.

reFLect is apparently a follow-on to the earlier FL language (which I asked about in an earlier thread), the language used in Intel's Forte hardware verification environment. Within Forte, reFLect can be used to perform a seamless mix of theorem proving and model-checking (invocation of a model-checker is just a reFLect function call, with the source text of any call to the model-checker that returns true becoming a theorem of the logic). Tom Melham's reFLect page has a little more information, and also points out that a Linux version of the Forte system, including an implementation of reFLect, is freely downloadable from Intel.

note: thanks to Ehud's grace (or lack of good judgement, depending on your viewpoint) I have been granted powers of editor ;-) Please feel free to offer me suggestions in private or in public on how I can better address the needs of community in what I choose to post or write. I hope the contributions of a neophyte can still be appreciated.

- Christopher (cdiggins@gmail.com )

For my first post as editor I thought I'd bring up an observation of mine while perusing the literature. of what appears to be a lack of usage of the typed SK calculus in theoretical papers. In my studies I am very surprised it hasn't come up more often, since it is elegant, and easy to understand.

I encountered the typed SK calculus first in Laufer and Odersky 1993. A web search for the phrase "typed SK calculus" yielded a brief usage on the Haskell Wiki in a discussion on Generalized Data Types.

I first encountered the SK calculus without types when reading Brent Kerby's A Theory of Concatenative Combinators which is an informal examination of combinators in Joy.

As a referesher, the typed SK calculus is made up of only two operations S and K:

  K : a -> b -> a
  S : (a -> b -> c) -> (a -> b) -> a -> c

So the questions I am pondering are: why is the lambda calculus so much more popular? Is it because Scheme and other similar languages more closely resemble the lambda calculus? If there was a language based on the SK calculus, would it become more popular? I also wonder what applications there are for the SK calculus, and what place it should occupy in my programming language theory arsenal?

New paper by Hongwei Xi and others, Distributed Meta-Programming. Also contrasts the presented approach with that of Alice:

Distributed meta-programming (DMP), which allows code to be generated and distributed at run-time, has already become a common practice. However, code generation currently often relies on rather ad hoc approaches that represent code as plain text. making DMP notoriously error-prone. This unfortunate situation is further exacerbated due to issues such as mobility (of code) and locality and heterogeneity (of resources), which complicate testing and debugging drastically.

In this paper, we study distributed meta-programming from a type-theoretic perspective, presenting a language to facilitate the construction of programs that may generate and distribute code at run-time. The approach we take makes use of a form of typeful code representation developed in a previous study on metaprogramming, and it guarantees statically that only well-typed code (according to some chosen type discipline) can be constructed at run-time and sent to proper locations for execution. We also mention a prototype implementation in support of the practicality of our approach to DMP, providing a solid proof of concept.

EMPL: Small APL for the Intel 8080

It fits in 5808 bytes. ... Today, you can use a C 8080 simulator to run the EMPL code after first converting it from hex to binary

I guess we should look forward to the completion of Python for Toddlers :-)