Sat Oct 22 11:47:03 EDT 2011

Compiling to expression form

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

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

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
  :: (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.