Lambda the Ultimate

Ola Bini, a core JRuby developer and author of the book Practical JRuby on Rails Projects, has been developing a new language for the JVM called Ioke. This strongly typed, extremely dynamic, prototype based object oriented language aims to give developers the same kind of power they get with Lisp and Ruby, combined with a nice, small, regular syntax.

InfoQ has a Q&A with Ola about Ioke.

Hey, while tutoring a student for a University of Toronto course, I was linked to a paper on Burst Tries. (A mirror is available here)

They're basically the same as tries except that they use containers to store keys/values before creating branches. When the containers are full, they "burst" and are turned into branches. The point of this is that a more efficient data structure for small sets of keys/values can be used in the container, making it faster than a traditional trie.

The paper is by Steffen Heinz, Justin Zobel, and Hugh E. Williams of RMIT University (Australian university it looks like). They have included benchmarks in the paper along with descriptions of alternatives (binary trees, splay trees, hash tables) with the burst trie being discussed beginning at page 5. The benchmarks/experiments are page 13 and on.

The process of programming language creation is a subject of too little reflection and retrospection. Newcomers to the field (including, in some measure, us) regularly propose new languages without quite understanding what they are getting into or how big the task is.
... This paper describes the motivation and early design evolution of the BitC programming language, making our excuses in hindsight and providing a compilation of some of the things that we learned along the way.
... The ML module system [18] is fully understood only by David MacQueen, and only on alternating weeks. The Scheme module system [8] required the combined brilliance of Matt Flatt and Matthias Felleisen (and six revisions of the language standard) to achieve. From the perspective of a mere operating systems weenie, it's all rather discouraging, but what is the reluctant programming language designer to do?
... The real reason we stuck with the LISP-ish syntax is that we didn't want to be fiddling with the parser while designing the language, and (to a lesser degree) because we didn't want to encourage programmers until we thought the language was ready.

The Origins of the BitC Programming Language Warning: Work in Progress

I was just struck with a minor revelation. The informal explanation for α-equivalence in λ-calculus is that a function "does the same thing" regardless of the particular names that we might choose for its internal variables. But this seems like just a particular case of the general extensionality principle!

Technically, α-conversion means that a bound variable may be renamed to another one as long as no free variables are captured:

    y ∉ FV(e)
―――――――――――――――――― (α)
λx. e = λy. e[y/x]

And indeed, it turns out that in the presence of the η-rule, which expresses the extensionality principle, the above rule is derivable:

y ∉ FV(e)
―――――――――――――       ―――――――――――――――――― (β)
y ∉ FV(λx. e)       (λx. e) y = e[y/x]
――――――――――――― (η)   ―――――――――――――――――― (ξ)
λx. e  =  λy. (λx. e) y  =  λy. e[y/x]

This is of course quite trivial. However, I've read a fair number of tutorials to λ-calculus, and I don't recall having ever seen this particular tidbit mentioned anywhere. I'm unsure whether this is because I just haven't read the right papers, or the matter is so trivial that no one bothers mentioning it explicitly, or there's something wrong with my reasoning.

So, just to ease my mind, could someone please either direct me to some respectable source where the redundancy of α in the presence of η is confirmed, or else point out what I'm missing here?

Thanks.

It seems to me that Haskell imitates subtyping for numeric types by implicitly passing number literals to the coercion functions fromInteger or fromRational. Is it possible to give subtyping and overloading a more elegant/complete way to coexist?

If, for example, the literal "1" has type int, what needs to be added to an ML-like type system so that "1 + 0.3" will be typed as a float?

Thanks,
Alex