mikrokosmos: Lambda calculus interpreter

[ gpl, language, program ] [ Propose Tags ]

A didactic untyped lambda calculus interpreter.

[Skip to Readme]
Versions [faq] 0.1.0, 0.2.0, 0.3.0, 0.4.0, 0.5.0, 0.6.0, 0.8.0
Dependencies ansi-terminal, base (>=4.7 && <5), containers (>=0.5), haskeline (>=0.7), HUnit (>=1.0), mtl (>=2.2), multimap, parsec (>=3) [details]
License GPL-3.0-only
Author Mario Román (M42)
Maintainer mromang08+github@gmail.com
Category Language
Home page https://github.com/M42/mikrokosmos
Bug tracker https://github.com/M42/mikrokosmos/issues
Source repo head: git clone git://github.com/M42/mikrokosmos.git
Uploaded by mroman42 at Sat Sep 10 11:40:17 UTC 2016
Distributions NixOS:0.8.0
Executables mikrokosmos
Downloads 2293 total (167 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
Last success reported on 2016-11-20 [all 3 reports]


Maintainer's Corner

For package maintainers and hackage trustees

Readme for mikrokosmos-0.1.0

[back to package description]


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 will be soon installable from Hackage. Meanwhile, you can install it cloning the repository and using cabal:

git clone https://github.com/M42/mikrokosmos.git
cd mikrokosmos
cabal install

First steps

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:

First steps

You can write expressions using \var. to denote a lambda abstraction on the var variable and you can bind names to expressions using =. But why am I getting this weird output? Well, the interpreter outputs the lambda expressions in De Bruijn notation; it is more compact and the interpreter works internally with it. However, 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:

Help screen

The standard library

Mikrokosmos comes bundled with a standard library. It allows you to experiment with Church encoding of booleans, integers and much more. You can load it with :load std.mkr; after that, you can use a lot of new constants:

Standard library

All this is written in lambda calculus! You can check the definitions on the std.mkr file.

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.

Verbose mode

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.

References & interesting links