This project is an implementation of different lambda calculi. Terms are implemented using locally nameless representation, as described in this paper. So far, the project includes untyped lambda calculus and simply typed lambda calculus.

This project has most recently been most recently tested using GHC 8.4.1, and requires an installation of the parsec and containers libraries. See the included lambda-cube.cabal file for specific version requirements.
Note that the build-depends section has been auto-generated by cabal, and the minimum requirements are likely lower.

From the root directory, run cabal build to install dependencies, build the lambda-cube library, and build the lambda-parser executable, which will be located in the dist/build/lambda-parser directory.

Documentation for the source modules can be generated by running cabal haddock for just the lambda-cube library or add the --executables flag to add documentation for the executable.

To explore the libary interactively, run cabal repl lambda-cube and all of the modules will be available for import.

Running the lambda-parser executable will bring up a prompt to enter in a lambda term to be reduced. From the parser documentation:

A typing context is expected first, wrapped in square brackets [].
The elements inside are pairs (n,type) where n is a natural number and type is a valid type. Consecutive pairs do not have any delimiter, and in the case of multiple pairs containing the same number n, the type associated with that variable in the context will be the last in the list.

Types are expected to be characters, typically uppercase, separated by arrows, ->. Parentheses can be used to override arrow type's right associativity.

For terms, no spaces, \:type. to represent lambda binders. Bound variables are represented as natural numbers referencing their binder as is standard in De Bruijn notation. Free variables are also represented by natural numbers, but with an 'f' preceding them. Application is implicit with adjacent terms, but parenthesis can be used to change the order of application and end the binding scope of a lambda.

After a valid term is entered, if it is a terminating untyped term or is a properly-typed term, a reduction sequence to its normal form will be displayed. Non-terminating terms cause an infinite loop and invalid type annotations will output the reason for the failure.