Implementations of untyped lazy lambda calculus

I am trying to create a very efficient implentation of John Tromp's binary lambda calculus so that it can be used as a toy language at It is the pure untyped lambda calculus with only 3 types of operations, lambda abstraction, variable (argument) lookup, and apply.

I figure the easiest way to do this is just to convert it into some other language. I only have basic knowledge of some functional languages, I would not mind learning more, but only if it is actually possible to convert the untyped lambda calculus into it.

Haskell is lazy but since it is not dynamically typed it runs into problems with "cannot construct the infinite type"

Ocaml might be able to get around this problem with the -rectypes but lazyness must be done manually with lazy and Lazy.force. Even if it could work, Ocaml's lazy functions might not be very efficient at all.

Another option is to convert into the spineless tagless gmachine notation that Haskell uses. Alot of the Haskell optimizations are done before this step.

Can any of these problems be overcome without too much cost? Or any other good languages out there that could? Any advice is appreciated, but you do not need to explain the whole thing in detail, a pointer to the right direction will be of enough help.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Why do you need recursive

Why do you need recursive types? Maybe it would be more useful to use one of the already well-documented state transition machines such as TIM, G-Machine, and STG

Types don't get in the way

Haskell may be typed but you can still reflect the lazyness into an interpreter for untyped lambda calculus:
 data Un =
    Var Un
  | Lam (Un -> Un)
  | App Un Un
 eval (Var v) = Var v
 eval (Lam b) = Lam b
 eval (App m n) = eval m * n
  where Lam b * n = eval (b n)
        m * n = App m n
I am not sure how this compares in efficiency to SAPL, STG, supercombinators or any of the other methods though. (see also shortest beta-normalizer)

Recursive types are needed

Recursive types are needed because the untyped type is really U->U, where U is the untyped type. An example of something that causes a problem is (\x.x x).

I'll try the code based on the shortest beta-normalizer and test its efficiency. I think it is similar to what Tromp used in his interpreter, which was not that fast, but maybe the compiler can make it efficient. Might take me a while to post results, I am a Haskell newbie.

Thanks both for your advice, if it isn't fast I'll try a lower level machine next.

Recursive types are needed

Recursive types are needed because the untyped type is really U->U, where U is the untyped type.

Why does this cause a problem? It's not as if you're about to typecheck it.

Well, my initial approach

Well, my initial approach was to convert the expressions directly into Haskell, resulting in it being typed checked.


Do you understand the post by Vicky? Just to be sure...

I think there used to be a hack in the type-system of Haskell you could exploit to get a universal (or rather: your infinite) type, I'll think it over again.

Not yet

I do not fully understand it yet, I am going ahead with learning Haskell and then I will I think.

Is this the kind of hack you were talking about? It was for church list and not just arbitrary expressions, although perhaps it could be made to work for those too. Again I need to learn Haskell first to really understand it.

Sorry, I forgot

Forgot, I posted an example to the Haskell list in, I think, 1999/2000. But I forgot, and I also forgot the pseudonym I used then (I use many).

I think it had something to do with using a recursive data type to derive a combinator or type which would be self-referential, but I am not sure... (And maybe I got it wrong anyway...).

[I guess it was the same trick as Phillipa is refering to.]

Separate syntax and semantics

The universal type only denotes U = U->U, you can implement it just working with the AST for terms and an evaluator. Once you've got that, you can then pull one of my pet favourite tricks and 'fuse' the AST itself away if you want to, but life is much saner with it still around.

PLT Scheme and its Lazy

PLT Scheme and its Lazy Scheme module.

Sorry it took so long

After learning some Haskell I made an interpreter based on the shortest beta normalizer that vicky posted. But instead of converting it back into an AST I convert it directly to the output string. I benchmarked it using the prime number printer from lazy k, s, k, and i are just defined as lambda expressions at the top then rest of code can be used as is. To print out the first 3000 characters it took 64 seconds, much faster than I thought it would be, whereas with the lazy-k interpreter it takes 42 seconds. This is plenty fast since the lazy-k interpreter is really efficient. Normally I would run a size optimizer on the source first (since it is for golf after all), that took the time down to 30 seconds (it just looks to make applications that result in shorter code).

Thanks for your help and patience. I should have a web page up soon with a tutorial and tools for golfing. Although nothing new and interesting about the language (it is just a rip off of Tromp's), mainly a toy for learning functional programming which it seems everyone here already knows :)

John Smith: Hmm sounds like a good idea, I'll stick with the Haskell method for now though.

Philippa Cowderoy: Is your method of fusing the AST away just like using the eval function (from the shortest beta normalizer) on it?

Edit: If instead of interpreting the source, converting it to Haskell and letting the compiler work its magic, resulted in 4 second runtime (16 seconds for non size optimized version). This is even better, but I would have thought it would be just as fast for non size optimized version, I guess ghc doesn't look for those types of optimizations.

Edit#2: Actually the standard lazy-k isn't that fast, I was comparing speed to the wrong interpreter, the fast one is here (and probably a good reference for making a fast untyped lambda calculus interpreter).