Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Fine-grain (Small Step) implementations of common lambda calculi in Haskell.
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!
See each repo for details on installation/use.
Submit a PR if there's something you want to add or fix! Bearing in mind a few things:
-W
, This catches any warnings. There shouldn't be any warningsFoo.hs
when running hlint Foo.hs
.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.
>
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.
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.
We do the following to keep code quality up:
⇒ make quality-check
Note: when you build a single language with make build LANGUAGE=<lang>
it will lint source code for that language only.