[Haskell-cafe] Monad for HOAS?

[Conal Elliott]

I share your perspective, Edsko.  If foo and (Let foo id) are
indistinguishable to clients of your module and are equal with respect to
your intended semantics of Exp, then I'd say at least this one monad law
holds.  - Conal

On Wed, May 14, 2008 at 7:59 AM, Edsko de Vries <devriese at cs.tcd.ie> wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080514/1b266709/attachment.htm