[Haskell-cafe] Monad for HOAS?

[Edsko de Vries]

Hi,

On Wed, May 14, 2008 at 03:59:58PM +0300, Lauri Alanko wrote:
> On Wed, May 14, 2008 at 10:11:17AM +0100, Edsko de Vries wrote:
> > Suppose we have some data structure that uses HOAS; typically, a DSL
> > with explicit sharing. For example:
> > 
> > > data Expr = One | Add Expr Expr | Let Expr (Expr -> Expr)
> > 
> > When I use such a data structure, I find myself writing expressions such
> > as
> > 
> > > Let foo $ \a -> 
> > > Let bar $ \b ->
> > > Add a b
> > 
> > It seems to me that there should be a monad here somewhere, so that I
> > can write this approximately like
> > 
> > do a <- foo
> >    b <- bar
> > 	return (Add a b)
> 
> Neat idea, but the monad can't work exactly as you propose, because
> it'd break the monad laws: do { a <- foo; return a } should be equal
> to foo, but in your example it'd result in Let foo id.
> 
> However, with an explicit binding marker the continuation monad does
> what you want:
> 
> import Control.Monad.Cont
> 
> data Expr = One | Add Expr Expr | Let Expr (Expr -> Expr)
> 
> type ExprM = Cont Expr
> 
> bind :: Expr -> ExprM Expr
> bind e = Cont (Let e)
> 
> runExprM :: ExprM Expr -> Expr
> runExprM e = runCont e id
> 
> Now you'd write your example as
> 
> do a <- bind foo
>    b <- bind bar
>    return (Add a b)

Nice. That's certainly a step towards what I was looking for, although
it requires slightly more "tags" than I was hoping for :) But I've
incorporated it into my code and it's much better already :)

You mention that a "direct" implementation of what I suggested would
break the monad laws, as (foo) and (Let foo id) are not equal. But one
might argue that they are in fact, in a sense, equivalent. Do you reckon
that if it is acceptable that foo and do { a <- foo; return a } don't
return equal terms (but equivalent terms), we can do still better?

Thanks again,

Edsko