A λ-calculus interpreter

A strongly-normalizing interpreter for the untyped lambda calculus.

$ make
$ ./lc "(λ x y. x) (λ x. x)"
Input: (λ x y. x) (λ x. x)
Compiling... Compiled! Normalizing...
Normal form: λ a b. b

Features

Generational copying GC, with a dynamically sized old space
Custom strongly normalizing lazy evaluation runtime
Compiles lambda terms to x86_64 machine code

Only tested on Linux, and it only supports x86_64.

What?

Normalizing a term in the λ-calculus means applying the β-reduction rule until it can't be simplified any more. While it's usually described using syntactic substitution, the fastest algorithm in practice (normalization by evaluation) involves running it like a regular functional programming language, with a catch: we need to run programs with free variables in them, requiring some special runtime support.

There are, of course, many ways to run a regular functional programming language: eager vs lazy evaluation, interpreted vs bytecode interpreted vs compiled to machine code, etc. This implementation uses lazy evaluation and compiles to machine code.

How?

Short description of the lazy evaluation implementation strategy:

Push/enter, like Clean and old GHC
Closures instead of supercombinators, like GHC
Separate data stack + call stack, like Clean
Every heap object's a closure, like GHC
Eager blackholing
Thunk entry code pushes its own update frame, like GHC
Collapsing adjacent update frames is handled by the thunk entry code

It has a two-pass compiler and a simple generational copying GC.

Simple benchmarks

The file bench.lc contains a lambda calculus program that does some Church numeral math, with normal form λ s z. z. The same lambda term is implemented in Haskell in different ways in haskell/{Strong,Weak}.hs.

Here are the results, on my computer:

This interpreter: 3.5 seconds; allocates 5,854,199,808 bytes
Haskell, Strong.hs: 2.5 seconds; allocates 8,609,423,616 bytes

This would perform comparably to a Haskell-based implementation of the "Tagged normalization" presented in the paper about Coq's native_compute.
Haskell, Weak.hs: 2.3 seconds; allocates 6,887,761,200 bytes

This would perform comparably to a Haskell-based implementation of the native_compute paper's "Untagged normalization".

Despite allocating a lot, this lambda term uses very little space: GHC reports ~50K max residency in both cases (and it's similar for my interpreter, but I haven't measured).

The extra 1.7GB that the tagged implementation allocates compared to the untagged implementation come from two sources: both the overhead of including tags, and the overhead of currying not being optimized. I'm surprised the overhead is so little.

This interpreter and the untagged implementation should make pretty much the same allocations, so I think the extra gigabyte that Weak.hs allocates comes from two cases where GHC's heap objects are larger than mine:

GHC's thunks all contain an extra word, for lock-free concurrency reasons
GHC's partial application objects use a 3-word header, while mine use only 2 words

IMO the main takeaway from this benchmark is that for purely functional languages, the garbage collector is key. How currying is done, how arguments are passed, etc., all matter much less than having a high-quality garbage collector.

The one area where this interpreter beats GHC is compile time: it compiles the term practically instantly.

Future things

Really ought to have:

Big enough tests to actually test the GC
Standardize a global term size limit
mmap the data stack with a guard page below it
Make sure allocations are inlined in the runtime
Benchmarks
Fix the -Wstrict-aliasing warnings
Document the runtime better

Want to have:

Add support for fix, let/letrec
Nice CLI and REPL

Probably won't have but would be cool:

Use it in some algorithm that requires strong normalization, like a dependent typechecker or possibly supercompilation by evaluation

License

mb64/LC-interpreter

ErrorLooks like something went wrong!

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Languages

Error
Looks like something went wrong!

Packages