Wed Jan 4 10:22:27 EST 2012


class SysCompile stx u i where
  sysCompile :: u -> i -> stx

Hmm... not abstract enough.

What about hiding all the operations in a SSM class, then doing *just*
the phantom type in Sys.

This is what it looks like, without interface:

  data Sys stx m i o = 
    forall s. () => Sys (SSM m s i o)

  instance Monad m => Category (Sys stx m) where
    (.) (Sys f) (Sys g) = Sys (ssmSer f g)
    id  = Sys (ssmPure id) 

  instance Monad m => Arrow (Sys stx m) where
    arr f = Sys (ssmPure f)
    (***) (Sys f) (Sys g) = Sys (ssmPar f g)
    first   a = a *** (arr id)
    second  a = (arr id) *** a

  instance Monad m => Functor (Sys stx m i) where
    fmap f op = (arr f) . op

  instance Monad m => Applicative (Sys stx m i) where
    pure f = arr $ \_ -> f
    (<*>) f a = fmap (uncurry ($)) (f &&& a)

The trick is now to add a compilation interface to SSM.  One that
guarantees the preservation of that interface after ser/par

Still note: this is entirely optional.  SSM might be good enough!

This is a strange thing.  How to express in a general way that when
the inputs of ssmSer / ssmPar / ssmPure are compilable, that also the
outputs are?  The only thing that happens is (,)

But the way this is encoded in dependencies seems "upside down".
Eventually in Loop / Array this is encoded in the recursive instances
of TMLword and Struct.

The trouble is that there are quite a lot of constraints that need to
be satisfied before a function can be compilable, so maybe this just
needs to be added as type constraints to the SSM data structure?

The thing is that by itself, SSM is quite simple and doesn't need all
that.  The trouble really arrives somewhere else, so maybe these
things should be expressed as part of Sys's constraints?

So what about 3 layers:

   - SSM:     basic types, no fuss
   - CSSM:    all type class constraints for compilable SSM
   - Sys:     only phantom state

Hmm.. I won't get there with mindless manipulation.

What's the point?

       Compositions of compilable SSM are compilable SSM.

How to express that?  Put it in a class with proper constraints.
How to prove it?  Provide instances.

It's more directional:

       If a, b are compilable SSM  

       then a `ser` b, a `par` b are compilable SSM

I don't see a way to encode that in a recursive type class because the
compile operation is completely opaque: you can't compile 2 parts of
this "composition" separately.

Maybe the key lays in not compiling to stx, but to another "growing"

Pff.. mismatch between intuition and tools.  Another one of those
"glossed-over isomorphisms" that's not properly encoded.

This probably just needs time.  Or some rest.