/gadt-STLC

lambda calculus interpreter using GADTs

Primary LanguageHaskellBSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

Implementation of simply typed lambda calculus, using GADTs achieve a representation of well-typed terms.

Inspired by this talk by Richard Eisenberg.

Installing

Run

cabal configure
cabal build

Then run cabal run gadt-STLC

Language

The language is just simply-typed lambda calculus with recursion.

  • The only types are Int, Bool, and t -> t
  • There are integer constants and the operations +, -, ==, <, >
  • There are lambda abstractions and applications: lam x:Int.x and e e. You must annotate the type of all lambdas
  • There are let expressions: let x = e in e
  • There are if expressions: if e1 then e2 else e3, where e1 must have type Bool and e2 must have the same type as e3.
  • There is the fixed point combinator: fix f, where f has type a -> a. We can use this to define recursive functions.

Repl Interaction

The REPL uses commands prefixed with : like in GHCi.

  • :eval or :e evaluates an expression and displays its type. This is also the default action of the REPL (if you just type an expression)
  • :step or :s uses small-step evaluation and displays all the reductions
  • :type or :t displays the type of an expression
  • :parse or :p displays the result of parsing (but not typechecking) the input
  • Ctrl-D to exit