[Haskell-cafe] Problems with type families

[Leza Morais Lutonda]

On 07/06/2015 07:29 PM, Silvio Frischknecht wrote:
> looks like the problem are the 'e's. you can see it from
>
> Could not deduce (TFunOut t1 e ~ TFunOut t1 e0)
>
> the e0 comes from the output of TFunIn/TFunOut and the instance does not
> know that it is the same as the e variable you use.
>
> I don't know exactly what your program does. but if e is just a
> phantom/security parameter you can do it like this.
>
> type family TFunIn t :: * -> *
>
> type instance TFunIn  IdT = Signal
>
> type instance TFunIn  (ComposeT t1 t2) = TFunIn  t2
>
> instance (SignalT t1 e, SignalT t2 e, TFunOut t2 ~ TFunIn t1)
>      => SignalT (ComposeT t1 t2) e where
>          transform _ x = (transform (undefined :: t1) .
>                           transform (undefined :: t2)) x
>
>
> Otherwise you will have to find a way to prove that the 'e's are the same
>
> Cheers Silvio
>
Hi Silvio,

The `e` type is important. The problem with not including `e` in the 
`TFunIn` is that I will want to define:

type instance TFunIn DoubleT e = (Signal e, Signal e)

which I cannot express without specifying the `e` type parameter.

And it cannot be a closed type family. So what can I prove that the `e`s 
are the same?
The intuition I get from the instance declaration is that "they/it" are 
the same:

instance (SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e) => SignalT (ComposeT t1 t2) e
     where
         transform _ x = (transform (undefined :: t1) . transform (undefined :: t2)) x


Thanks.

-- 
Leza Morais Lutonda, Lemol-C
http://lemol.github.io



50 Aniversario de la Cujae. Inaugurada por Fidel el 2 de diciembre de 1964  http://cujae.edu.cu