[<<][meta][>>][..]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 composition. 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" state. 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.

[Reply][About]

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