Agate: an Agda-to-Haskell compiler AIST / CVS Hiroyuki Ozaki (joint work with Makoto Takeyama)
What is Agda? Proof assistant based on Martin-Löf type theory. Curry-Howard correspondence available for its core language - ⇒ Proof language can be regarded as a functional programming language with dependent types.
Full language contains extension of packages, classes (therefore, monads), hidden arguments, metavariables, etc.
Goal To provide a tool for experimentation of programming with dependent types. - implement the tool quickly
- reasonably fast execution of the emitted code
- deal with “side effects,” such as I/O.
Requirements Treat full Agda language Faster execution - compile, rather than interpret!
Quick implementation - make the target language be Haskell
- Agda language is close to it and there is GHC which generates executable binaries of high quality
- use Higher Order Abstract Syntax
- to eliminate coding for variable substitution
Our HOAS Tree data Val = VAbs (Val -> Val) | VCon String [Val] | VStr [(String, Val)] | VIO (IO Val) apply :: Val -> Val -> Val apply (VAbs f) v = f v select :: Val -> String -> Val select (VStr bs) x = lookup x bs
How to deal with IO Pass the buck to Haskell!
Performance GHC : Agate = 1 : 6 (execution time)
Conclusion Running under Linux, Windows and MacOSX Visit my homepage to download Agate! - http://staff.aist.go.jp/hiroyuki.ozaki/
Dostları ilə paylaş: |