[Haskell-cafe] Trying to write an Embedded DSL that threads a monad?

[wren romano]

On Wed, Oct 14, 2015 at 9:31 AM, Ian Bloom <ianmbloom at gmail.com> wrote:
> Here is what I'd like from the language:
>
>  * To use haskell syntax for substitution and pattern matching rather than
> implementing this myself.
>  * To be able to express lambdas in my language.
>  * To be able to embed any haskell terms including functions into the
> language.
>  * I'd like the Haskell type checker to tell me about bad terms.
>  * I'd like to thread a monad through the entire expression.

It's still not clear exactly what you want/need with that last bullet
point. So I can try to offer help, but have no idea if this is on the
right track...


> So here is the first implementation that I tried of this (full source here:
> http://lpaste.net/142959)
>
>     data Exp m x where
>        Val :: m x -> Exp m x
>        Lam1 :: m (a -> Exp m b)        -> Exp m (a -> b)
>        Lam2 :: m (a -> Exp m (b -> c)) -> Exp m (a -> b -> c)
>
> a function liftE allows me to lift a haskell term into an expression:
>
>     liftE x = Val $ return x
>
> Application is a function <@> so:
>
>     (<@>) :: forall m a b. Monad m => Exp m (a -> b) -> Exp m a -> Exp m b
>     (<@>) (Val  f) (Val x) = Val  $ f `ap` x
>     (<@>) (Lam2 f) (Val x) = Lam1 $ f >>= \f' -> x >>= \x' -> unLam1 $ f' x'
>     (<@>) (Lam1 f) (Val x) = Val $ f >>= \f' -> x >>= \x' -> unVal $ f' x'
>
>[...]
>
> Ok so that's a lot. I was surprised I got this working. You can see from the
> code that my main gripe with this is I haven't found a way to remove the
> need to specify the number of embedded lambdas using Lam1 and Lam2 (we could
> easily add more) and I haven't found a way to apply a Lam to another Lam.
> I'm also curious if I am reinventing the wheel, I hadn't found a library yet
> that let's me do something similar.

So, two things to notice.

First, the type for Lam2 is just a refinement of the type for Lam1.
Thus, Lam2 gives you nothing new in terms of what can be made to
typecheck; the only thing it gives you is the ability to make runtime
decisions based on whether a particular expression was built with Lam1
or Lam2 (or Val).

Second, the apparent need for multiple lambdas stems from the fact
that your (<@>) function needs to "count down by one" each time an
argument is applied. This hides a big problem in the definition,
namely that you're assuming that after the right number of arguments
the resulting Exp will be built with Val; which isn't actually
guaranteed by the types.

After playing around with it for a while, it seems like the crux of
the issue comes from not being able to embed m(Exp m a) into Exp m a.
So, we can fix that by adding a new constructor:

    data Exp m x where
        Val :: m a -> Exp m a
        Exp :: m (Exp m a) -> Exp m a
        Lam :: m (a -> Exp m b) -> Exp m (a -> b)

    Exp f <@> x     = Exp ((<@> x) <$> f)
    f     <@> Exp x = Exp ((f <@>) <$> x)
    Val f <@> Val x = Val (f <*> x)
    Lam f <@> Val x = Exp (($) <$> f <*> x)
    -- TODO: Val/Lam and Lam/Lam cases...

    unVal :: Monad m => Exp m a -> m a
    unVal (Val v) = v
    unVal (Exp e) = e >>= unVal

This at least works for the given test case with mapE, testExpression,
and test— though it doesn't give exactly the same result about the
number of binds. But again I'm not sure what you're really after here.

(Note that, once we add the Exp constructor, we can redo Val to take a
pure argument without losing anything re typeability. Though again,
the exact semantics of dubious things like (>>=)-counting won't
necessarily be preserved. Still, as a general rule, it makes sense for
EDSLs to distinguish between pure values vs impure expressions...)

-- 
Live well,
~wren