| Chapter 1 Epigram Reloaded: (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract Epigram, a functional programming environment with dependent types, interacts with the programmer via an extensible high level language of programming constructs which elaborates incrementally into Epigram’s Type Theory, ETT, a rather spartan λ-calculus with dependent types, playing the rôle of a ‘core language’. We implement a standalone typechecker for ETT in Haskell, allowing us to reload existing libraries into the system safely without re-elaboration. Rather than adopting a rewriting approach to computation, we use a glued representation of values, pairing first-order syntax with a functional representation of its semantics, computed lazily. This approach separates β-reduction from βηconversion. We consequently can not only allow the η-laws for λ-abstractions and pairs, but also collapse each of the unit and empty types. 1.1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||