Transcript An Implementation of a Compiler for a Dependently Typed

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
Untyped lambda calculus for representing Agda terms
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
E.g.,
(∖x -> x) zero
⇨
VAbs (∖x -> x)
`apply` (VCon “zero” [])
struct {
inc = ∖x -> succ x;
n
= inc zero
}
⇨
let inc = VAbs (∖x ->
succ `apply` x)
n = inc `apply` zero
in VStr [(“n”,n),(“inc”,inc)]
How to deal with IO
Pass the buck to Haskell!
posutulate IO
:: Set -> Set
posutulate putStr :: String -> IO Unit
main :: IO Unit
main = putStr “Hello World”
x_main, x_putStr :: Val
x_main = x_putStr `apply` VString “Hello World”
x_putStr = VAbs (∖v -> VIO (putStr (deString v)
>> return VUnit ))
main :: IO Val
data Val
=…
main = deIO x_main
| VIO (IO Val)
| VString String
deIO
(VIO m) = m
deString (VString s) = s
Performance
GHC : Agate = 1 : 6
(execution time)
Agate (sec)
GHC (sec)
ratio
Agda
fact 8
0.130
0.022
5.9
∞
fib 20
0.071
0.012
5.9
∞
ack 3 6
0.130
0.037
3.5
∞
Conclusion
• FULL dependently typed functional
language including IO, with a very
sophisticated development environment
Availability
• Running under Linux, Windows and
MacOSX
• Visit my homepage to download Agate!
http://staff.aist.go.jp/hiroyuki.ozaki/