Re: [Haskell-cafe] Type family signatures
Thank your for this elaborate explanation, you made my day! Thomas Ryan Ingram wrote: On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noorttho...@cs.ru.nl wrote: Somehow I didn't receive David's mail, but his explanation makes a lot of sense. I'm still wondering how this results in a type error involving rigid type variables. rigid type means the type has been specified by the programmer somehow. Desugaring your code a bit, we get: GADT :: forall a b. (b ~ Fam a) = a - b - GADT b Notice that this is an existential type that partially hides a; all we know about a after unwrapping this type is that (Fam a ~ b). unwrap :: forall a b. (b ~ Fam a) = GADT b - (a,b) unwrap (GADT x y) = (x,y) So, the type signature of unwrap fixes a and b to be supplied by the caller. Then the pattern match on GADT needs a type variable for the existential, so a new a1 is invented. These are rigid because they cannot be further refined by the typechecker; the typechecker cannot unify them with other types, like a1 ~ Int, or a1 ~ a. An example of a non-rigid variable occurs type-checking this expression: foo x = x + (1 :: Int) During type-checking/inference, there is a point where the type environment is: (+) :: forall a. Num a = a - a - a b :: *, non-rigid x :: b c :: *, non-rigid foo :: b - c Then (+) gets instantiated at Int and forces b and c to be Int. In your case, during the typechecking of unwrap, we have: unwrap :: forall a b. (b ~ Fam a) = GADT b - (a,b) a :: *, rigid b :: *, rigid (b ~ Fam a) -- From the pattern match on GADT: a1 :: *, rigid x :: a1 y :: b (b ~ Fam a1) Now the typechecker wants to unify a and a1, and it cannot, because they are rigid. If one of them was still open, we could unify it with the other. The type equalities give us (Fam a ~ Fam a1), but that does not give us (a ~ a1). If Fam was a data type or data family, we would know it is injective and be able to derive (a ~ a1), but it is a type family, so we are stuck. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Type family signatures
David is right that the program should be rejected. To be concrete, as he suggests, suppose type instance Fam Int = Bool type instance Fam Char = Bool Now suppose that 'unwrap' did typecheck. Then we could write: x :: Fam Int x = GADT 3 True y :: (Char, Bool) y = unwrap x Voila! We started with an Int (3), and managed to return it as the first component of a pair of type (Char,Bool). Ryan's explanation of the type checking process is accurate, but I agree that the error message is horrible. Dimitrios and I are working on a better version of the type checker that will say something more helpful, like Cannot deduce (a ~ a1) from (Fam a ~ Fam a1) which is a lot more useful. Nice example, thank you. Simon | -Original Message- | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe-boun...@haskell.org] On | Behalf Of Ryan Ingram | Sent: 18 August 2009 21:56 | To: Thomas van Noort | Cc: Haskell Cafe | Subject: Re: [Haskell-cafe] Type family signatures | | On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noorttho...@cs.ru.nl wrote: | Somehow I didn't receive David's mail, but his explanation makes a lot of | sense. I'm still wondering how this results in a type error involving rigid | type variables. | | rigid type means the type has been specified by the programmer somehow. | | Desugaring your code a bit, we get: | | GADT :: forall a b. (b ~ Fam a) = a - b - GADT b | | Notice that this is an existential type that partially hides a; all | we know about a after unwrapping this type is that (Fam a ~ b). | | unwrap :: forall a b. (b ~ Fam a) = GADT b - (a,b) | unwrap (GADT x y) = (x,y) | | So, the type signature of unwrap fixes a and b to be supplied by | the caller. Then the pattern match on GADT needs a type variable for | the existential, so a new a1 is invented. These are rigid because | they cannot be further refined by the typechecker; the typechecker | cannot unify them with other types, like a1 ~ Int, or a1 ~ a. | | An example of a non-rigid variable occurs type-checking this expression: | | foo x = x + (1 :: Int) | | During type-checking/inference, there is a point where the type environment is: | | (+) :: forall a. Num a = a - a - a | | b :: *, non-rigid | x :: b | | c :: *, non-rigid | foo :: b - c | | Then (+) gets instantiated at Int and forces b and c to be Int. | | In your case, during the typechecking of unwrap, we have: | | unwrap :: forall a b. (b ~ Fam a) = GADT b - (a,b) | a :: *, rigid | b :: *, rigid | (b ~ Fam a) | | -- From the pattern match on GADT: | a1 :: *, rigid | x :: a1 | y :: b | (b ~ Fam a1) | | Now the typechecker wants to unify a and a1, and it cannot, | because they are rigid. If one of them was still open, we could unify | it with the other. | | The type equalities give us (Fam a ~ Fam a1), but that does not give | us (a ~ a1). If Fam was a data type or data family, we would know it | is injective and be able to derive (a ~ a1), but it is a type family, | so we are stuck. | | -- ryan | ___ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family signatures
On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noorttho...@cs.ru.nl wrote: Somehow I didn't receive David's mail, but his explanation makes a lot of sense. I'm still wondering how this results in a type error involving rigid type variables. rigid type means the type has been specified by the programmer somehow. Desugaring your code a bit, we get: GADT :: forall a b. (b ~ Fam a) = a - b - GADT b Notice that this is an existential type that partially hides a; all we know about a after unwrapping this type is that (Fam a ~ b). unwrap :: forall a b. (b ~ Fam a) = GADT b - (a,b) unwrap (GADT x y) = (x,y) So, the type signature of unwrap fixes a and b to be supplied by the caller. Then the pattern match on GADT needs a type variable for the existential, so a new a1 is invented. These are rigid because they cannot be further refined by the typechecker; the typechecker cannot unify them with other types, like a1 ~ Int, or a1 ~ a. An example of a non-rigid variable occurs type-checking this expression: foo x = x + (1 :: Int) During type-checking/inference, there is a point where the type environment is: (+) :: forall a. Num a = a - a - a b :: *, non-rigid x :: b c :: *, non-rigid foo :: b - c Then (+) gets instantiated at Int and forces b and c to be Int. In your case, during the typechecking of unwrap, we have: unwrap :: forall a b. (b ~ Fam a) = GADT b - (a,b) a :: *, rigid b :: *, rigid (b ~ Fam a) -- From the pattern match on GADT: a1 :: *, rigid x :: a1 y :: b (b ~ Fam a1) Now the typechecker wants to unify a and a1, and it cannot, because they are rigid. If one of them was still open, we could unify it with the other. The type equalities give us (Fam a ~ Fam a1), but that does not give us (a ~ a1). If Fam was a data type or data family, we would know it is injective and be able to derive (a ~ a1), but it is a type family, so we are stuck. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family signatures
Somehow I didn't receive David's mail, but his explanation makes a lot of sense. I'm still wondering how this results in a type error involving rigid type variables. Ryan Ingram wrote: On Fri, Aug 14, 2009 at 12:03 PM, Dan Westonweston...@imageworks.com wrote: But presumably he can use a data family instead of a type family to restore injectivity, at the cost of adding an extra wrapped bottom value and one more layer of value constructor? Actually, you don't even necessarily pay this penalty, since you can put newtypes into data families. data family Foo a newtype instance Foo () = UnitFoo Int You do need to add the constructor wrap/unwrapping in code, but they all get erased after typechecking. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type family signatures
Hello, I have a question regarding type family signatures. Consider the following type family: type family Fam a :: * Then I define a GADT that takes such a value and wraps it: data GADT :: * - * where GADT :: a - Fam a - GADT (Fam a) and an accompanying unwrapper: unwrap :: GADT (Fam a) - (a, Fam a) unwrap (GADT x y) = (x, y) When Fam is declared using the first notation, type family Fam a :: * GHC HEAD gives the following error message: Main.hs:9:21: Couldn't match expected type `a' against inferred type `a1' `a' is a rigid type variable bound by the type signature for `unwrap' at Main.hs:8:20 `a1' is a rigid type variable bound by the constructor `GADT' at Main.hs:9:8 In the expression: x In the expression: (x, y) In the definition of `unwrap': unwrap (GADT x y) = (x, y) However, when Fam is declared as (moving the a to the other side of the :: and changing it into *), type family Fam :: * - * everything is ok. So, it seems to me that GHC HEAD considers both signatures to be really different. However, I do not quite understand the semantic difference in my example, other than that Fam needs to be fully satisfied in its named type arguments. Note that GHC 6.10.3 does not accept the latter signature for Fam since it requires at least one index for some reason, that's why I'm using GHC HEAD. Regards, Thomas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family signatures
On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noorttho...@cs.ru.nl wrote: Hello, I have a question regarding type family signatures. Consider the following type family: type family Fam a :: * Then I define a GADT that takes such a value and wraps it: data GADT :: * - * where GADT :: a - Fam a - GADT (Fam a) and an accompanying unwrapper: unwrap :: GADT (Fam a) - (a, Fam a) unwrap (GADT x y) = (x, y) When Fam is declared using the first notation, type family Fam a :: * GHC HEAD gives the following error message: Main.hs:9:21: Couldn't match expected type `a' against inferred type `a1' `a' is a rigid type variable bound by the type signature for `unwrap' at Main.hs:8:20 `a1' is a rigid type variable bound by the constructor `GADT' at Main.hs:9:8 In the expression: x In the expression: (x, y) In the definition of `unwrap': unwrap (GADT x y) = (x, y) This is because type families are not injective. Nothing stops you from defining two instances such as, type instance Fam Int = Bool type instance Fam Char = Bool in which case a value of type GADT Bool is ambiguous. Does it contain an Int or a Char? However, when Fam is declared as (moving the a to the other side of the :: and changing it into *), type family Fam :: * - * everything is ok. So, it seems to me that GHC HEAD considers both signatures to be really different. However, I do not quite understand the semantic difference in my example, other than that Fam needs to be fully satisfied in its named type arguments. Note that GHC 6.10.3 does not accept the latter signature for Fam since it requires at least one index for some reason, that's why I'm using GHC HEAD. A type family with no index is equivalent to a type synonym. But in answer to your question, these signatures are very different. Consider these families. type family Foo a b :: * type family Bar a :: * - * Foo is indexed by two parameters, but Bar is only indexed by one. type instance Foo A B = X type instance Foo A C = X -- Foo a b ~ Foo a c does not imply b ~ c type instance Bar A = [] -- Bar a b ~ Bar a c does imply b ~ c Bar returns a type constructor, so it can be used anywhere a type constructor of kind * - * can be used. foo :: (Functor (Foo a)) = ... -- invalid bar :: (Functor (Bar a)) = ... -- valid -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family signatures
But presumably he can use a data family instead of a type family to restore injectivity, at the cost of adding an extra wrapped bottom value and one more layer of value constructor? David Menendez wrote: On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noorttho...@cs.ru.nl wrote: Hello, I have a question regarding type family signatures. Consider the following type family: type family Fam a :: * Then I define a GADT that takes such a value and wraps it: data GADT :: * - * where GADT :: a - Fam a - GADT (Fam a) and an accompanying unwrapper: unwrap :: GADT (Fam a) - (a, Fam a) unwrap (GADT x y) = (x, y) When Fam is declared using the first notation, type family Fam a :: * GHC HEAD gives the following error message: Main.hs:9:21: Couldn't match expected type `a' against inferred type `a1' `a' is a rigid type variable bound by the type signature for `unwrap' at Main.hs:8:20 `a1' is a rigid type variable bound by the constructor `GADT' at Main.hs:9:8 In the expression: x In the expression: (x, y) In the definition of `unwrap': unwrap (GADT x y) = (x, y) This is because type families are not injective. Nothing stops you from defining two instances such as, type instance Fam Int = Bool type instance Fam Char = Bool in which case a value of type GADT Bool is ambiguous. Does it contain an Int or a Char? However, when Fam is declared as (moving the a to the other side of the :: and changing it into *), type family Fam :: * - * everything is ok. So, it seems to me that GHC HEAD considers both signatures to be really different. However, I do not quite understand the semantic difference in my example, other than that Fam needs to be fully satisfied in its named type arguments. Note that GHC 6.10.3 does not accept the latter signature for Fam since it requires at least one index for some reason, that's why I'm using GHC HEAD. A type family with no index is equivalent to a type synonym. But in answer to your question, these signatures are very different. Consider these families. type family Foo a b :: * type family Bar a :: * - * Foo is indexed by two parameters, but Bar is only indexed by one. type instance Foo A B = X type instance Foo A C = X -- Foo a b ~ Foo a c does not imply b ~ c type instance Bar A = [] -- Bar a b ~ Bar a c does imply b ~ c Bar returns a type constructor, so it can be used anywhere a type constructor of kind * - * can be used. foo :: (Functor (Foo a)) = ... -- invalid bar :: (Functor (Bar a)) = ... -- valid ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family signatures
On Fri, Aug 14, 2009 at 12:03 PM, Dan Westonweston...@imageworks.com wrote: But presumably he can use a data family instead of a type family to restore injectivity, at the cost of adding an extra wrapped bottom value and one more layer of value constructor? Actually, you don't even necessarily pay this penalty, since you can put newtypes into data families. data family Foo a newtype instance Foo () = UnitFoo Int You do need to add the constructor wrap/unwrapping in code, but they all get erased after typechecking. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
