Mary had a little lamb,
little lamb, little lamb.
Mary had a little lamb,
its fleece was white as snow...
A "blazingly fast" lambda calculus interpreter in Rust and Chumsky (a beautiful parser combinator library), using de Bruijn indices and full-reducing Krivine machine (KN) as the default evaluation strategy.
Note
This repo is a toy project and is under active development.
- Rust (recent version should work)
- Cargo
# Install from git
cargo install --git https://github.com/MagentaManifold/little-lamblittle-lamb /path/to/your_program.lilExamples can be found in the /examples directory. Some of them don't make much sense.
# Run an example
cargo run -- examples/example.lil
# or run with installed binary
little-lamb examples/example.lilPretty standard lambda calculus syntax. Indentation and line breaks are ignored.
\x . x -- identity
\x y . x -- K combinator
The currying syntax is a syntax sugar for nested lambdas.
E.g., \x y . x is equivalent to \x . \y . x.
f x -- apply f to x
Function application is left associative and has higher precedence than lambda (and parentheses have the highest precedence, of course).
E.g., \x . x x x is equivalent to \x . ((x x) x).
let a = <X> in <Y> is a syntax sugar for (\a . <Y>) <X>.
let I = \x . x in
let K = \x y . x in
K I K
Multiple let bindings can also be written using comma syntax:
let
I = \x . x,
K = \x y . x, -- trailing comma is optional
in
K I K
-- Or, you can even do leading comma (inspired by Elm)
let
, I = \x . x
, K = \x y . x
in
K I K
All above are equivalent. The comma syntax supports leading and trailing commas for convenience.
Natural numbers are a syntax sugar for Church numeral encoding.
import add in
add 2 3
-- evaluates to \f . \x . f (f (f (f (f x)))),
-- i.e., 5 in Church numeral encoding
Anything after -- until the end of line is ignored. There are no comment blocks.
\x . x -- this is a comment
Import syntax is still WIP. Currently, it only supports flat imports (no nested directories) and has limited error handling.
You can import definitions from other files or from the built-in standard library:
import I in -- import identity combinator from std lib
import K as const in -- import with alias
import add, succ in -- import multiple modules
I const
import <mod> as <name> in <body> is a syntax sugar for let <name> = <module file content> in <body>, and comma separated imports is equivalent to nested imports.
The import system works as follows:
- User modules: First search for
.lilfiles relative to the current file's directory - Built-in modules: Fallbacks to searching in the embedded standard library (
lib/directory)
Available built-in modules include:
- Combinators:
I(identity),K(constant),S(substitution),Y(fixed point) - Boolean logic:
true,false,and,or,not,if - Pairs:
pair,car,cdr - Arithmetic:
add,mult,sub,succ(successor),pred(predecessor),iszero
Current limitations:
- No nested directories (only flat module structure)
- No relative imports (
../or./) - Circular dependencies will cause an error
# Run tests
cargo test
# Run benchmarks (uses Criterion for stats)
cargo bench
# Build release version
cargo build --release- Syntax (
src/syntax/): AST/Expression/de Bruijn term types and conversions (ast.rs,expr.rs,term.rs) plus desugaring (desugar.rs) - Lexer (
src/lexer.rs): Tokenizes source code into tokens - Parser (
src/parser.rs): Parses tokens into AST using Chumsky - Import (
src/import.rs): Handles module imports and dependency resolution - Evaluator (
src/eval/): Multiple evaluation strategieskn.rs: A Full-reducing KN machine.substitution.rs: Naive substitution based evaluation, very slow .krivine.rs: A pile of incomprehensible vibe-coded crap that miraculously works. Left here only as a baseline for benchmarking.
- Main (
src/main.rs): CLI entry point
- Tokenize source into
Vec<Token> - Parse tokens into
Ast - Desugar AST into
Expr - Convert to de Bruijn indices (
Term) - Eval to normal form (or give up after step limit reached)
- Print result
I'd be surprised if anyone else would like to work on it, but let me know if you are interested.
Roughly in descending order of priority:
- Syntax support for common encodings like booleans (done with importing) and Church numerals.
- Syntax support for more structures, like pairs and lists
- Improve performance
- Improve import system: nested directories, better error messages
- Support converting results back to primitives and common combinators (not perfect right now, but basically working)
- Better error messages
- Support step by step evaluation
- Support REPL
- Add more examples/library functions
- Create a web demo (compile to WASM)
- Clean up tests (most are LLM generated, some aren't really helpful)
- LSP support (Kinda ambitious, could be another project)
- Support Tromp's Diagram styled visualization or other types of graphical representation (a very ambitious goal)
This project is licensed under MIT License.