Problems with type families
Hi All! Consider the following definitions: type family TFunIn t e type family TFunOut t e data IdT data ComposeT t1 t2 -- etc... type instance TFunIn (ComposeT t1 t2) e = TFunIn t2 e type instance TFunOut (ComposeT t1 t2) e = TFunOut t1 e -- etc... class SignalT t e where transform :: t -> TFunIn t e -> TFunOut t e instance (SignalT t1 e, SignalT t2 e) => SignalT (ComposeT t1 t2) e where transform _ x = (transform (undefined :: t1) . transform (undefined :: t2)) x Due to the `TFunIn` and `TFunOut` type families instances for [(ComposeT t1 t2) e], the `transform` function for [(ComposeT t1 t2) e] instance of SignalT should be inferred as: transform :: t -> TFunIn (ComposeT t1 t2) e -> TFunOut (ComposeT t1 t2) e <==> :: t -> TFunIn t2 e -> TFunOut t1 e But I cannot figure out why it does not compile. Any ideas? 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
On 07/06/2015 01:20 PM, Leza Morais Lutonda wrote:
instance (SignalT t1 e, SignalT t2 e) => SignalT (ComposeT t1 t2) e where transform _ x = (transform (undefined :: t1) . transform (undefined :: t2)) x Sorry for a typo:
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 but still not compile. -- Leza Morais Lutonda, Lemol-C Electronic and Telecommunication Engineer Software Development and Architecture Enthusiast http://lemol.github.io 50 Aniversario de la Cujae. Inaugurada por Fidel el 2 de diciembre de 1964 http://cujae.edu.cu
What's the error message? Is a bit hard without that. The problem is probably that you have to explicitly state everything. Maybe TFunIn (ComposeT t1 t2) e ~ TFunOut (SignalT t2 e) The problem with typefamilies is that often things can not be used as you would expect unless you state things explicitly. It is because the instance declaration can not know that TFunIn is always the same. You could import two different ones from different modules and thus convert one type into another. closed typefamilies can sometimes help too. Silvio
Hi Silvio, thanks for the answer.
What's the error message? Is a bit hard without that.
The error message is: (the source code is attached) src/DSP/Sig.hs:41:25: Could not deduce (TFunOut t1 e ~ TFunOut t1 e0) from the context (SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e) bound by the instance declaration at src/DSP/Sig.hs:39:10-95 NB: ‘TFunOut’ is a type function, and may not be injective The type variable ‘e0’ is ambiguous Expected type: TFunOut (ComposeT t1 t2) e Actual type: TFunOut t1 e0 Relevant bindings include x :: TFunIn (ComposeT t1 t2) e (bound at src/DSP/Sig.hs:41:21) transform :: ComposeT t1 t2 -> TFunIn (ComposeT t1 t2) e -> TFunOut (ComposeT t1 t2) e (bound at src/DSP/Sig.hs:41:9) In the expression: (transform (undefined :: t1) . transform (undefined :: t2)) x In an equation for ‘transform’: transform _ x = (transform (undefined :: t1) . transform (undefined :: t2)) x src/DSP/Sig.hs:41:26: Could not deduce (TFunIn t1 e0 ~ TFunOut t2 e1) from the context (SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e) bound by the instance declaration at src/DSP/Sig.hs:39:10-95 The type variables ‘e0’, ‘e1’ are ambiguous Expected type: TFunOut t2 e1 -> TFunOut t1 e0 Actual type: TFunIn t1 e0 -> TFunOut t1 e0 Relevant bindings include x :: TFunIn (ComposeT t1 t2) e (bound at src/DSP/Sig.hs:41:21) transform :: ComposeT t1 t2 -> TFunIn (ComposeT t1 t2) e -> TFunOut (ComposeT t1 t2) e (bound at src/DSP/Sig.hs:41:9) In the first argument of ‘(.)’, namely ‘transform (undefined :: t1)’ In the expression: transform (undefined :: t1) . transform (undefined :: t2) src/DSP/Sig.hs:41:56: Could not deduce (TFunIn t2 e1 ~ TFunIn t2 e) from the context (SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e) bound by the instance declaration at src/DSP/Sig.hs:39:10-95 NB: ‘TFunIn’ is a type function, and may not be injective The type variable ‘e1’ is ambiguous Expected type: TFunIn t2 e -> TFunOut t2 e1 Actual type: TFunIn t2 e1 -> TFunOut t2 e1 Relevant bindings include x :: TFunIn (ComposeT t1 t2) e (bound at src/DSP/Sig.hs:41:21) transform :: ComposeT t1 t2 -> TFunIn (ComposeT t1 t2) e -> TFunOut (ComposeT t1 t2) e (bound at src/DSP/Sig.hs:41:9) In the second argument of ‘(.)’, namely ‘transform (undefined :: t2)’ In the expression: transform (undefined :: t1) . transform (undefined :: t2) Failed, modules loaded: none.
The problem is probably that you have to explicitly state everything.
Maybe
TFunIn (ComposeT t1 t2) e ~ TFunOut (SignalT t2 e)
The problem with typefamilies is that often things can not be used as you would expect unless you state things explicitly.
It is because the instance declaration can not know that TFunIn is always the same. You could import two different ones from different modules and thus convert one type into another.
closed typefamilies can sometimes help too.
-- Leza Morais Lutonda, Lemol-C Electronic and Telecommunication Engineer Software Development and Architecture Enthusiast http://lemol.github.io 50 Aniversario de la Cujae. Inaugurada por Fidel el 2 de diciembre de 1964 http://cujae.edu.cu
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
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
type instance TFunIn DoubleT e = (Signal e, Signal e)
I give up. I'm not sure it's possible to tell to the compiler that when using transform function (the IdT version in the implementation of ComposeT) that it should use the one with the same e. Not sure it's possible. Anyway a workaround would be. class SignalT t e where transform :: e -> t -> TFunIn t e -> TFunOut t e instance ( SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e ) => SignalT (ComposeT t1 t2) e where transform _ _ x = (transform (undefined :: e) (undefined :: t1)) (transform (undefined :: e) (undefined :: t2)) (x :: TFunIn (ComposeT t1 t2) e) But you could save your self a lot of hurt by just using newtype DoubleSignal a = DoubleSignal (Signal a, Signal a) you could even remove the e from the SignalT class. Silvio
On 07/08/2015 11:30 PM, Silvio Frischknecht wrote:
Anyway a workaround would be.
class SignalT t e where transform :: e -> t -> TFunIn t e -> TFunOut t e
instance ( SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e ) => SignalT (ComposeT t1 t2) e where transform _ _ x = (transform (undefined :: e) (undefined :: t1)) (transform (undefined :: e) (undefined :: t2)) (x :: TFunIn (ComposeT t1 t2) e)
I got it! This solution is nice for me, and helped me to understand how to tell the compiler about the `e` type. Thank you Silvio! -- 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
participants (2)
-
Leza Morais Lutonda -
Silvio Frischknecht