-</sect2>
-
-</sect1>
-<!-- ==================== End of type system extensions ================= -->
-
-<!-- ====================== Generalised algebraic data types ======================= -->
-
-<sect1 id="gadt">
-<title>Generalised Algebraic Data Types</title>
-
-<para>Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you
-to give the type signatures of constructors explicitly. For example:
-<programlisting>
- data Term a where
- Lit :: Int -> Term Int
- Succ :: Term Int -> Term Int
- IsZero :: Term Int -> Term Bool
- If :: Term Bool -> Term a -> Term a -> Term a
- Pair :: Term a -> Term b -> Term (a,b)
-</programlisting>
-Notice that the return type of the constructors is not always <literal>Term a</literal>, as is the
-case with ordinary vanilla data types. Now we can write a well-typed <literal>eval</literal> function
-for these <literal>Terms</literal>:
-<programlisting>
- eval :: Term a -> a
- eval (Lit i) = i
- eval (Succ t) = 1 + eval t
- eval (IsZero t) = eval t == 0
- eval (If b e1 e2) = if eval b then eval e1 else eval e2
- eval (Pair e1 e2) = (eval e1, eval e2)
-</programlisting>
-These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
-</para>
-<para> The extensions to GHC are these:
-<itemizedlist>
-<listitem><para>
- Data type declarations have a 'where' form, as exemplified above. The type signature of
-each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal
-Haskell data type declaration, the type variable(s) in the "<literal>data Term a where</literal>" header
-have no scope. Indeed, one can write a kind signature instead:
-<programlisting>
- data Term :: * -> * where ...
-</programlisting>
-or even a mixture of the two:
-<programlisting>
- data Foo a :: (* -> *) -> * where ...
-</programlisting>
-The type variables (if given) may be explicitly kinded, so we could also write the header for <literal>Foo</literal>
-like this:
-<programlisting>
- data Foo a (b :: * -> *) where ...
-</programlisting>
-</para></listitem>
-
-<listitem><para>
-There are no restrictions on the type of the data constructor, except that the result
-type must begin with the type constructor being defined. For example, in the <literal>Term</literal> data
-type above, the type of each constructor must end with <literal> ... -> Term ...</literal>.
-</para></listitem>
-
-<listitem><para>
-You can use record syntax on a GADT-style data type declaration:
-
-<programlisting>
- data Term a where
- Lit { val :: Int } :: Term Int
- Succ { num :: Term Int } :: Term Int
- Pred { num :: Term Int } :: Term Int
- IsZero { arg :: Term Int } :: Term Bool
- Pair { arg1 :: Term a
- , arg2 :: Term b
- } :: Term (a,b)
- If { cnd :: Term Bool
- , tru :: Term a
- , fls :: Term a
- } :: Term a
-</programlisting>
-For every constructor that has a field <literal>f</literal>, (a) the type of
-field <literal>f</literal> must be the same; and (b) the
-result type of the constructor must be the same; both modulo alpha conversion.
-Hence, in our example, we cannot merge the <literal>num</literal> and <literal>arg</literal>
-fields above into a
-single name. Although their field types are both <literal>Term Int</literal>,
-their selector functions actually have different types:
-
-<programlisting>
- num :: Term Int -> Term Int
- arg :: Term Bool -> Term Int
-</programlisting>
-
-At the moment, record updates are not yet possible with GADT, so support is
-limited to record construction, selection and pattern matching:
-
-<programlisting>
- someTerm :: Term Bool
- someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } }
-
- eval :: Term a -> a
- eval Lit { val = i } = i
- eval Succ { num = t } = eval t + 1
- eval Pred { num = t } = eval t - 1
- eval IsZero { arg = t } = eval t == 0
- eval Pair { arg1 = t1, arg2 = t2 } = (eval t1, eval t2)
- eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t)
-</programlisting>
-
-</para></listitem>
-
-<listitem><para>
-You can use strictness annotations, in the obvious places
-in the constructor type:
-<programlisting>
- data Term a where
- Lit :: !Int -> Term Int
- If :: Term Bool -> !(Term a) -> !(Term a) -> Term a
- Pair :: Term a -> Term b -> Term (a,b)
-</programlisting>
-</para></listitem>
-
-<listitem><para>
-You can use a <literal>deriving</literal> clause on a GADT-style data type
-declaration, but only if the data type could also have been declared in
-Haskell-98 syntax. For example, these two declarations are equivalent
-<programlisting>
- data Maybe1 a where {
- Nothing1 :: Maybe a ;
- Just1 :: a -> Maybe a
- } deriving( Eq, Ord )
-
- data Maybe2 a = Nothing2 | Just2 a
- deriving( Eq, Ord )
-</programlisting>
-This simply allows you to declare a vanilla Haskell-98 data type using the
-<literal>where</literal> form without losing the <literal>deriving</literal> clause.
-</para></listitem>
-
-<listitem><para>
-Pattern matching causes type refinement. For example, in the right hand side of the equation
-<programlisting>
- eval :: Term a -> a
- eval (Lit i) = ...
-</programlisting>
-the type <literal>a</literal> is refined to <literal>Int</literal>. (That's the whole point!)
-A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper
-about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page.</para>
-
-<para> The general principle is this: <emphasis>type refinement is only carried out based on user-supplied type annotations</emphasis>.
-So if no type signature is supplied for <literal>eval</literal>, no type refinement happens, and lots of obscure error messages will
-occur. However, the refinement is quite general. For example, if we had:
-<programlisting>
- eval :: Term a -> a -> a
- eval (Lit i) j = i+j
-</programlisting>
-the pattern match causes the type <literal>a</literal> to be refined to <literal>Int</literal> (because of the type
-of the constructor <literal>Lit</literal>, and that refinement also applies to the type of <literal>j</literal>, and
-the result type of the <literal>case</literal> expression. Hence the addition <literal>i+j</literal> is legal.
-</para>
-</listitem>
-</itemizedlist>
-</para>