<option>-fno-monomorphism-restriction</option>,<option>-fno-monomorphism-restriction</option>:
</term>
<listitem>
- <para> These two flags control how generalisation is done in
+ <para> These two flags control how generalisation is done.
See <xref linkend="monomorphism"/>.
</para>
</listitem>
you should be all right.</para>
</sect2>
+
+<sect2 id="postfix-operators">
+<title>Postfix operators</title>
+
+<para>
+GHC allows a small extension to the syntax of left operator sections, which
+allows you to define postfix operators. The extension is this: the left section
+<programlisting>
+ (e !)
+</programlisting>
+is equivalent (from the point of view of both type checking and execution) to the expression
+<programlisting>
+ ((!) e)
+</programlisting>
+(for any expression <literal>e</literal> and operator <literal>(!)</literal>.
+The strict Haskell 98 interpretation is that the section is equivalent to
+<programlisting>
+ (\y -> (!) e y)
+</programlisting>
+That is, the operator must be a function of two arguments. GHC allows it to
+take only one argument, and that in turn allows you to write the function
+postfix.
+</para>
+<para>Since this extension goes beyond Haskell 98, it should really be enabled
+by a flag; but in fact it is enabled all the time. (No Haskell 98 programs
+change their behaviour, of course.)
+</para>
+<para>The extension does not extend to the left-hand side of function
+definitions; you must define such a function in prefix form.</para>
+
+</sect2>
+
</sect1>
check for that declaration.
</para></listitem>
</itemizedlist>
-All this makes it possible for a library author to design a library that relies on
-overlapping instances without the library client having to know.
+These rules make it possible for a library author to design a library that relies on
+overlapping instances without the library client having to know.
+</para>
+<para>
+If an instance declaration is compiled without
+<option>-fallow-overlapping-instances</option>,
+then that instance can never be overlapped. This could perhaps be
+inconvenient. Perhaps the rule should instead say that the
+<emphasis>overlapping</emphasis> instance declaration should be compiled in
+this way, rather than the <emphasis>overlapped</emphasis> one. Perhaps overlap
+at a usage site should be permitted regardless of how the instance declarations
+are compiled, if the <option>-fallow-overlapping-instances</option> flag is
+used at the usage site. (Mind you, the exact usage site can occasionally be
+hard to pin down.) We are interested to receive feedback on these points.
</para>
<para>The <option>-fallow-incoherent-instances</option> flag implies the
<option>-fallow-overlapping-instances</option> flag, but not vice versa.
</sect3>
</sect2>
+ <!-- ======================= COMMENTED OUT ========================
+
+ We intend to remove linear implicit parameters, so I'm at least removing
+ them from the 6.6 user manual
+
<sect2 id="linear-implicit-parameters">
<title>Linear implicit parameters</title>
<para>
<para>
Linear implicit parameters are just like ordinary implicit parameters,
-except that they are "linear" -- that is, they cannot be copied, and
+except that they are "linear"; that is, they cannot be copied, and
must be explicitly "split" instead. Linear implicit parameters are
written '<literal>%x</literal>' instead of '<literal>?x</literal>'.
(The '/' in the '%' suggests the split!)
</sect2>
+================ END OF Linear Implicit Parameters commented out -->
+
<sect2 id="sec-kinding">
<title>Explicitly-kinded quantification</title>
</sect2>
-
+<sect2 id="impredicative-polymorphism">
+<title>Impredicative polymorphism
+</title>
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>. This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types. For example:
+<programlisting>
+ f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+ f (Just g) = Just (g [3], g "hello")
+ f Nothing = Nothing
+</programlisting>
+Notice here that the <literal>Maybe</literal> type is parameterised by the
+<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
+[a])</literal>.
+</para>
+<para>The technical details of this extension are described in the paper
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy">Boxy types:
+type inference for higher-rank types and impredicativity</ulink>,
+which appeared at ICFP 2006.
+</para>
+</sect2>
<sect2 id="scoped-type-variables">
-<title>Scoped type variables
+<title>Lexically scoped type variables
</title>
<para>
-A <emphasis>lexically scoped type variable</emphasis> can be bound by:
-<itemizedlist>
-<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
-<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
-<listitem><para>A result type signature (<xref linkend="result-type-sigs"/>)</para></listitem>
-</itemizedlist>
-For example:
+GHC supports <emphasis>lexically scoped type variables</emphasis>, without
+which some type signatures are simply impossible to write. For example:
<programlisting>
-f (xs::[a]) = ys ++ ys
- where
- ys :: [a]
- ys = reverse xs
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
</programlisting>
-The pattern <literal>(xs::[a])</literal> includes a type signature for <varname>xs</varname>.
-This brings the type variable <literal>a</literal> into scope; it scopes over
-all the patterns and right hand sides for this equation for <function>f</function>.
-In particular, it is in scope at the type signature for <varname>y</varname>.
-</para>
-
-<para>
-At ordinary type signatures, such as that for <varname>ys</varname>, any type variables
-mentioned in the type signature <emphasis>that are not in scope</emphasis> are
-implicitly universally quantified. (If there are no type variables in
-scope, all type variables mentioned in the signature are universally
-quantified, which is just as in Haskell 98.) In this case, since <varname>a</varname>
-is in scope, it is not universally quantified, so the type of <varname>ys</varname> is
-the same as that of <varname>xs</varname>. In Haskell 98 it is not possible to declare
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope; it scopes over
+the entire definition of <literal>f</literal>.
+In particular, it is in scope at the type signature for <varname>ys</varname>.
+In Haskell 98 it is not possible to declare
a type for <varname>ys</varname>; a major benefit of scoped type variables is that
it becomes possible to do so.
</para>
-
-<para>
-Scoped type variables are implemented in both GHC and Hugs. Where the
-implementations differ from the specification below, those differences
-are noted.
-</para>
-
-<para>
-So much for the basic idea. Here are the details.
+<para>Lexically-scoped type variables are enabled by
+<option>-fglasgow-exts</option>.
</para>
+<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
+variables work, compared to earlier releases. Read this section
+carefully!</para>
<sect3>
-<title>What a scoped type variable means</title>
-<para>
-A lexically-scoped type variable is simply
-the name for a type. The restriction it expresses is that all occurrences
-of the same name mean the same type. For example:
-<programlisting>
- f :: [Int] -> Int -> Int
- f (xs::[a]) (y::a) = (head xs + y) :: a
-</programlisting>
-The pattern type signatures on the left hand side of
-<literal>f</literal> express the fact that <literal>xs</literal>
-must be a list of things of some type <literal>a</literal>; and that <literal>y</literal>
-must have this same type. The type signature on the expression <literal>(head xs)</literal>
-specifies that this expression must have the same type <literal>a</literal>.
-<emphasis>There is no requirement that the type named by "<literal>a</literal>" is
-in fact a type variable</emphasis>. Indeed, in this case, the type named by "<literal>a</literal>" is
-<literal>Int</literal>. (This is a slight liberalisation from the original rather complex
-rules, which specified that a pattern-bound type variable should be universally quantified.)
-For example, all of these are legal:</para>
-
-<programlisting>
- t (x::a) (y::a) = x+y*2
-
- f (x::a) (y::b) = [x,y] -- a unifies with b
-
- g (x::a) = x + 1::Int -- a unifies with Int
-
- h x = let k (y::a) = [x,y] -- a is free in the
- in k x -- environment
-
- k (x::a) True = ... -- a unifies with Int
- k (x::Int) False = ...
-
- w :: [b] -> [b]
- w (x::a) = x -- a unifies with [b]
-</programlisting>
-
-</sect3>
-
-<sect3>
-<title>Scope and implicit quantification</title>
-
-<para>
+<title>Overview</title>
+<para>The design follows the following principles
<itemizedlist>
-<listitem>
-
-<para>
-All the type variables mentioned in a pattern,
-that are not already in scope,
-are brought into scope by the pattern. We describe this set as
-the <emphasis>type variables bound by the pattern</emphasis>.
-For example:
-<programlisting>
- f (x::a) = let g (y::(a,b)) = fst y
- in
- g (x,True)
-</programlisting>
-The pattern <literal>(x::a)</literal> brings the type variable
-<literal>a</literal> into scope, as well as the term
-variable <literal>x</literal>. The pattern <literal>(y::(a,b))</literal>
-contains an occurrence of the already-in-scope type variable <literal>a</literal>,
-and brings into scope the type variable <literal>b</literal>.
-</para>
-</listitem>
-
-<listitem>
-<para>
-The type variable(s) bound by the pattern have the same scope
-as the term variable(s) bound by the pattern. For example:
-<programlisting>
- let
- f (x::a) = <...rhs of f...>
- (p::b, q::b) = (1,2)
- in <...body of let...>
-</programlisting>
-Here, the type variable <literal>a</literal> scopes over the right hand side of <literal>f</literal>,
-just like <literal>x</literal> does; while the type variable <literal>b</literal> scopes over the
-body of the <literal>let</literal>, and all the other definitions in the <literal>let</literal>,
-just like <literal>p</literal> and <literal>q</literal> do.
-Indeed, the newly bound type variables also scope over any ordinary, separate
-type signatures in the <literal>let</literal> group.
-</para>
-</listitem>
-
-
-<listitem>
-<para>
-The type variables bound by the pattern may be
-mentioned in ordinary type signatures or pattern
-type signatures anywhere within their scope.
-
-</para>
-</listitem>
-
-<listitem>
-<para>
- In ordinary type signatures, any type variable mentioned in the
-signature that is in scope is <emphasis>not</emphasis> universally quantified.
-
-</para>
-</listitem>
-
-<listitem>
-
-<para>
- Ordinary type signatures do not bring any new type variables
-into scope (except in the type signature itself!). So this is illegal:
-
-<programlisting>
- f :: a -> a
- f x = x::a
-</programlisting>
-
-It's illegal because <varname>a</varname> is not in scope in the body of <function>f</function>,
-so the ordinary signature <literal>x::a</literal> is equivalent to <literal>x::forall a.a</literal>;
-and that is an incorrect typing.
-
+<listitem><para>A scoped type variable stands for a type <emphasis>variable</emphasis>, and not for
+a <emphasis>type</emphasis>. (This is a change from GHC's earlier
+design.)</para></listitem>
+<listitem><para>Furthermore, distinct lexical type variables stand for distinct
+type variables. This means that every programmer-written type signature
+(includin one that contains free scoped type variables) denotes a
+<emphasis>rigid</emphasis> type; that is, the type is fully known to the type
+checker, and no inference is involved.</para></listitem>
+<listitem><para>Lexical type variables may be alpha-renamed freely, without
+changing the program.</para></listitem>
+</itemizedlist>
</para>
-</listitem>
-
-<listitem>
<para>
-The pattern type signature is a monotype:
-</para>
-
+A <emphasis>lexically scoped type variable</emphasis> can be bound by:
<itemizedlist>
-<listitem> <para>
-A pattern type signature cannot contain any explicit <literal>forall</literal> quantification.
-</para> </listitem>
-
-<listitem> <para>
-The type variables bound by a pattern type signature can only be instantiated to monotypes,
-not to type schemes.
-</para> </listitem>
-
-<listitem> <para>
-There is no implicit universal quantification on pattern type signatures (in contrast to
-ordinary type signatures).
-</para> </listitem>
-
+<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
+<listitem><para>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
+<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
+<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
</itemizedlist>
-
-</listitem>
-
-<listitem>
+</para>
<para>
-
-The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
-scope over the methods defined in the <literal>where</literal> part. For example:
-
-
+In Haskell, a programmer-written type signature is implicitly quantifed over
+its free type variables (<ulink
+url="http://haskell.org/onlinereport/decls.html#sect4.1.2">Section
+4.1.2</ulink>
+of the Haskel Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is <emphasis>not</emphasis> universally
+quantified. For example, if type variable <literal>a</literal> is in scope,
+then
<programlisting>
- class C a where
- op :: [a] -> a
-
- op xs = let ys::[a]
- ys = reverse xs
- in
- head ys
+ (e :: a -> a) means (e :: a -> a)
+ (e :: b -> b) means (e :: forall b. b->b)
+ (e :: a -> b) means (e :: forall b. a->b)
</programlisting>
-
-
-(Not implemented in Hugs yet, Dec 98).
</para>
-</listitem>
-
-</itemizedlist>
-</para>
</sect3>
+
<sect3 id="decl-type-sigs">
<title>Declaration type signatures</title>
<para>A declaration type signature that has <emphasis>explicit</emphasis>
</para>
</sect3>
-<sect3 id="pattern-type-sigs">
-<title>Where a pattern type signature can occur</title>
-
-<para>
-A pattern type signature can occur in any pattern. For example:
-<itemizedlist>
-
-<listitem>
-<para>
-A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
-
-
-<programlisting>
- f ((x,y)::(a,b)) = (y,x) :: (b,a)
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- Pattern type signatures, including the result part, can be used
-in lambda abstractions:
-
-<programlisting>
- (\ (x::a, y) :: a -> x)
-</programlisting>
-</para>
-</listitem>
-<listitem>
-
-<para>
- Pattern type signatures, including the result part, can be used
-in <literal>case</literal> expressions:
+<sect3 id="exp-type-sigs">
+<title>Expression type signatures</title>
+<para>An expression type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression. For example:
<programlisting>
- case e of { ((x::a, y) :: (a,b)) -> x }
+ f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
</programlisting>
-
-Note that the <literal>-></literal> symbol in a case alternative
-leads to difficulties when parsing a type signature in the pattern: in
-the absence of the extra parentheses in the example above, the parser
-would try to interpret the <literal>-></literal> as a function
-arrow and give a parse error later.
-
+Here, the type signature <literal>forall a. ST s Bool</literal> brings the
+type variable <literal>s</literal> into scope, in the annotated expression
+<literal>(op >>= \(x :: STRef s Int) -> g x)</literal>.
</para>
-</listitem>
+</sect3>
-<listitem>
+<sect3 id="pattern-type-sigs">
+<title>Pattern type signatures</title>
<para>
-To avoid ambiguity, the type after the “<literal>::</literal>” in a result
-pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
-token or a parenthesised type of some sort). To see why,
-consider how one would parse this:
-
-
+A type signature may occur in any pattern; this is a <emphasis>pattern type
+signature</emphasis>.
+For example:
<programlisting>
- \ x :: a -> b -> x
+ -- f and g assume that 'a' is already in scope
+ f = \(x::Int, y::a) -> x
+ g (x::a) = x
+ h ((x,y) :: (Int,Bool)) = (y,x)
</programlisting>
-
-
+In the case where all the type variables in the pattern type sigature are
+already in scope (i.e. bound by the enclosing context), matters are simple: the
+signature simply constrains the type of the pattern in the obvious way.
</para>
-</listitem>
-
-<listitem>
-
<para>
- Pattern type signatures can bind existential type variables.
-For example:
-
-
+There is only one situation in which you can write a pattern type signature that
+mentions a type variable that is not already in scope, namely in pattern match
+of an existential data constructor. For example:
<programlisting>
data T = forall a. MkT [a]
- f :: T -> T
- f (MkT [t::a]) = MkT t3
+ k :: T -> T
+ k (MkT [t::a]) = MkT t3
where
t3::[a] = [t,t,t]
</programlisting>
-
-
+Here, the pattern type signature <literal>(t::a)</literal> mentions a lexical type
+variable that is not already in scope. Indeed, it cannot already be in scope,
+because it is bound by the pattern match. GHC's rule is that in this situation
+(and only then), a pattern type signature can mention a type variable that is
+not already in scope; the effect is to bring it into scope, standing for the
+existentially-bound type variable.
</para>
-</listitem>
-
-
-<listitem>
-
<para>
-Pattern type signatures
-can be used in pattern bindings:
-
-<programlisting>
- f x = let (y, z::a) = x in ...
- f1 x = let (y, z::Int) = x in ...
- f2 (x::(Int,a)) = let (y, z::a) = x in ...
- f3 :: (b->b) = \x -> x
-</programlisting>
-
-In all such cases, the binding is not generalised over the pattern-bound
-type variables. Thus <literal>f3</literal> is monomorphic; <literal>f3</literal>
-has type <literal>b -> b</literal> for some type <literal>b</literal>,
-and <emphasis>not</emphasis> <literal>forall b. b -> b</literal>.
-In contrast, the binding
-<programlisting>
- f4 :: b->b
- f4 = \x -> x
-</programlisting>
-makes a polymorphic function, but <literal>b</literal> is not in scope anywhere
-in <literal>f4</literal>'s scope.
-
+If this seems a little odd, we think so too. But we must have
+<emphasis>some</emphasis> way to bring such type variables into scope, else we
+could not name existentially-bound type variables in subequent type signatures.
</para>
-</listitem>
-</itemizedlist>
+<para>
+This is (now) the <emphasis>only</emphasis> situation in which a pattern type
+signature is allowed to mention a lexical variable that is not already in
+scope.
+For example, both <literal>f</literal> and <literal>g</literal> would be
+illegal if <literal>a</literal> was not already in scope.
</para>
-<para>Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures. The two can be used independently or together.</para>
+
</sect3>
+<!-- ==================== Commented out part about result type signatures
+
<sect3 id="result-type-sigs">
<title>Result type signatures</title>
<para>
-The result type of a function can be given a signature, thus:
-
+The result type of a function, lambda, or case expression alternative can be given a signature, thus:
<programlisting>
- f (x::a) :: [a] = [x,x,x]
-</programlisting>
+ {- f assumes that 'a' is already in scope -}
+ f x y :: [a] = [x,y,x]
+ g = \ x :: [Int] -> [3,4]
-The final <literal>:: [a]</literal> after all the patterns gives a signature to the
-result type. Sometimes this is the only way of naming the type variable
-you want:
-
-
-<programlisting>
- f :: Int -> [a] -> [a]
- f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
- in \xs -> map g (reverse xs `zip` xs)
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ (y:ys) :: a -> y
</programlisting>
-
+The final <literal>:: [a]</literal> after the patterns of <literal>f</literal> gives the type of
+the result of the function. Similarly, the body of the lambda in the RHS of
+<literal>g</literal> is <literal>[Int]</literal>, and the RHS of the case
+alternative in <literal>h</literal> is <literal>a</literal>.
</para>
+<para> A result type signature never brings new type variables into scope.</para>
<para>
-The type variables bound in a result type signature scope over the right hand side
-of the definition. However, consider this corner-case:
+There are a couple of syntactic wrinkles. First, notice that all three
+examples would parse quite differently with parentheses:
<programlisting>
- rev1 :: [a] -> [a] = \xs -> reverse xs
+ {- f assumes that 'a' is already in scope -}
+ f x (y :: [a]) = [x,y,x]
- foo ys = rev (ys::[a])
+ g = \ (x :: [Int]) -> [3,4]
+
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ ((y:ys) :: a) -> y
</programlisting>
-The signature on <literal>rev1</literal> is considered a pattern type signature, not a result
-type signature, and the type variables it binds have the same scope as <literal>rev1</literal>
-itself (i.e. the right-hand side of <literal>rev1</literal> and the rest of the module too).
-In particular, the expression <literal>(ys::[a])</literal> is OK, because the type variable <literal>a</literal>
-is in scope (otherwise it would mean <literal>(ys::forall a.[a])</literal>, which would be rejected).
-</para>
-<para>
-As mentioned above, <literal>rev1</literal> is made monomorphic by this scoping rule.
-For example, the following program would be rejected, because it claims that <literal>rev1</literal>
-is polymorphic:
+Now the signature is on the <emphasis>pattern</emphasis>; and
+<literal>h</literal> would certainly be ill-typed (since the pattern
+<literal>(y:ys)</literal> cannot have the type <literal>a</literal>.
+
+Second, to avoid ambiguity, the type after the “<literal>::</literal>” in a result
+pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
+token or a parenthesised type of some sort). To see why,
+consider how one would parse this:
<programlisting>
- rev1 :: [b] -> [b]
- rev1 :: [a] -> [a] = \xs -> reverse xs
+ \ x :: a -> b -> x
</programlisting>
</para>
+</sect3>
+
+ -->
+<sect3 id="cls-inst-scoped-tyvars">
+<title>Class and instance declarations</title>
<para>
-Result type signatures are not yet implemented in Hugs.
-</para>
+The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
+scope over the methods defined in the <literal>where</literal> part. For example:
+
+
+<programlisting>
+ class C a where
+ op :: [a] -> a
+
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
+</programlisting>
+</para>
</sect3>
</sect2>
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 extensions to GHC are these:
+<para>
+The rest of this section outlines the extensions to GHC that support GADTs.
+It is far from comprehensive, but the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
+unification-based type inference for GADTs</ulink>,
+which appeared in ICFP 2006.
<itemizedlist>
<listitem><para>
Data type declarations have a 'where' form, as exemplified above. The type signature of
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
<sect1 id="template-haskell">
<title>Template Haskell</title>
-<para>Template Haskell allows you to do compile-time meta-programming in Haskell. There is a "home page" for
-Template Haskell at <ulink url="http://www.haskell.org/th/">
-http://www.haskell.org/th/</ulink>, while
-the background to
+<para>Template Haskell allows you to do compile-time meta-programming in
+Haskell.
+The background to
the main technical innovations is discussed in "<ulink
url="http://research.microsoft.com/~simonpj/papers/meta-haskell">
Template Meta-programming for Haskell</ulink>" (Proc Haskell Workshop 2002).
-The details of the Template Haskell design are still in flux. Make sure you
-consult the <ulink url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online library reference material</ulink>
+</para>
+<para>
+There is a Wiki page about
+Template Haskell at <ulink url="http://haskell.org/haskellwiki/Template_Haskell">
+http://www.haskell.org/th/</ulink>, and that is the best place to look for
+further details.
+You may also
+consult the <ulink
+url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online
+Haskell library reference material</ulink>
(search for the type ExpQ).
[Temporary: many changes to the original design are described in
<ulink url="http://research.microsoft.com/~simonpj/tmp/notes2.ps">"http://research.microsoft.com/~simonpj/tmp/notes2.ps"</ulink>.
-Not all of these changes are in GHC 6.2.]
+Not all of these changes are in GHC 6.6.]
</para>
<para> The first example from that paper is set out below as a worked example to help get you started.
<para>GHC supports an extension of pattern matching called <emphasis>bang
patterns</emphasis>. Bang patterns are under consideration for Haskell Prime.
The <ulink
-url="http://hackage.haskell.org/trac/haskell-prime/wiki/BangPatterns">the
-Haskell prime feature description</ulink> contains more discussion and examples
+url="http://hackage.haskell.org/trac/haskell-prime/wiki/BangPatterns">Haskell
+prime feature description</ulink> contains more discussion and examples
than the material below.
</para>
<para>
GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
r) ->
tpl2})
- (%note "foo"
+ (%note "bar"
eta);
</programlisting>
<sect1 id="generic-classes">
<title>Generic classes</title>
- <para>(Note: support for generic classes is currently broken in
- GHC 5.02).</para>
-
<para>
The ideas behind this extension are described in detail in "Derivable type classes",
Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
</sect2>
<sect2>
-<title>Monomorphic patteern bindings</title>
+<title>Monomorphic pattern bindings</title>
<indexterm><primary><option>-fno-mono-pat-binds</option></primary></indexterm>
<indexterm><primary><option>-fmono-pat-binds</option></primary></indexterm>
projects / ghc-hetmet.git / blobdiff