Hi, Thanks for your reply. I think the Monad that I chose for my example code was not the best. I've been hoping to generalize across all possible monads but the real use case arises because I have an expensive computation that I know will repeat multiple times within the evaluation of a given large expression so in my monad I want to implement a cache. If I query the cache and it has not done the computation it will perform the computation once and then return the result plus a new cache holding the result, if the computation has already been performed it is present in the cache and taken from there. In my definition of Exp there would then be one more value, say Ext that when applied to a parameter can access and modify the cache. In this case the order of evaluation doesn't affect the result of the Monad, I'm not sure if "commutative" is the right way to describe this. There is a lot to think about here but let me try playing around with your code. Thanks, Ian On Thu, Oct 15, 2015 at 7:43 AM, wren romano wrote:

...

Here is what I'd like from the language:

* To use haskell syntax for substitution and pattern matching rather

On Wed, Oct 14, 2015 at 9:31 AM, Ian Bloom wrote: 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

-- 718.755.5483 http://ianbloom.com/