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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort<[hidden email]> 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 <[hidden email]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 Noort<[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Fri, Aug 14, 2009 at 12:03 PM, Dan Weston<[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 Weston<[hidden email]> 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 Noort<[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Ryan Ingram
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: [hidden email] [mailto:[hidden email]] 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 Noort<[hidden email]> 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 | [hidden email] | http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |