| Agate –an Agda-to-Haskell compiler (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. We report some features of Agate, a compiler for the dependently typed functional language of Agda proof-assistant. Agate is developed to be an experimental platform for practice of dependently typed programming and it extends Agda language with I/O facilities and calls to Haskell functions. The first feature is the use of higher order abstract syntax to translate terms of Agda language into untyped λ-calculus encoded in Haskell. The second is the application of Haskell class mechanism to embed typed Haskell terms in the universal type for untyped λ-calculus. This approach makes Agate very lightweight. Performance report of some codes emitted by Agate is given. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||