Luke's Programming Languages Zoo

Fine-grain (Small Step) implementations of common lambda calculi in Haskell.

Motivation

I've been studying the Foundations of Programming Languages, Semantics, and Type Theory. I decided to implement some of the common Lambda Calculi to solidify my understanding.

The naming of this repo was inspired in part by Andrej Bauer's plzoo but with a focus on the underlying calculus and semantics of functional languages.

One aim of the repo is to implement popular (functional) languages and extensions to portray how the theory translates into practice.

The languages are written in Haskell and are intentionally simple. That is, they do not use advanced features of Haskell but rather minimal use of type constructors, recursion, and functional programming.

The intention here is to maximise your understanding of language design whilst minimising the need to understand Haskell. Of course it helps if you know it!

See the blog for some more pointers and a fish!

Languages

1. ULC: Alonzo Church's Untyped Lambda Calculus (Church Style)
2. SKI: Moses Schonfinkel's SKI Combinator Calculus. In essence an (untyped) combinator calculus equivalent in computational power to ULC, but without abstraction.
3. STLC: Alonzo Church's Simply-Typed Lambda Calculus (Church) with one base type and function types
4. SystemT: Kurt Godel's System T. In essence the STLC with Nat swapped out for the base type and primitive recursion on Nats.
5. PCF: Gordon Plotkin's Programming Computable Functions. In essence it's System T but using the Y combinator for general recursion instead of primitive.
6. Mu: Michel Parigot's Lambda-Mu. In essence it's STLC with continuations that don't rely on the reduction strategy used.
7. SystemF: John Reynolds' System F. In essence it's STLC with parametric polymorphism built in.
8. SOL: John Mitchell and Gordon Plotkin's SOL. In essence it's System F but with existential types made explicit.
9. Cata: In essence it's STLC with inductive types.
10. Ana: In essence it's STLC with coinductive types.
11. Sub: Benjamin Pierce's Lambda Calculus with Subtypes. In essence it's STLC with generalised records and subtype polymorphism.
12. Omega: Renardel de Lavalette's L(or λω). In essence it's STLC with kinding and type-operators.
13. FOmega: Jean Yves-Girard's FOmega. In essence it's SystemF + Omega which enables higher-order polymorphism.
14. LF: Bob Harper, Furio Honsell, and Gordon Plotkin's Edinburgh Logical Framework. In essence it's STLC with pure first-order dependent types.
15. C: Thierry Coquand and Gerard Huet's Calculus of Constructions. In essence it is FOmega + LF written in a pure type systems style. This serves as the apex of the lambda cube and a constructive foundation of mathematics.

See each repo for details on installation/use.

Contributions

Submit a PR if there's something you want to add or fix! Bearing in mind a few things:

1. Compile your code with -W, This catches any warnings. There shouldn't be any warnings
2. Use hlint, to handle code linting and suggestions. Like wall, there should be no suggesstions for file Foo.hs when running hlint Foo.hs.
3. Ensure code has 100% Haddock coverage. This helps to document things if ever we want to.
4. All of this can be run automatically (see below). Make sure to run these locally before you commit.
5. Keep in mind the motivations above, this code is not meant to be advanced Haskell, but rather simple (for demonstration) so try not to use advanced technologies if you can.

Building

First make sure your cabal is up to date:

make check-deps

Each language in the zoo can be built using cabal, or just using ghc in each directory. You can build a language from this directory using e.g:

⇒  make build LANGUAGE=ULC

and run it using:

⇒  make run LANGUAGE=ULC

and you will see something like:

⇒  cabal run ulc
Up to date
Welcome to the Untyped λ-calculus REPL
Type some terms or press Enter to leave.
>

You can build all of the languages with:

⇒  make build-all

Alternatively you can build each language with vanilla GHC. First by navigating into a language directory, you can do e.g:

⇒ cd ulc
⇒ ghc -O2 -o ulc Main -W
... Compilation bits ...
⇒ ./ulc
Welcome to the Untyped λ-calculus REPL
Type some terms or press Enter to leave.
>

Testing

The languages in the zoo are tested using unit tests in the form of example terms, QuickCheck to test parsing of randomly generated terms. This is a work in progress but for the testsuites that exist you can use cabal to run the tests:

⇒ make test
... Build bits ...
Test suite test-ulc: RUNNING...
+++ OK, passed 20 tests.
+++ OK, passed 20 tests.
Test suite test-ulc: PASS
... Rest of Tests ...
Test suite logged to:
... Log dir ...

Alternatively you can use vanilla GHC to test each langauge (you'll need a local version of QuickCheck), using:

⇒  ghci Tests.hs
*Tests> runTests
+++ OK, passed 20 tests.
+++ OK, passed 20 tests.

See the Cabal file for the testsuites.

Documentation

We use haddock to generate developer documentation:

⇒  make docs
... build things ...
Haddock coverage:
... checks all functions are covered ...
Documentation created:
... location where dev docs are stored ...

You can then open the index.html file in a browser to see the documentation

Note: when you build a single language with make build LANGUAGE=<lang> it will generate docs for that language only.

Code Quality

We do the following to keep code quality up:

1. Document every function using Haddock - see Documentation
2. Lint all implementations using hlint:

⇒  make quality-check

Note: when you build a single language with make build LANGUAGE=<lang> it will lint source code for that language only.