[Haskell-cafe] Re: Monad for HOAS?

[Edsko de Vries]

On Wed, May 14, 2008 at 06:01:37PM -0400, Chung-chieh Shan wrote:
> Conal Elliott <conal at conal.net> wrote in article <ea8ae9fb0805140915of9434b1la727da90de82635a at mail.gmail.com> 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