Hi Ryan,
On 19 Nov 2008, at 04:39, Ryan Ingram wrote:
In HOAS, a lambda expression in the target language is represented
by a function in the source language:
data ExpE t where
ApE :: ExpE (a -> b) -> ExpE a -> ExpE b
LamE :: (ExpE a -> ExpE b) -> ExpE (a -> b)
But without a way to inspect the function inside LamE, you can't get
back to the "source code". You end up adding special constructors for
"Primitive" or "Variable" to let you do something with the resultant
structure, which leads to the expression language containing "unsafe"
constructors which need to be hidden.
There's a perfectly legitimate way to incorporate free variables in
your expression data type, without sacrificing type safety. You just
need to parametrise your expression type by the context:
> data Exp g t where
> App :: Exp g (a -> b) -> Exp g a -> Exp g b
> Lam :: (Exp g a -> Exp g b) -> Exp g (a -> b)
> Var :: Var g a -> Exp g a
>
> data Var g a where
> Top :: Var (a,g) a
> Pop :: Var a g -> Var a (b, g)
I wouldn't call this "unsafe" (or at least no more unsafe than HOAS).
Note that in particular "Exp Empty a" correspond to closed terms,
where Empty denotes the empty type.
Secondly, you can always turn a HOAS Exp into non-HOAS expression.
Essentially, you map applications to applications, etc. The only
interesting case deal with lambda abstractions - there you need to
generate a fresh variable name, apply the function to the fresh
variable, and continue traversing the resulting expression. You might
be interested in a tutorial Andres Loeh, Conor McBride, and I wrote
about implementing a dependently typed lambda calculus:
http://www.cs.nott.ac.uk/~wss/Publications/Tutorial.pdf
The "quote" function in Figure 7 gives the code.
Does anyone think this is a direction worth pursuing?
I'm not convinced yet. The problem is that there's no best way to
handle binding. HOAS is great for some things (you don't have to write
substitution), but annoying for others (optimisations or showing
code). From your message, I couldn't understand why you want to use
monads/do-notation to handle binding. Care to elaborate?
All the best,
Wouter
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
