Jebus is an interpreter for a lambda calculus variation implemented in Haskell. Jebus was created for demonstration purposes, as part of a lambda calculus course of National Technical University of Athens.
e ::= e1 e2
| """ ident "." e
| "let" ["rec"] ident "=" e1 "in" e2
| "["e1"," e1"]"
| "true" | "false"
| "if" e1 "then" e2 "else" e3
| e1 op e2
| e1 rop e2
| e1 bop e2
op ::= "+" | "-" | "*" | "**"
rop ::= "=" | "<" | "<=" | ">" | ">="
bop ::= "&&" | "||"
The language is strictly typed using the Hindley–Milner type system. The types are implicit in the source and they are reconstructed before the interpretation using the algorithm W for type inference. The supported types are natural numbers, booleans, function and product types. It features let-polymorphism.
The implementation also provides the following build-in functions:
- succ : nat -> nat
- pred : nat -> nat
- iszero : nat -> bool
- not : bool -> bool
- fst : a x b -> a
- snd : a x b -> b
To compile:
$ gch jebus.hs
Jebus reads a program from the standard input. The following command-line options are available:
$ jebus [COMMAND] ... [OPTIONS]
Common flags:
-h --help Display help message
-V --version Print version information
jebus annot
Prints an explicitly typed version of the program
jebus eval [OPTIONS]
Interpret the program
-t --trace show each beta reduction
-e --eval=EVALMODE specify evaluation strategy: normal (default) or
applicative
All the functionality is implemented using abstractions and function applications. For more imformation about the implementation read the slides in the report directory.