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 possibilit
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 w
> 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 =
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
> >
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@ha
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 :: DBoo
