interaction of GADTs and data families: a bug?
Dear GHC experts, Certain behaviour when using {-# LANGUAGE GADTs, TypeFamilies #-} surprises me. The following is accepted by GHC 6.12.1: data GADT a where BoolGADT :: GADT Bool foo :: GADT a -> a -> Int foo BoolGADT True = 42 But the following is not: data family DataFam a data instance DataFam Bool where BoolDataFam :: DataFam Bool fffuuuu :: DataFam a -> a -> Int fffuuuu BoolDataFam True = 42 GHC 6.12.1 throws the following error (GHC 6.10.4 panics): Couldn't match expected type `a' against inferred type `Bool' `a' is a rigid type variable bound by the type signature for `fffuuuu' at gadtDataFam.hs:13:19 In the pattern: BoolDataFam In the definition of `fffuuuu': fffuuuu BoolDataFam True = 42 I expect that `fffuuuu` should be accepted just like `foo`. Do I expect too much? Cheers, Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Hi Sebastian, Is this perhaps another instance of #3851? http://hackage.haskell.org/trac/ghc/ticket/3851 Cheers, Pedro On Thu, Apr 15, 2010 at 14:10, Sebastian Fischer < sebf@informatik.uni-kiel.de> wrote:
Dear GHC experts,
Certain behaviour when using
{-# LANGUAGE GADTs, TypeFamilies #-}
surprises me. The following is accepted by GHC 6.12.1:
data GADT a where BoolGADT :: GADT Bool
foo :: GADT a -> a -> Int foo BoolGADT True = 42
But the following is not:
data family DataFam a data instance DataFam Bool where BoolDataFam :: DataFam Bool
fffuuuu :: DataFam a -> a -> Int fffuuuu BoolDataFam True = 42
GHC 6.12.1 throws the following error (GHC 6.10.4 panics):
Couldn't match expected type `a' against inferred type `Bool' `a' is a rigid type variable bound by the type signature for `fffuuuu' at gadtDataFam.hs:13:19 In the pattern: BoolDataFam In the definition of `fffuuuu': fffuuuu BoolDataFam True = 42
I expect that `fffuuuu` should be accepted just like `foo`. Do I expect too much?
Cheers, Sebastian
-- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Is this perhaps another instance of #3851? http://hackage.haskell.org/trac/ghc/ticket/3851
Honestly: I don't know. My example is different from the one shown in #3851 in that it also does not work in GHC 6.10 (which even panics instead of giving the error 6.12 gives) and in that it uses a data family, not a type family. Whether or not it is the same "awkward interaction" that causes this behaviour is beyond my expertise. Cheers, Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Hi Sebastian, On Thu, Apr 15, 2010 at 15:08, Sebastian Fischer < sebf@informatik.uni-kiel.de> wrote:
Is this perhaps another instance of #3851? http://hackage.haskell.org/trac/ghc/ticket/3851
Honestly: I don't know.
My example is different from the one shown in #3851 in that it also does not work in GHC 6.10 (which even panics instead of giving the error 6.12 gives) and in that it uses a data family, not a type family.
The example in the ticket uses type families, but later in the comments I show an example with data families which fails on both 6.10.4 and 6.12.1. Cheers, Pedro
Whether or not it is the same "awkward interaction" that causes this behaviour is beyond my expertise.
Cheers, Sebastian
-- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
but later in the comments I show an example with data families which fails on both 6.10.4 and 6.12.1.
Ah, I think I misinterpreted your comment, when I read it for the first time. Thanks for pointing me at it again. But I still don't see whether or not the two examples are related. At least the error is different. Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Sebastian Fischer wrote:
Dear GHC experts,
Certain behaviour when using
{-# LANGUAGE GADTs, TypeFamilies #-}
surprises me. The following is accepted by GHC 6.12.1:
data GADT a where BoolGADT :: GADT Bool
foo :: GADT a -> a -> Int foo BoolGADT True = 42
But the following is not:
data family DataFam a data instance DataFam Bool where BoolDataFam :: DataFam Bool
fffuuuu :: DataFam a -> a -> Int fffuuuu BoolDataFam True = 42
GHC 6.12.1 throws the following error (GHC 6.10.4 panics):
Couldn't match expected type `a' against inferred type `Bool' `a' is a rigid type variable bound by the type signature for `fffuuuu' at gadtDataFam.hs:13:19 In the pattern: BoolDataFam In the definition of `fffuuuu': fffuuuu BoolDataFam True = 42
I expect that `fffuuuu` should be accepted just like `foo`. Do I expect too much?
I think you expect too much. You just don't get type refinement with type or data families. The function you wrote is similar to this code that doesn't use families at all: fffuuu :: Maybe a -> a -> Int fffuuu (Just True) True = 42 and we wouldn't expect that to work because Haskell in general doesn't have the runtime type match that would be required to handle it. With GADTs, the specific choice of constructor is what gives you the type matching functionality. Cheers, Ganesh =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================
With GADTs, the specific choice of constructor is what gives you the type matching functionality.
My intention was to use a GADT as data family instance (hence, I wrote it in GADT style and it was accepted as such). Can't GADTs be used as data family instances? Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Sebastian Fischer wrote:
With GADTs, the specific choice of constructor is what gives you the type matching functionality.
My intention was to use a GADT as data family instance (hence, I wrote it in GADT style and it was accepted as such). Can't GADTs be used as data family instances?
I'm not aware of any restriction there, but that's not the issue here. You were trying to choose between different top-level types (which happen to be instances of the same family) by their constructors. GADTs allow you to choose between different constructors of the *same* top-level type. If DataFam Bool had multiple constructors, you could choose between them in fffuuuu. But fffuuuu would have to have type DataFam Bool -> Bool -> Int (as is necessary with your originally posted code). Ganesh =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================
On Apr 15, 2010, at 3:44 PM, Sittampalam, Ganesh wrote:
You were trying to choose between different top-level types (which happen to be instances of the same family) by their constructors.
That is true. I was trying to emulate an open data type such that I can write -- does not work fffuuuu :: DataFam a -> a -> Int fffuuuu BoolDataFam True = 42 fffuuuu CharDataFam 'c' = 43 But apparently such thing is only possible with a (closed) GADT: data GADT a where BoolGADT :: GADT Bool CharGADT :: GADT Char -- does work foo :: GADT a -> a -> Int foo BoolGADT True = 42 foo CharGADT 'c' = 43 I was hoping to achieve the same without having a single closed type. On Apr 15, 2010, at 3:29 PM, Dan Doel wrote:
DataFam Bool is not a GADT, it's an ADT written with GADT syntax.
Yes, that was the main source of my confusion. Thank you both for clarifying! Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
| > My intention was to use a GADT as data family instance (hence, I | > wrote it in GADT style and it was accepted as such). Can't GADTs be | > used as data family instances? | | I'm not aware of any restriction there, but that's not the issue here. | | You were trying to choose between different top-level types (which | happen to be instances of the same family) by their constructors. GADTs | allow you to choose between different constructors of the *same* | top-level type. | | If DataFam Bool had multiple constructors, you could choose between them | in fffuuuu. But fffuuuu would have to have type DataFam Bool -> Bool -> | Int (as is necessary with your originally posted code). Ganesh and Dan are exactly right. You can certainly have a data family instance that it itself a GADT: data family T a b data instance T Int b where Foo :: T Int Bool Bar :: T Int Char data instance T Char b where .... And indeed matching on a (T Int b) can refine the b: f :: T Int b -> b f Foo = True f Bra = 'c' But (T Int b) and (T Char b) are distinct data types, and do not share constructors. Simon
On Thursday 15 April 2010 8:10:42 am Sebastian Fischer wrote:
Dear GHC experts,
Certain behaviour when using
{-# LANGUAGE GADTs, TypeFamilies #-}
surprises me. The following is accepted by GHC 6.12.1:
data GADT a where BoolGADT :: GADT Bool
foo :: GADT a -> a -> Int foo BoolGADT True = 42
But the following is not:
data family DataFam a data instance DataFam Bool where BoolDataFam :: DataFam Bool
fffuuuu :: DataFam a -> a -> Int fffuuuu BoolDataFam True = 42
GHC 6.12.1 throws the following error (GHC 6.10.4 panics):
Couldn't match expected type `a' against inferred type `Bool' `a' is a rigid type variable bound by the type signature for `fffuuuu' at gadtDataFam.hs:13:19 In the pattern: BoolDataFam In the definition of `fffuuuu': fffuuuu BoolDataFam True = 42
I expect that `fffuuuu` should be accepted just like `foo`. Do I expect too much?
I don't really see how your example could be expected to work. I can only conclude that DataFam Bool is not a GADT, it's an ADT written with GADT syntax. Data/type families allow for definition of a family of types by case analysis on one or more indices. To define functions polymorphic in those indices, one must first do case analysis on those indices (via classes or a separate GADT parameter), or work at a specific index. Presumably one can do the following: data family Fam a :: * -> * data instance Fam Bool :: * -> * where BoolInt :: Fam Bool Int where Fam Bool a is itself a GADT with index a. But we can also write an instance: data instance Fam Int a = CInt a a which can also be written: data instance Fam Int a where CInt :: a -> a -> Fam Int a but the specificity of Int comes not from CInt being a GADT constructor, but because we are specifying what the type Fam Int is. And we cannot expect to define a function: foo :: Fam a b -> Int foo (CInt x y) = 32 foo BoolInt = 42 simply because type/data families do not work that way. The index of the family needs to be known before we can know which constructors we are able to match against. We could, however, write: foo :: Fam Bool b -> b foo BoolInt = 42 which shows that once we know that we are working with Fam Bool b, matching can refine b. I haven't used this feature yet, so perhaps an expert will correct me. But that is my interpretation of the situation. -- Dan
participants (5)
-
Dan Doel -
José Pedro Magalhães -
Sebastian Fischer -
Simon Peyton-Jones -
Sittampalam, Ganesh