Re: [Haskell-cafe] Re: Monad for HOAS?

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