Thu Oct 27 09:13:44 EDT 2011

Representing functions

The main problem with doing it the standard way is that the "r" and
the "m" seem to be in the way:

The source type is one of these:

    r a -> r b -> r c -> m (r t)

    (r a, (r b, r c)) -> m (r t)

which is what compileFun accepts and turns into ([i], m [o]), which is
further converted by termFun into a Lambda data structure.

The question then seems to be, how to perform the conversation to:

    (r ((a, (b,c)) -> m t))

or any other type that can be understood by _app, the inverse of _lambda.

The important parts seem to be:

  - _app and _lambda are inverses: as long as the representation is
    understood by both we're fine.

  - for proper embedding we really need the types above and not the
    "wrapped tuple" approach where _cons and _uncons are used in the
    meta language.  that is way too inconvenient.

So... How to express this?  Essentially this is an abstraction of the
unpack / pack that already happens in syntax elements like:

  _if (Code (Ref v)) mx my = do
    (Code x) <- mx
    (Code y) <- my
    return $ Code $ If v x y

in a way that is very similar to what happens in compileFun.  To
reiterate: it really doesn't matter what the form of the
representation is, as long as there is some form of type checking that
doesn't allow operation of _app and _lambda on function types that do
not match.

Note that for a Code embedding, the type parameter (Code (a -> m b))
is a phantom type and only used as a constraint.

Plan: first try to make it work for explicit in-language tupling.
Then see if this can somehow be automated using a recursive instance

    Could not deduce (TMLprim a) arising from a use of `termFun'
    from the context (TMLprim t, LoopArgs a)
      bound by the type signature for
                 _lambda :: (TMLprim t, LoopArgs a) =>
                            (Code a -> MCode' (Code t)) -> Code (a -> MCode' t)

What you want is (CompileVar (Code a)) not necessarily (TMLprim a).

Looks like this is the (r a, r b) vs r (and _only_ used for checkinga, b) issue again.  The former
is handled by the recursive instance of CompileVar defined in
Compile.hs, but the latter is new.

Maybe we need to represent "primitive data tree" on the TML level and
derive CompileVar from that?

Let's take the error message literally: termFun knows only one way to
compile (Code a) and that is when (TMLprim a).  How can we make
termFun smarter?  I.e how to define CompileVar for  (Code (LoopArgs a))?

I don't immediately see how to do this in terms of the data interface
of Compile.  The unpacking might need to happen somewhere else.

Hmm.. no good overview.  Let's fork and try to get rid of the _cons
_uncons stuff.  It's just phantom types so maybe it's possible to do
it differently.

This is hard...  Why?  I'm making some assumptions that don't hold up.

I'm trying this approach: make functions and function reps abstract.
Solve the representation of functions in a separate class, then use
this class' ops in the Loop language.

So I have something compiling, but that usually doesn't mean much with
classes when they are not used.  Basically, I've separated LoopFun
into a separate class that defines application and abstraction for a
set of types.  This should be enough to make it work.

class LoopFun m r t as ras where
  _lambda :: (ras -> m (r t)) -> r (as -> m t)
  _app :: r (as -> m t) -> (ras -> m (r t))

I have to stop for a while..

Conclusion: because there are going to be an infinite number of
possible function types for which this "unpacking" has to be done,
it's probably indeed better to put this in a class.

TODO: how to implement that class correctly?  Does the recursion need
to be implemented for each representation r separately?