Haskell Language Generalized Algebraic Data Types Basic Usage
Example
When the GADTs extension is enabled, besides regular data declarations, you can also declare generalized algebraic datatypes as follows:
data DataType a where
Constr1 :: Int -> a -> Foo a -> DataType a
Constr2 :: Show a => a -> DataType a
Constr3 :: DataType Int
A GADT declaration lists the types of all constructors a datatype has, explicitly. Unlike regular datatype declarations, the type of a constructor can be any N-ary (including nullary) function that ultimately results in the datatype applied to some arguments.
In this case we've declared that the type DataType has three constructors: Constr1, Constr2 and Constr3.
The Constr1 constructor is no different from one declared using a regular data declaration: data DataType a = Constr1 Int a (Foo a) | ...
Constr2 however requires that a has an instance of Show, and so when using the constructor the instance would need to exist. On the other hand, when pattern-matching on it, the fact that a is an instance of Show comes into scope, so you can write:
foo :: DataType a -> String
foo val = case val of
Constr2 x -> show x
...
Note that the Show a constraint doesn't appear in the type of the function, and is only visible in the code to the right of ->.
Constr3 has type DataType Int, which means that whenever a value of type DataType a is a Constr3, it is known that a ~ Int. This information, too, can be recovered with a pattern match.
