Lambda Calculus to SKI compiler and runtime.
This project is composed of:
- A Haskell compiler from lambda calculus expressions to a custom ski byte code
- A C interpeter that runs the ski expressions via graph reduction
- A Python interpeter that runs the ski expressions via compilation to lazy thunks.
This is inspired by Miranda's compilation model and Lazy K.
The runtime only evaluates and prints output, it does not take input. It excepts that the input code will be a stream of bytes with the given type encodings:
type bool = forall a. a -> a -> a
type byte = forall r. (bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> r) -> r
type list a = forall r. r -> (a -> list a -> r) -> r
type stream = list byte
These types use Mogensen Scott encoding.
Notice that list uses a recursive type rather then Boehm-Berarducci encoding.
A 1 bit is encoded as true (λx y. x).
- variables :
x - lambdas :
x => e - application :
e e' - let-in :
x = e; e' - parenthesis :
(e) - character :
'a' - nil :
[] - cons :
e : e' - string :
"abcd" - axiom :
_builtin x_builtin 'x'
The parenthesis are equivalent to the inner term.
The let expressions are equivalent to creating a lambda and immediately calling it.
character, nil, and cons use the byte, list and list encoding respectively.
Axiom are emitted direct into the output.
C-style // comments are supported
The byte code format is very similar to Iota except that it uses s and k rather then just i.
code = "0" code code | "1" | "2"
Where 0 e e' is e(e'), 1 is k, and 2 is s.
The C interpeter has some internal additional axioms to used by runtime.lambda to aid graph reduction.
The format the compiler emits in is configurable but format the runtime accepts is not. See ./sky --help for format configuration details.
Install these packages
- make
- gcc
- python3
- ghc
- libghc-megaparsec-dev
Ensure that the Gnu C Compiler, Python, the Glasgow Haskell Compiler, Cabel are all installed, then run:
cabal install megaparsec --lib
Run make to build the executables and make samples to run the samples.
- For a general introduction into the lambda calculus: Lambda Calculus - Fundamentals of Lambda Calculus & Functional Programming in JavaScript .
- For a general introduction into ski combinators and graph reduction: "An Introduction to Combinator Compilers and Graph Reduction Machines" by David Graunke.