[Haskell-cafe] pattern matching on data families constructors

[Roman Cheplyaka]

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 <electreg at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe