Skip to content

Latest commit

 

History

History
34 lines (24 loc) · 978 Bytes

README.md

File metadata and controls

34 lines (24 loc) · 978 Bytes
Raw

simple

An implementation of simply typed lambda calculus in Haskell

Overview

simple is an implementation of simply typed lambda calculus presented by Benjamin C. Pierce in his Types and Programming Languages. I transliterated the original source code written in OCaml into Haskell except for the parser which I rewrote in Parsec.

Syntax

  • Variables: x
  • Applications: x x
  • Lambda abstractions: \x.x
  • Conditional: if x then y else z
  • Booleans: true, false

Implementation Details

  • The representation of a variable is a number - its De Brujin index
  • Evaluation performs substitution

REPL

simplei is a REPL where you can input a lambda calculus term.

% \x:Bool.x
(\x:Bool.x)
$ (\x:Bool->Bool.x) true
parameter type mismatch at (1,19)