Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus)

Andres LÃ¶h, Conor McBride and Wouter Swierstra

We present an implementation in Haskell of a dependently-typed lambda calculus that can be used as the core of a programming language. We show that a dependently-typed lambda calculus is no more difficult to implement than other typed lambda calculi. In fact, our implementation is almost as easy as an implementation of the simply typed lambda calculus, which we emphasize by discussing the modifications necessary to go from one to the other. We explain how to add data types and write simple programs in the core language, and discuss the steps necessary to build a full-fledged programming language on top of our simple core.

## Recent comments

3 hours 30 min ago

6 hours 49 min ago

2 days 1 hour ago

2 days 2 hours ago

2 days 8 hours ago

2 days 10 hours ago

2 days 18 hours ago

2 days 18 hours ago

2 days 19 hours ago

2 days 21 hours ago