[Haskell-cafe] pattern matching on data families constructors
Hi, suppose that there is following data family: data family D a data instance D Int = DInt Int data instance D Bool = DBool Bool it is not possible to match on constructors from different instances: -- type error a :: D a - a a (DInt x) = x a (DBool x) = x however, following works: data G :: * - * where GInt :: G Int GBool :: G Bool b :: G a - D a - a b GInt (DInt x) = x b GBool (DBool x) = x The reason why second example works is equality constraints (a ~ Int) and (a ~ Bool) introduced by GADT's constructors, I suppose. I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching? Thanks.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pattern matching on data families constructors
At Thu, 25 Apr 2013 20:29:16 +0400, Alexey Egorov wrote: I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching? I think you are misunderstanding what data families do. ‘DInt :: DInt - D Int’ and ‘DBool :: DBool - D Bool’ are two data constructors for *different* data types (namely, ‘D Int’ and ‘D Bool’). The type family ‘D :: * - *’ relates types to said distinct data types. On the other hand the type constructor ‘D :: * - *’ parametrises a *single* data type over another type—the fact that the parameter can be constrained depending on the data constructor doesn’t really matter here. Would you expect this to work? newtype DInt a = DInt a newtype DBool a = DBool a type family D a type instance D Int = DInt Int type instance D Bool = DBool Bool a :: D a - a a (DInt x) = x a (DBool x) = x Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pattern matching on data families constructors
At Thu, 25 Apr 2013 19:08:17 +0100, Francesco Mazzoli wrote: ... ‘DInt :: DInt - D Int’ and ‘DBool :: DBool - D Bool’ ... This should read ‘DInt :: Int - D Int’ and ‘DBool :: Bool - D Bool’. Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pattern matching on data families constructors
At Thu, 25 Apr 2013 19:08:17 +0100, Francesco Mazzoli wrote: Would you expect this to work? newtype DInt a = DInt a newtype DBool a = DBool a type family D a type instance D Int = DInt Int type instance D Bool = DBool Bool a :: D a - a a (DInt x) = x a (DBool x) = x Or even better: data family D a data instance D Int = DInt1 Int | DInt2 Int data instance D Bool = DBool Bool a :: D a - a a (DInt1 x) = x a (DInt2 x) = x a (DBool x) = x Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pattern matching on data families constructors
Would you expect this to work?
newtype DInt a = DInt a
newtype DBool a = DBool a
type family D a
type instance D Int = DInt Int
type instance D Bool = DBool Bool
a :: D a - a
a (DInt x) = x
a (DBool x) = x
Or even better:
data family D a
data instance D Int = DInt1 Int | DInt2 Int
data instance D Bool = DBool Bool
a :: D a - a
a (DInt1 x) = x
a (DInt2 x) = x
a (DBool x) = x
Yes, my question is about why different instances are different types even if
they have the same type constructor (D).
I'm just find it confusing that using GADTs trick it is possible to match on
different constructors.
Another confusing thing is that following works:
data G :: * - * where
{ GInt :: G Int
; GBool :: G Bool }
b :: G a - D a - a
b GInt (DInt x) = x
b GBool (DBool x) = x
while quite similar doesn't:
c :: D a - G a - a
c (DInt x) GInt = x
c (DBool x) GBool = x
However, viewing data families as type families + per-instance newtype/data
declaration is helpful, thank you.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pattern matching on data families constructors
At Fri, 26 Apr 2013 00:20:36 +0400, Alexey Egorov wrote: Yes, my question is about why different instances are different types even if they have the same type constructor (D). I'm just find it confusing that using GADTs trick it is possible to match on different constructors. See it this way: the two ‘D’s (the GADTs and the data family one) are both type functions, taking a type and giving you back another type. In standard Haskell all such type functions return instances of the same data type (with a set of data constructors you can pattern match on), much like the ‘D’ of the GADTs. With type/data families the situation changes, and the returned type can be different depending on the provided type, which is what’s happening here. Now the thing you want to do is ultimately write your ‘a’, which as you said relies on type coercions, but this fact (the ‘GADTs trick’) has nothing to do with the fact that type families will relate types to different data types. Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pattern matching on data families constructors
Let's look at it from the operational perspective. In the GADT case, the set of possibilities is fixed in advance (closed). Every GADT constructor has a corresponding tag (a small integer) which, when pattern-matching, tells us which branch to take. In the data family case, the set of possibilities is open. It is harder to do robust tagging over all the instances, given that new instances can be added after the module is compiled. The right way to do what you want is to use a type class and associate your data family with that class: class C a where data D a a :: D a - a instance C Int where data D Int = DInt Int a (DInt x) = x instance C Bool where data D Bool = DBool Bool a (DBool x) = x Roman * Alexey Egorov elect...@list.ru [2013-04-25 20:29:16+0400] Hi, suppose that there is following data family: data family D a data instance D Int = DInt Int data instance D Bool = DBool Bool it is not possible to match on constructors from different instances: -- type error a :: D a - a a (DInt x) = x a (DBool x) = x however, following works: data G :: * - * where GInt :: G Int GBool :: G Bool b :: G a - D a - a b GInt (DInt x) = x b GBool (DBool x) = x The reason why second example works is equality constraints (a ~ Int) and (a ~ Bool) introduced by GADT's constructors, I suppose. I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching? Thanks. ___ 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
