James T. Martin
59a55acdc6
This is done by requiring applications to be at least 2 terms, and making grouping a syntactic feature instead of a feature of applications. I also made the code a bit more clear by handling whitespace a bit more cleanly; now, each parser is responsible for its own trailing whitespace, and whitespace handling is pushed down to the token level to avoid cluttering high-level definitions with whitespace stuff. This all also had the effect of improving error messages, in part due to me labelling many of the parsers. |
||
|---|---|---|
| .github/workflows | ||
| app | ||
| src | ||
| test | ||
| .editorconfig | ||
| .gitignore | ||
| LICENSE | ||
| README.md | ||
| Setup.hs | ||
| package.yaml | ||
| stack.yaml | ||
| stack.yaml.lock | ||
README.md
Lambda Calculus
This is a simple implementation of the untyped lambda calculus with an emphasis on clear, readable Haskell code.
Usage
Type in your expression at the prompt: >> .
The expression will be evaluated to normal form and then printed.
Exit the prompt with Ctrl-c (or equivalent).
Example session
>> let D = \x. x x; F = \f. f (f y) in D (F \x. x)
y y
>> let T = \f x. f (f x) in (\f x. T (T (T (T T))) f x) (\x. x) y
y
>> (\x y z. x y) y
λy' z. y y'
>> let fix = (\x. x x) \fix f x. f (fix fix f) x; S = \n f x. f (n f x); plus = fix \plus x. x S in plus (\f x. f (f (f x))) (\f x. f (f x)) f x
f (f (f (f (f x))))
>> ^C
Notation
Conventional Lambda Calculus notation applies,
with the exception that variable names are multiple characters long,
\ is permitted in lieu of λ to make it easier to type,
and spaces are used to separate variables rather than commas.
- Variable names are alphanumeric, beginning with a letter.
- Outermost parentheses may be dropped:
M Nis equivalent to(M N). - Applications are left-associative:
M N Pmay be written instead of((M N) P). - The body of an abstraction or let expression extends as far right as possible:
\x. M Nmeans\x.(M N)and not(\x. M) N. - A sequence of abstractions may be contracted:
\foo. \bar. \baz. Nmay be abbreviated as\foo bar baz. N. - Variables may be bound using let expressions:
let x = N in Mis syntactic sugar for(\x. N) M. - Multiple variables may be defined in one let expression:
let x = N; y = O in M