GADTSyntax extension allows you to write data declarations in such a way that the types of the constructors are made more obvious.
The name “GADT syntax” comes from the fact that this syntax is necessary when defining GADTs, or generalized algebraic datatypes, but you don’t need to worry about what GADTs are to use the syntax. The
GADTs extension implies the
GADTSyntax extension; that is, enabling
GADTSyntax on as well, but the opposite is not true. When
GADTSyntax is enabled but not
GADTs, then some features of GADTs are not enabled. We will not concern ourselves with those features in this article.
The extensionGHC documentation for
GADTSyntax was introducedGADTs (and thus GADT syntax) existed as early as GHC 6.4, but
GADTSyntax was not a separate extension at first. in GHC 7.2.1 and is available in all subsequent GHC releases.
Here is the standard definition of
A constructor has a type, just like any other value in Haskell. We can see this in the REPL using the
λ> :type Nothing Nothing :: Maybe a λ> :type Just Just :: a -> Maybe a
With GADT syntax, we define a type by explicitly writing the type signature for each of its constructors.
This definition of
Maybe has exactly the same meaning as the one above.
This is why we sometimes use this extension for teaching and learning purposes. It is important to understanding Haskell to understand data constructors as functions. Sometimes, as with
Nothing or the Boolean values
False, they are nullary functions. However, writing our data declaration this way still allows us to notice that
Nothing, unlike those Boolean values, is still parameterized by the type variable
a. That isn’t visible in the
Nothing value at term-level, and we believe it is less obvious when written in standard data declaration syntax (even though the meaning of that and this are identical).
Any data declaration that can be written in standard Haskell98 style can be written with GADT syntax.
For example, you could define a heterogeneous pair type resembling a two-tuple.
Note that the
Tuple constructor and the
(,) constructor then have the same type, albeit without the special syntax.
λ> :type Tuple Tuple :: a -> b -> Tuple a b λ> :type (,) (,) :: a -> b -> (a, b)
You can also use this syntax to define record types. For example, consider this ordinary
The same type written with GADT syntax looks like this (we’ll give it slightly different names so we can have both in scope at once without them clashing):
Just to demonstrate to ourselves that these behave the same way, let’s do a few experiments in our REPL.
The constructors have the same type:
λ> :type Person Person :: String -> Int -> Person λ> :type Person' Person' :: String -> Int -> Person'
And the field accessor functions work just the same:
λ> alonzo = Person "Alonzo" 7 alonzo :: Person λ> name alonzo "Alonzo" λ> age alonzo 7 λ> melman = Person' "Melman" 5 melman :: Person' λ> name' melman "Melman" λ> age' melman 5
There are many more powerful things you can do with GADTs themselves, but this extension only enables the syntax without enabling those other things, so as you become a more experienced Haskeller, you will probably not have much cause to use this extension. But, again, we sometimes find the explicitness of writing the constructors this way helpful when learning, and starting here is also a reasonable gateway to GADTs themselves because you grow accustomed to the funky syntax.