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