[<<][meta][>>][..]Sat Oct 22 11:47:03 EDT 2011

It looks like this Expr form is better served with a language counterpart that mirrors it exactly, but includes typing information. If this can be pulled off in a generic way, i suppose the rest would be really straightforward. So let's see if it breaks down somewhere. Now it gets confusing because this requires encoding of functions, working around the fact that we don't know the arity. Anywyays, let's proceed. class TML m r => TMLP m r where Simple, but wrong (not monadic): _let :: (r a) -> (r (a -> b)) -> (r b) Is this correct? It compiles.. _let :: (r a) -> (r (a -> m b)) -> (r (m b)) _if :: (r a) -> (r (a -> m b -> m b -> m b)) -> (r (m b)) Now, for recursive function bindings it probably becomes quite a problem to break the cycle.. It needs some kind of multi-argument Y-combinator. Or, it might be possible to construct a cyclic data structure and flatten it later? There's another problem to solve first. There is no return value! This is CPS. Let's try to see if that makes sense, setting return value to () for convenience. _let :: r a -> r (a -> m ()) -> r (m ()) _if :: r a -> r (a -> m () -> m () -> m ()) -> r (m ()) _app :: r (as -> m x) -> r as -> r (m x) It's weird that _app has practically the same type as _let. This can not be the case: some more annotation is necessary. class TMLvar r a class TMLfun r f class TML m r => TMLP x m r where _let :: TMLvar r a => r a -> r (a -> m x) -> r (m x) _if :: TMLvar r a => r a -> r (a -> m x -> m x -> m x) -> r (m x) _app :: (TMLvar r a, TMLfun r f) => r (a -> m x) -> r as -> r (m x) Just string from _let I come to: _letrec :: (TMLfun r fs) => r fs -> r (fs -> m x) -> r (m x) Where fs can be multiple functions. I still don't understand how the cyclic binding would work here. Hmm.. looks like there's an error. This doesn't support forms like: _let .. $ \v -> ... This should be it: class TML m r => TMLP x m r | r -> m where _let :: TMLvar m r a => r a -> (a -> r (m x)) -> r (m x) _if :: TMLvar m r a => (r a -> r (m x) -> r (m x) -> r (m x)) -> r (m x) _app :: TMLvars m r as => r (as -> m x) -> r as -> r (m x) _letrec :: (TMLfuns m r fs) => r fs -> (fs -> r (m x)) -> r (m x) _lambda :: TMLfun m r (as -> m x) => (r as -> r (m x)) -> r (as -> m x) I also needed a _lambda form to actually create function bodies. The _letrec just binds names with a type constraint (that they are functions). After this I have trouble expressing tuples, so maybe (since it's almost the lambda calculus) it's better to use currying anyway? Actually, no. The monad makes it impossible (or hard beyond my current abilities). I wonder... What about limiting the monad to the serialization of the expressions? Maybe the control flow part doesn't actually need it? Can it be expressed without it? It might be best to experiment with this in isolation. 1. Make a lambda language. 2. Make it monadic 3. Restrict functions to first class. Does it help to realize that a representation of a lambda in the first class language needs to be a reference? Prolly not. I get in trouble when I want to represent curried monadic functions. Maybe such things make no sense? I don't know.. Let's take a break. I lost the point. I just need lambda and application, and a way to distinguish between function and variable references. Maybe curried functions are just not such a good idea.. So.. Back to non-curried functions. The problem was the representation of the tuple if I recall. The trouble is that _lambda expects a type (r (a,b)) but we're giving it (r a, r b). _lambda :: TMLfun m r (as -> m x) => (r as -> m (r x)) -> r (as -> m x) h1 = _lambda $ \(a,b) -> _ret a That seems to be a problem. Maybe it needs a separate unpack operation? Yep, that was it: _uncons :: r (a, b) -> (r a, r b) _cons :: (r a, r b) -> r (a, b) -- single g1 = _lambda lam where lam l = _app g1 l' where (a, b) = _uncons l l' = _cons (b, a) -- mutual g2 = _lambda lam where lam l = _app g3 l' where (a, b) = _uncons l l' = _cons (b, a) g3 = _lambda $ \l -> _app g2 l Then in terms of these _cons and _uncons it's probably possible to write some generic pack / unpack operations that can dispatch on the type. Ok. Getting closer. Now some type errors. I've added explicit _nil :: r () to avoid overlapping instances. Now I can't type g1 manually. Its inferred type looks quite horrible. g1 = _lambda f where f l = _app g1 l''' where (a, l') = _uncons l (b, _) = _uncons l' l'' = _cons (a, _nil) l''' = _cons (b, l'') *TML> :t g1 g1 :: (TMLvar m r a, TMLP x4 m r, TMLP x3 m r, TMLP x m r, TMLP x5 m r, TMLP x1 m r, TMLP x2 m r) => r ((a, (a, ())) -> m x3) Adding a functional dependency r -> x helped, but I'm not sure if that's not a bit too limited.. Anyway, can always work around this in separate modules. So, trying to implement pack / unpack doesn't seem to work well. It looks like it's too generic.. Things infer but types look weird. It's probably possible but I'm getting too tired for this madness. Summary? I don't know.. I got a bit lost before I could see if it's actually going the right direction. The cool thing is that if this works: if it's possible to use the same generic code to construct target code and host evaluation/test code, then that is a big plus. I'm not 100% convinced yet it will work, or I will be able to actually pull it off.

[Reply][About]

[<<][meta][>>][..]