Lambda calculus interpreter https://github.com/M42/mikrokosmos
|Latest on Hackage:||0.2.0|
This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.
Mikrokosmos is an untyped lambda calculus interpreter, borrowing its name from the series of progressive piano études Mikrokosmos written by Bela Bartok. It aims to provide students with a tool to learn and understand lambda calculus. If you want to start learning about lambda calculus, I suggest you to read:
And to install and to tinker with this interpreter.
Mikrokosmos is installable from Hackage; you can install it directly from
cabal update cabal install mikrokosmos
You can also install it by cloning the git repository and using cabal:
git clone https://github.com/M42/mikrokosmos.git cd mikrokosmos cabal install
If you have
ghc version 8 or greater you can also compile it directly using:
git clone https://github.com/M42/mikrokosmos.git cd mikrokosmos ghc Main.hs
Once installed, you can open the interpreter typing
mikrokosmos in your terminal. It will show you a prompt where
you can write lambda expressions to evaluate them:
You can write expressions using
\var. to denote a lambda abstraction on the
var variable and
you can bind names to expressions using
=. As you can see in the image, whenever the interpreter finds a known constant, it labels the expression with its name.
If you need help at any moment, you can type
:help into the prompt to get a summary of the available options:
The standard library
Mikrokosmos comes bundled with a standard library in a file called
std.mkr; if it was not the case for you, you can download the library from the git repository. It allows you to experiment with Church encoding of booleans,
integers and much more. You can load it with
:load std.mkr, given the file is in your working directory; after that, you can use a lot of new constants:
All this is written in lambda calculus! You can check the definitions on the
Debugging and verbose mode
If you want to check how the lambda reductions are being performed you can use the verbose mode.
It can be activated and deactivated writing
:verbose, and it will show you every step on the reduction of
the expression, coloring the substitution at every step.
It uses DeBruijn notation to show the substitutions, because this is the internal representation used by the interpreter. The term in red is being substituted by the term in yellow.
Advanced data structures
There are representations of structures such as linked lists or trees in the standard library. You can use them to do a bit of your usual functional programming:
Oh! And you can insert comments with
#, both in the interpreter and in the files the interpreter can load.