Covering untimed/SDF with the MoC class

ugeorge commented 8 years ago

Up till now timed MoCs fitted elegantly with the atom view due to their applicative style of operating on signals, thus I could cover them all as instances of a class MoC. With untimed MoCs things are a bit more complicated since the function applied takes vectors as arguments. Instantiating for example SDF couldn't be that complicated, right? Just express the function arguments as type synonym families... well, not really. The type-level constraints are quite a pain to deal with.

Long story short : this compiles and behaves just fine:

import qualified Data.Param.FSVec as V
...
(-$-) :: (Nat rate) => (V.FSVec rate a -> b) -> Signal a -> Signal b
_ -$- NullS = NullS
f -$- sig   = let x  = (V.reallyUnsafeVector . take c . fromSignal) sig
                  xs = dropS c sig 
                  c  = V.length x
              in if c == length (V.fromVector x) then f x :- (f -$- xs) else NullS

I need though to express this as an instance of:

class MoC e where
  type Arg e a
  (-$-)  :: (Arg e a -> b) -> Signal (e (Value a)) -> Signal (e b)

The pain is described in a recent question on StackOverflow, where I did not get an answer yet.

@2opremio : sorry to tag you too, but since you implemented FSVec, do you know a way to either cheat the type system to express it as a type synonym (Rank2Types does not work with type families), or somehow extract the size so that I am correctly building x in the let binding?

P.S.: this fails miserably:

newtype ArgV a = ArgV (forall rate.Nat rate => FSVec rate (Value a))
instance MoC SDF where
  type Arg SDF a = ArgV a
  f -$- sig   = let x  = (V.reallyUnsafeVector . take c . fromSignal . fmap fromSDF) sig
                    xs = dropS c sig 
                    c  = V.length x
                in if c == length (V.fromVector x) then SDF (f (ArgV x)) :- (f -$- xs) else NullS

because for some reason x does not seem to have its size inferred as rate, but as an unknown s0.

ugeorge commented 8 years ago

@2opremio : sorry, it has nothing to do with FSVec. It is a Haskell feature that type families are not injective.

Since it is impossible prove injectivity due to the library design, some heavy plumbing needs to be done in order to cheat the type checker into accepting type synonyms with and without "context". And since it is a hacking job, I alone need to do this (a.k.a. sorry for tagging you).

2opremio commented 8 years ago

No worries! Are you going to give the suggestion in the Stackoverflow answer a try?

On Jul 4, 2016 12:18, "George Ungureanu" notifications@github.com wrote:

@2opremio https://github.com/2opremio : sorry, it has nothing to do with FSVec. It is a Haskell feature that type families are not injective.

Since it is impossible prove injectivity due to the library design, some heavy plumbing needs to be done in order to cheat the type checker into accepting type synonyms with and without "context". And since it is a hacking job, I alone need to do this (a.k.a. sorry for tagging you).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/forsyde/forsyde-atom/issues/5#issuecomment-230267885, or mute the thread https://github.com/notifications/unsubscribe/ACQOJBtEv67bitWuCSDmrjGzL5ScnPmtks5qSOwKgaJpZM4JBmv- .

ugeorge commented 8 years ago

Yeah... that didn't really work out. Although the answer I got competent, it was (by just a few lines of code) off the actual question. I tried modifying it since it was complete enough, but my modifications were not accepted it seems. I guess I need to write another answer in this case.

Of course, the scale of the problem I am faced with is far larger than the minimal example I gave, and posting my full presumed solution (i.e. heavy hacking) makes no sense for a StackOverflow post.

On 2016-07-04 14:20, Alfonso Acosta wrote:

No worries! Are you going to give the suggestion in the Stackoverflow answer a try?

On Jul 4, 2016 12:18, "George Ungureanu" notifications@github.com wrote:

@2opremio https://github.com/2opremio : sorry, it has nothing to do with FSVec. It is a Haskell feature that type families are not injective.

Since it is impossible prove injectivity due to the library design, some heavy plumbing needs to be done in order to cheat the type checker into accepting type synonyms with and without "context". And since it is a hacking job, I alone need to do this (a.k.a. sorry for tagging you).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub

https://github.com/forsyde/forsyde-atom/issues/5#issuecomment-230267885, or mute the thread

https://github.com/notifications/unsubscribe/ACQOJBtEv67bitWuCSDmrjGzL5ScnPmtks5qSOwKgaJpZM4JBmv- .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/forsyde/forsyde-atom/issues/5#issuecomment-230278031, or mute the thread https://github.com/notifications/unsubscribe/AJBn1L48YeUdFJdXvb6OVMdCmw_myarKks5qSPqXgaJpZM4JBmv-.

ugeorge commented 8 years ago

The lastest compilable version of my attempts to cover the untimed/SDF MoCs in the same atom class as the timed ones are found in the sdf-inclusion branch.

Idea:

define event constructors to include a "context" type variable (member of NoContext for timed and Nat for untimed)
redefine atom functions to carry this "context" as such both the argument type is inferrable and there are no (immediate) type clashes in the case of SDF, where the context is made of different types.
used constraint families to bind the "context" variable to something useful

Unfortunately it doesn't really work. Although it compiles and works with small examples, it is not scalable. Reasons:

I had to find a "sweet spot" between binding the contexts and zig-zagging them to somehow decouple the signal events' from the arguments' contexts.
if less contexts are bound then the compiler complains about "ambiguous types"
with all my decoupling effort there are still more or less obvious type clashes if we try to instantiate certain composition of processes. This mean that there are quite many restrictions on what compositions are possible
last but not least... the atoms type signatures are now ugly, and certainly non-intuitive.

Conclusion: event constructors with contexts are a bad, bad, bad, very bad idea! Terrible even!

Resolution (for now): implement two classes of atoms for timed and untimed MoCs, having the same names. This seems to be the only Haskell-accepted solution. This issue is a convincing reason to invest into developing an own language + type checker for ForSyDe.

ugeorge commented 8 years ago

It seems that there is one chance to make this work, using ghc-8's injective type families. Although hell breaks loose if I wrap FSVec inside a newtype (i.e. the Nat context is lost when I apply a function), it seems that things are a bit milder when I wrap Value instead.

newtype DEVal dummy a = Value a

instance MoC DE where
  type Arg DE c a = DEVal c a -- this is injective since c can be inferred from the result (unique)
  ...

instance MoC SDF where
  type Arg SDF c a = FSVec c a -- also result unique, thus type equation is injective
  ...

This means that there still are chances to design the Arg type family as closed. Of course, things will get a bit uglier since I now have to provide interfaces and unwrappers, but I hope that this can be hidden underneath applicative functors. The first tests proved to be encouraging.

forsyde / forsyde-atom

Covering untimed/SDF with the MoC class #5