[<<][compsci][>>][..]

Thu Feb 18 08:10:18 CET 2010

## Generalized Algebraic Data Type (GADT)

From WikiPedia[2]:
... the parameters of the return type of a data constructor can be
freely chosen when declaring the constructor, while for algebraic
data types in Haskell 98, the type parameter of the return value
is inferred from data types of parameters;
From HaskellWiki[3]:
Generalised Algebraic Datatypes (GADTs) are datatypes for which a
constructor has a non standard type.
and [4] explains it in mortal:
why Haskell don't yet supports full-featured type functions? Hold
your breath... Haskell already contains them and at least GHC
implements all the mentioned abilities more than 10 years ago!
They just was named... TYPE CLASSES!
Together with the multiparam typeclass extension this gives a way to
represent quite powerful type functions.
(for "data" constructs) Lack of pattern matching means that left
side can contain only free type variables, that in turn means that
left sides of all "data" statements for one type will be
essentially the same. Therefore, repeated left sides in
multi-statement "data" definitions are omitted and instead of
data Either a b = Left a
Either a b = Right b
we write just
data Either a b = Left a
| Right b
... And here finally comes the GADTs! It's just a way to define
data types using pattern matching and constants on the left side
of "data" statements! How about this:
data T String = D1 Int
T Bool = D2
T [a] = D3 (a,a)
Amazed? After all, GADTs seems really very simple and obvious
extension to data type definition facilities.
It seems the main trick that GADTs facilitate is to replace
constructor tag matching for sum types with type-level pattern
matching. This moves information from run-time to compile time and so
can provide more safety.
[1] http://lambda-the-ultimate.org/node/1293
[2] http://en.wikipedia.org/wiki/Generalized_algebraic_data_type
[3] http://www.haskell.org/haskellwiki/GADT
[4] http://www.haskell.org/haskellwiki/GADTs_for_dummies

[Reply][About]

[<<][compsci][>>][..]