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