Agate: an Agda-to-Haskell compiler aist / cvs hiroyuki Ozaki

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.

• To achieve it, we need

• implement the tool quickly
• reasonably fast execution of the emitted code
• deal with “side effects,” such as I/O.

Requirements

• Treat full Agda language

• use parser of the current Agda implementation

• 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)

• | VString String

• 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/