For example:
<programlisting>
-- f and g assume that 'a' is already in scope
- f = \(x::Int, y) -> x
+ f = \(x::Int, y::a) -> x
g (x::a) = x
h ((x,y) :: (Int,Bool)) = (y,x)
</programlisting>
where
<itemizedlist>
<listitem><para>
- The type <literal>t</literal> is an arbitrary type
+ The <literal>ci</literal> are partial applications of
+ classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
+ is exactly <literal>j+1</literal>. That is, <literal>C</literal> lacks exactly one type argument.
</para></listitem>
<listitem><para>
- The <literal>vk+1...vn</literal> are type variables which do not occur in
- <literal>t</literal>, and
+ The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.
</para></listitem>
<listitem><para>
- The <literal>ci</literal> are partial applications of
- classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
- is exactly <literal>j+1</literal>. That is, <literal>C</literal> lacks exactly one type argument.
+ The type <literal>t</literal> is an arbitrary type.
+</para></listitem>
+<listitem><para>
+ The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>,
+ nor in the <literal>ci</literal>, and
</para></listitem>
<listitem><para>
None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>,
Then, for each <literal>ci</literal>, the derived instance
declaration is:
<programlisting>
- instance ci (t vk+1...v) => ci (T v1...vp)
+ instance ci t => ci (T v1...vk)
</programlisting>
-where <literal>p</literal> is chosen so that <literal>T v1...vp</literal> is of the
-right <emphasis>kind</emphasis> for the last parameter of class <literal>Ci</literal>.
-</para>
-<para>
-
As an example which does <emphasis>not</emphasis> work, consider
<programlisting>
newtype NonMonad m s = NonMonad (State s m s) deriving Monad
<!-- ====================== Generalised algebraic data types ======================= -->
<sect1 id="gadt">
-<title>Generalised Algebraic Data Types</title>
+<title>Generalised Algebraic Data Types (GADTs)</title>
-<para>Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you
+<para>Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you
to give the type signatures of constructors explicitly. For example:
<programlisting>
data Term a where
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.
+These and many other examples are given in papers by Hongwei Xi, and
+Tim Sheard. There is a longer introduction
+<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
+and Ralf Hinze's
+<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
+may use different notation to that implemented in GHC.
</para>
<para>
The rest of this section outlines the extensions to GHC that support GADTs.
Haskell-98 syntax. For example, these two declarations are equivalent
<programlisting>
data Maybe1 a where {
- Nothing1 :: Maybe a ;
- Just1 :: a -> Maybe a
+ Nothing1 :: Maybe1 a ;
+ Just1 :: a -> Maybe1 a
} deriving( Eq, Ord )
data Maybe2 a = Nothing2 | Just2 a