interaction of GADTs and data families: a bug?
Sebastian Fischer
sebf at informatik.uni-kiel.de
Thu Apr 15 10:04:34 EDT 2010
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.)
More information about the Glasgow-haskell-users
mailing list