Monad for HOAS?

newer
saner shootout programs

older
Re: Richer (than ascii) notation...

Edsko de Vries

14 May 2008 14 May '08

9:11 a.m.

Hi, 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) or something along those lines. It is however not at all clear to me what this monad should look like. I have experimented with adding a type parameter to Expr, something like

...

data Expr a = One | Add (Expr a) (Expr a) | Let (Expr a) (Expr a -> Expr a) | Place a

which has the additional benefit of supporting catamorphisms; I have also experimented with defining various variations on

...

Let a b = Let a (a -> b)

and making Let an instance of Monad rather than Expr; but none of my experiments wered satisfactory. Am I missing something obvious, or is there a good reason this cannot be done? Thanks, Edsko

Show replies by date

Lauri Alanko

14 May 14 May

12:59 p.m.

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) HTH. Lauri

Edsko de Vries

2:59 p.m.

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

Lauri Alanko

3:25 p.m.

On Wed, May 14, 2008 at 03:59:23PM +0100, Edsko de Vries wrote:

...

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?

If you just want the syntactic sugar and don't care about monads, in GHC you can use plain do-notation: {-# OPTIONS -fno-implicit-prelude #-} import Prelude hiding ((>>=), fail) data Expr = One | Add Expr Expr | Let Expr (Expr -> Expr) (>>=) = Let fail = error t :: Expr t = do a <- One b <- Add a a Add b b That's generally pretty icky, though. Lauri

Conal Elliott

4:15 p.m.

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Chung-chieh Shan

10:01 p.m.

Conal Elliott wrote in article in gmane.comp.lang.haskell.cafe:

...

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

I am at least sympathetic to this perspective, but the Expr constructors are not as polymorphic as the monad operations: if in do a <- foo return a foo has type "ExprM String" (perhaps foo is equal to "return []"), then we want to generate the DSL expression "Let [] id", but "[]" is not of type "Expr". Because whenever foo's type is not "ExprM Expr" the above code using do notation must be exactly equal to foo, by parametricity even when foo's type is "ExprM Expr" we cannot generate Let. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig The pomotarians have nothing to lose but their value chains. Call the Thermodynamics Police!

Edsko de Vries

15 May 15 May

6:04 a.m.

On Wed, May 14, 2008 at 06:01:37PM -0400, Chung-chieh Shan wrote:

...

Conal Elliott wrote in article in gmane.comp.lang.haskell.cafe:

...
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

I am at least sympathetic to this perspective, but the Expr constructors are not as polymorphic as the monad operations: if in

do a <- foo return a

foo has type "ExprM String" (perhaps foo is equal to "return []"), then we want to generate the DSL expression "Let [] id", but "[]" is not of type "Expr". Because whenever foo's type is not "ExprM Expr" the above code using do notation must be exactly equal to foo, by parametricity even when foo's type is "ExprM Expr" we cannot generate Let.

Yes, absolutely. This is the core difficulty in designing the monad, and the reason why I started experimenting with adding a type constructor to Expr data Expr a = One | Add (Expr a) (Expr a) | Let (Expr a) (Expr a -> Expr a) | Place a This is useful regardless, because we can now define catamorphisms over Expr. Nevertheless, I still can't see how to define my monad properly (other than using Lauri's suggestion, which has already improved the readability of my code). Return is now easy (return = Place), and it should be relatively easy to define a join operation Expr (Expr a) -> Expr a *but* since Expr uses HOAS, it is not an instance of Functor and so we cannot use the join operator to define return. Actually, I think this approach is a dead end too, but I'm not 100% sure. Edsko

6263

Age (days ago)

6264

Last active (days ago)

List overview

Download

6 comments

4 participants

participants (4)

Chung-chieh Shan
Conal Elliott
Edsko de Vries
Lauri Alanko