Mikrokosmos
User's guide (v0.8.0)

Mikrokosmos is installable from Hackage. The Haskell tools cabal and stack can be used to install it. For instance, it can be installed using cabal with the following commands.

cabal update
cabal install mikrokosmos

Binaries are also available from the GitHub repository. Manual installation is also available by cloning the git repository and using cabal or stack as follows.

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

git clone https://github.com/mroman42/mikrokosmos.git
cd mikrokosmos
stack install

The ghc compiler can be also directly used from its version 8. In that case, you must check that all the Haskell libraries on the following list are available first.

git clone https://github.com/mroman42/mikrokosmos.git
cd mikrokosmos
ghc Main.hs

Please refer to the mikrokosmos.cabal file for an updated list of libraries.

Mikrokosmos comes bundled with a collection of lambda calculus libraries. They will be directly loaded into the interpreter unless you specify the flag --no-libs.

Apart from these, you can write your own libraries and load them onto the interpreter. A library consists on a file with extension .mkr and containing definitions. The following is an example of the contents of a file ski.mkr.

# SKI combinators
S = \x.\y.\z. x z (y z)
K = \x.\y.x
I = S K K

# Schönfinkel combinators
C = \f.\x.\y.f y x
B = \f.\g.\x.f (g x)
W = \x.\y.(y y)

# Y combinator
Y := \f.(\x.f (x x))(\x.f (x x))

To load a library into the interpreter, it must be placed under your home directory in a folder called ~/.mikrokosmos, or, more easily, in the current working directory. Mikrokosmos will automatically look for libraries on the following list of directories. The :load <filename> command must then be used to load the library <filename>.mkr.

~/
~/.mikrokosmos/
./
./lib/

Please note that the Jupyter kernel does not correctly displays Unicode characters on Windows. This is a known bug, see Issue #49.

Using pip, the Jupyter kernel can be installed with the following command. Use the flag -U if you want to update a previous install to the latest version.

pip install imikrokosmos

Development versions of the kernel can be installed from its GitHub repository. For instance, you can use the following command if you want to download the source from the master branch of the repository.

pip install git+https://github.com/mroman42/jupyter-mikrokosmos.git@master

Once installed, the interpreter can be opened by executing mikrokosmos in a terminal. It will open a prompt where lambda expressions can be evaluated.

You can write expressions using \x. to denote a lambda abstraction on the x 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. You can type :help into the prompt to get a summary of the available interpreter commands.

Commands available from the prompt:
	<expression>		 evaluates the expression
	:quit       		 quits the interpreter
	:restart    		 restarts the interpreter
	:load <file>		 loads the given .mkr library or script
	:verbose <on/off> 	 sets verbose mode on/off
	:color <on/off> 	 sets color mode on/off
	:ski <on/off> 		 sets ski mode on/off
	:types <on/off> 	 untyped/simply typed lambda calculus
	:help       		 shows this help

If Jupyter and the Mikrokosmos Jupyter kernel are installed, a Jupyter Notebook server can be started by executing jupyter notebook. You can see more information in how to use a Jupyter notebook server here.

Once a notebook is opened, the mikrokosmos kernel can be selected in the menu Kernel > Change kernel > IMikrokosmos. Multiple expressions can be evaluated in one cell but each line will be evaluated separately.

The verbose mode makes the interpreter show every step on the beta reductions it performs internally using De Bruijn notation, coloring the next substitution at each step. It can be activated and deactivated by executing :verbose on and :verbose off.

Every lambda expression can be written in terms of SKI combinators, and Mikrokosmos implements a translation algorithm. The SKI mode shows every result also in terms of SKI combinators. It can be activated and deactivated by executing :ski on and :ski off.

Colored output will be activated by default. It can be deactivated however by executing :color off in the interpreter; :color on will activate the color again.

Mikrokosmos uses untyped λ-calculus by default, but you can activate the simply-typed λ-calculus interpreter using :types on. The syntax is the same on both; but there are some differences with the untyped version.

• Every term will be displayed along with its type.
• Non-typeable expressions will not be computed. Instead, an error message will be shown if a type cannot be found for the expression.
• Every computation terminates. Non-terminating computation cannot be expressed on simply-typed lambda calculus.

In particular, Mikrokosmos can be used to check proofs on intuitionistic propositional logic.

To this end, implementation of simply typed λ-calculus is presents the following type constructors.

You can directly use these types via the built-in term constructors INL, INR, ABORT, UNIT and (-,-). However, it is recommended to load the standard library and work with the type constructors already available on the library.

A lambda abstraction \((\lambda x. x)\) can be written as \x.x. Combinations of alphanumeric characters are valid variable names. Application of lambda expressions is written by yuxtaposition. For example, the following code applies the identity function to itself.

(\a.a)(\a.a)

A expression can be evaluated and the results of the evaluation bound to a name using the = operator. Sometimes, we do not want to evaluate the expression before the binding, maybe because it is a non-terminating computation. In these cases, we can use the := operator to assign a value to a variable without evaluating it.

plus = \a.\b.\c.\d.((a c) ((b c) d))
fix != \f.(\x.f (x x))(\x.f (x x))

Comments must always start with a # and they always expand for one line. This rule applies to the interpreter, the libraries and the Jupyter notebook.

When the :types option is on, and the standard library is loaded, a predefined set of type constructors and destructors are allowed on λ-expressions.

The reserved keyword :load is used to load libraries. If the library name is foo.mkr, it will be loaded using :load foo. Note that the standard libraries are loaded by default if the flag --no-libs is not activated. You can write your own libraries as *.mkr files. Each line of a library is interpreted in the same way it would be interpreted on the command line interpreter.

You can check the definitions of the standard library and examples on this repository. There are representations of structures such as linked lists or trees in the standard library.