Lambda-calculus-interpreter

Untyped lambda calculus

Project of the BYOHC-Workshop.

How to use

Make

$ make

$ ./main [source pathname]
# ./main samplecode/iotest

Syntax

Lambda

\x y

Beta reduce

(\x y) z  -- evaluates `y` with `x` bounded to `z`

Expressions are left associative.

• a b c d evaluates to ((a b) c) d
• a \x y z evaluates to a (\x (y z))

IO

-- Monadic bind
-- >>= :: IO a -> (a -> IO b) -> IO b
-- Sequencial compose
-- >>  :: IO a -> IO b -> IO b

-- print a character
-- putChar :: Char -> IO ()
putChar 'a'

-- read a character
-- getChar :: IO Char
(>>= getChar (\c putChar (+ 1 c)))  -- an IO action of "read one char, shift one amount, then print it"

-- Run an IO monad with runIO
runIO (>> (putChar '4') (putChar '2'))

Comments

-- Comments start with two minuses
-- Only have single-line comments right now

Semantic sugars

let x y in z
-- evaluates `z` in the context of `x` being bounded to `y`
-- i.e. `(\x z) y`

Example

let helloworld (: 'H' (: 'e' (: 'l' (: 'l' (: 'o' (: ',' (: ' ' (: 'w' (: 'o' (: 'r' (: 'l' (: 'd' (: '!' []))))))))))))) in
let fibs Y(\fibs (: 1 (: 1 (zipWith + fibs (tail fibs))))) in
let main (>>
    (putStrLn helloworld)
    (sequence (map (\x putStrLn (showInt x)) (take 30 fibs)))
  )
in runIO main
-- See complete code in `samplecode/prelude` and `samplecode/iotest`

TODO

• Parsing
• To json
• From json
• Substitution
• Normal form
• Weak normal form
• Blah Blah
• Refactor
• Codegen