[Haskell-cafe] Monadic bind with associated types + PHOAS?

[Wouter Swierstra]

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