</varlistentry>
<varlistentry>
+ <term><option>-fimplicit-params</option></term>
+ <listitem>
+ <para>Enables implicit parameters (see <xref
+ linkend="implicit-parameters"/>). Currently also implied by
+ <option>-fglasgow-exts</option>.</para>
+
+ <para>Syntax stolen:
+ <literal>?<replaceable>varid</replaceable></literal>,
+ <literal>%<replaceable>varid</replaceable></literal>.</para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
+ <term><option>-fscoped-type-variables</option></term>
+ <listitem>
+ <para>Enables lexically-scoped type variables (see <xref
+ linkend="scoped-type-variables"/>). Implied by
+ <option>-fglasgow-exts</option>.</para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
<term><option>-fth</option></term>
<listitem>
<para>Enables Template Haskell (see <xref
</listitem>
</varlistentry>
- <varlistentry>
- <term><option>-fimplicit-params</option></term>
- <listitem>
- <para>Enables implicit parameters (see <xref
- linkend="implicit-parameters"/>). Currently also implied by
- <option>-fglasgow-exts</option>.</para>
-
- <para>Syntax stolen:
- <literal>?<replaceable>varid</replaceable></literal>,
- <literal>%<replaceable>varid</replaceable></literal>.</para>
- </listitem>
- </varlistentry>
-
</variablelist>
</sect1>
<para>The Real Truth about what primitive types there are, and what operations
work over those types, is held in the file
-<filename>fptools/ghc/compiler/prelude/primops.txt</filename>.
+<filename>fptools/ghc/compiler/prelude/primops.txt.pp</filename>.
This file is used directly to generate GHC's primitive-operation definitions, so
it is always correct! It is also intended for processing into text.</para>
represents a primitive value, then it really does point to that value:
no unevaluated thunks, no indirections…nothing can be at the
other end of the pointer than the primitive value.
+A numerically-intensive program using unboxed types can
+go a <emphasis>lot</emphasis> faster than its “standard”
+counterpart—we saw a threefold speedup on one example.
</para>
<para>
-There are some restrictions on the use of primitive types, the main
-one being that you can't pass a primitive value to a polymorphic
+There are some restrictions on the use of primitive types:
+<itemizedlist>
+<listitem><para>The main restriction
+is that you can't pass a primitive value to a polymorphic
function or store one in a polymorphic data type. This rules out
things like <literal>[Int#]</literal> (i.e. lists of primitive
integers). The reason for this restriction is that polymorphic
worse, the unboxed value might be larger than a pointer
(<literal>Double#</literal> for instance).
</para>
+</listitem>
+<listitem><para> You cannot bind a variable with an unboxed type
+in a <emphasis>top-level</emphasis> binding.
+</para></listitem>
+<listitem><para> You cannot bind a variable with an unboxed type
+in a <emphasis>recursive</emphasis> binding.
+</para></listitem>
+<listitem><para> You may bind unboxed variables in a (non-recursive,
+non-top-level) pattern binding, but any such variable causes the entire
+pattern-match
+to become strict. For example:
+<programlisting>
+ data Foo = Foo Int Int#
-<para>
-Nevertheless, A numerically-intensive program using unboxed types can
-go a <emphasis>lot</emphasis> faster than its “standard”
-counterpart—we saw a threefold speedup on one example.
+ f x = let (Foo a b, w) = ..rhs.. in ..body..
+</programlisting>
+Since <literal>b</literal> has type <literal>Int#</literal>, the entire pattern
+match
+is strict, and the program behaves as if you had written
+<programlisting>
+ data Foo = Foo Int Int#
+
+ f x = case ..rhs.. of { (Foo a b, w) -> ..body.. }
+</programlisting>
+</para>
+</listitem>
+</itemizedlist>
</para>
</sect2>
using fully-fledged tuples. When an unboxed tuple is returned, the
components are put directly into registers or on the stack; the
unboxed tuple itself does not have a composite representation. Many
-of the primitive operations listed in this section return unboxed
+of the primitive operations listed in <literal>primops.txt.pp</literal> return unboxed
tuples.
+In particular, the <literal>IO</literal> and <literal>ST</literal> monads use unboxed
+tuples to avoid unnecessary allocation during sequences of operations.
</para>
<para>
There are some pretty stringent restrictions on the use of unboxed tuples:
-</para>
-
-<para>
-
<itemizedlist>
<listitem>
<para>
- Unboxed tuple types are subject to the same restrictions as
+Values of unboxed tuple types are subject to the same restrictions as
other unboxed types; i.e. they may not be stored in polymorphic data
structures or passed to polymorphic functions.
<listitem>
<para>
- Unboxed tuples may only be constructed as the direct result of
-a function, and may only be deconstructed with a <literal>case</literal> expression.
-eg. the following are valid:
+No variable can have an unboxed tuple type, nor may a constructor or function
+argument have an unboxed tuple type. The following are all illegal:
<programlisting>
-f x y = (# x+1, y-1 #)
-g x = case f x x of { (# a, b #) -> a + b }
-</programlisting>
+ data Foo = Foo (# Int, Int #)
+ f :: (# Int, Int #) -> (# Int, Int #)
+ f x = x
-but the following are invalid:
+ g :: (# Int, Int #) -> Int
+ g (# a,b #) = a
-
-<programlisting>
-f x y = g (# x, y #)
-g (# x, y #) = x + y
+ h x = let y = (# x,x #) in ...
</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- No variable can have an unboxed tuple type. This is illegal:
-
-
-<programlisting>
-f :: (# Int, Int #) -> (# Int, Int #)
-f x = x
-</programlisting>
-
-
-because <literal>x</literal> has an unboxed tuple type.
-
</para>
</listitem>
-
</itemizedlist>
-
</para>
-
<para>
-Note: we may relax some of these restrictions in the future.
-</para>
-
-<para>
-The <literal>IO</literal> and <literal>ST</literal> monads use unboxed
-tuples to avoid unnecessary allocation during sequences of operations.
+The typical use of unboxed tuples is simply to return multiple values,
+binding those multiple results with a <literal>case</literal> expression, thus:
+<programlisting>
+ f x y = (# x+1, y-1 #)
+ g x = case f x x of { (# a, b #) -> a + b }
+</programlisting>
+You can have an unboxed tuple in a pattern binding, thus
+<programlisting>
+ f x = let (# p,q #) = h x in ..body..
+</programlisting>
+If the types of <literal>p</literal> and <literal>q</literal> are not unboxed,
+the resulting binding is lazy like any other Haskell pattern binding. The
+above example desugars like this:
+<programlisting>
+ f x = let t = case h x o f{ (# p,q #) -> (p,q)
+ p = fst t
+ q = snd t
+ in ..body..
+</programlisting>
+Indeed, the bindings can even be recursive.
</para>
</sect2>
</programlisting>
<para>
-The semantics should be clear enough. The qualifers are matched in order.
+The semantics should be clear enough. The qualifiers are matched in order.
For a <literal><-</literal> qualifier, which I call a pattern guard, the
right hand side is evaluated and matched against the pattern on the left.
If the match fails then the whole guard fails and the next equation is
So the <option>-fno-implicit-prelude</option> flag causes
the following pieces of built-in syntax to refer to
<emphasis>whatever is in scope</emphasis>, not the Prelude
- versions:</para>
+ versions:
<itemizedlist>
<listitem>
- <para>Integer and fractional literals mean
- "<literal>fromInteger 1</literal>" and
- "<literal>fromRational 3.2</literal>", not the
- Prelude-qualified versions; both in expressions and in
- patterns. </para>
- <para>However, the standard Prelude <literal>Eq</literal> class
- is still used for the equality test necessary for literal patterns.</para>
- </listitem>
+ <para>An integer literal <literal>368</literal> means
+ "<literal>fromInteger (368::Integer)</literal>", rather than
+ "<literal>Prelude.fromInteger (368::Integer)</literal>".
+</para> </listitem>
- <listitem>
- <para>Negation (e.g. "<literal>- (f x)</literal>")
- means "<literal>negate (f x)</literal>" (not
- <literal>Prelude.negate</literal>).</para>
- </listitem>
+ <listitem><para>Fractional literals are handed in just the same way,
+ except that the translation is
+ <literal>fromRational (3.68::Rational)</literal>.
+</para> </listitem>
+
+ <listitem><para>The equality test in an overloaded numeric pattern
+ uses whatever <literal>(==)</literal> is in scope.
+</para> </listitem>
+
+ <listitem><para>The subtraction operation, and the
+ greater-than-or-equal test, in <literal>n+k</literal> patterns
+ use whatever <literal>(-)</literal> and <literal>(>=)</literal> are in scope.
+ </para></listitem>
<listitem>
- <para>In an n+k pattern, the standard Prelude
- <literal>Ord</literal> class is still used for comparison,
- but the necessary subtraction uses whatever
- "<literal>(-)</literal>" is in scope (not
- "<literal>Prelude.(-)</literal>").</para>
- </listitem>
+ <para>Negation (e.g. "<literal>- (f x)</literal>")
+ means "<literal>negate (f x)</literal>", both in numeric
+ patterns, and expressions.
+ </para></listitem>
<listitem>
<para>"Do" notation is translated using whatever
functions <literal>(>>=)</literal>,
- <literal>(>>)</literal>, <literal>fail</literal>, and
- <literal>return</literal>, are in scope (not the Prelude
- versions). List comprehensions, and parallel array
+ <literal>(>>)</literal>, and <literal>fail</literal>,
+ are in scope (not the Prelude
+ versions). List comprehensions, mdo (<xref linkend="mdo-notation"/>), and parallel array
comprehensions, are unaffected. </para></listitem>
- </itemizedlist>
- <para>Be warned: this is an experimental facility, with fewer checks than
- usual. In particular, it is essential that the functions GHC finds in scope
- must have the appropriate types, namely:
- <screen>
- fromInteger :: forall a. (...) => Integer -> a
- fromRational :: forall a. (...) => Rational -> a
- negate :: forall a. (...) => a -> a
- (-) :: forall a. (...) => a -> a -> a
- (>>=) :: forall m a. (...) => m a -> (a -> m b) -> m b
- (>>) :: forall m a. (...) => m a -> m b -> m b
- return :: forall m a. (...) => a -> m a
- fail :: forall m a. (...) => String -> m a
- </screen>
- (The (...) part can be any context including the empty context; that part
- is up to you.)
- If the functions don't have the right type, very peculiar things may
- happen. Use <literal>-dcore-lint</literal> to
- typecheck the desugared program. If Core Lint is happy you should be all right.</para>
+ <listitem>
+ <para>Arrow
+ notation (see <xref linkend="arrow-notation"/>)
+ uses whatever <literal>arr</literal>,
+ <literal>(>>>)</literal>, <literal>first</literal>,
+ <literal>app</literal>, <literal>(|||)</literal> and
+ <literal>loop</literal> functions are in scope. But unlike the
+ other constructs, the types of these functions must match the
+ Prelude types very closely. Details are in flux; if you want
+ to use this, ask!
+ </para></listitem>
+ </itemizedlist>
+In all cases (apart from arrow notation), the static semantics should be that of the desugared form,
+even if that is a little unexpected. For emample, the
+static semantics of the literal <literal>368</literal>
+is exactly that of <literal>fromInteger (368::Integer)</literal>; it's fine for
+<literal>fromInteger</literal> to have any of the types:
+<programlisting>
+fromInteger :: Integer -> Integer
+fromInteger :: forall a. Foo a => Integer -> a
+fromInteger :: Num a => a -> Integer
+fromInteger :: Integer -> Bool -> Bool
+</programlisting>
+</para>
+
+ <para>Be warned: this is an experimental facility, with
+ fewer checks than usual. Use <literal>-dcore-lint</literal>
+ to typecheck the desugared program. If Core Lint is happy
+ you should be all right.</para>
</sect2>
</sect1>
</sect3>
<sect3 id="infix-tycons">
-<title>Infix type constructors</title>
+<title>Infix type constructors, classes, and type variables</title>
<para>
-GHC allows type constructors to be operators, and to be written infix, very much
-like expressions. More specifically:
+GHC allows type constructors, classes, and type variables to be operators, and
+to be written infix, very much like expressions. More specifically:
<itemizedlist>
<listitem><para>
- A type constructor can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
+ A type constructor or class can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
The lexical syntax is the same as that for data constructors.
</para></listitem>
<listitem><para>
- Types can be written infix. For example <literal>Int :*: Bool</literal>.
+ Data type and type-synonym declarations can be written infix, parenthesised
+ if you want further arguments. E.g.
+<screen>
+ data a :*: b = Foo a b
+ type a :+: b = Either a b
+ class a :=: b where ...
+
+ data (a :**: b) x = Baz a b x
+ type (a :++: b) y = Either (a,b) y
+</screen>
+ </para></listitem>
+<listitem><para>
+ Types, and class constraints, can be written infix. For example
+ <screen>
+ x :: Int :*: Bool
+ f :: (a :=: b) => a -> b
+ </screen>
+ </para></listitem>
+<listitem><para>
+ A type variable can be an (unqualified) operator e.g. <literal>+</literal>.
+ The lexical syntax is the same as that for variable operators, excluding "(.)",
+ "(!)", and "(*)". In a binding position, the operator must be
+ parenthesised. For example:
+<programlisting>
+ type T (+) = Int + Int
+ f :: T Either
+ f = Left 3
+
+ liftA2 :: Arrow (~>)
+ => (a -> b -> c) -> (e ~> a) -> (e ~> b) -> (e ~> c)
+ liftA2 = ...
+</programlisting>
</para></listitem>
<listitem><para>
Back-quotes work
<literal>Int `a` Bool</literal>. Similarly, parentheses work the same; e.g. <literal>(:*:) Int Bool</literal>.
</para></listitem>
<listitem><para>
- Fixities may be declared for type constructors just as for data constructors. However,
+ Fixities may be declared for type constructors, or classes, just as for data constructors. However,
one cannot distinguish between the two in a fixity declaration; a fixity declaration
sets the fixity for a data constructor and the corresponding type constructor. For example:
<screen>
<listitem><para>
Function arrow is <literal>infixr</literal> with fixity 0. (This might change; I'm not sure what it should be.)
</para></listitem>
-<listitem><para>
- Data type and type-synonym declarations can be written infix. E.g.
-<screen>
- data a :*: b = Foo a b
- type a :+: b = Either a b
-</screen>
- </para></listitem>
-<listitem><para>
- The only thing that differs between operators in types and operators in expressions is that
- ordinary non-constructor operators, such as <literal>+</literal> and <literal>*</literal>
- are not allowed in types. Reason: the uniform thing to do would be to make them type
- variables, but that's not very useful. A less uniform but more useful thing would be to
- allow them to be type <emphasis>constructors</emphasis>. But that gives trouble in export
- lists. So for now we just exclude them.
- </para></listitem>
</itemizedlist>
</para>
<title>Liberalised type synonyms</title>
<para>
-Type synonmys are like macros at the type level, and
+Type synonyms are like macros at the type level, and
GHC does validity checking on types <emphasis>only after expanding type synonyms</emphasis>.
That means that GHC can be very much more liberal about type synonyms than Haskell 98:
<itemizedlist>
foo :: Generic Id []
</programlisting>
-After epxanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+After expanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
<programlisting>
foo :: forall x. x -> [x]
</programlisting>
<para>
This section documents GHC's implementation of multi-parameter type
classes. There's lots of background in the paper <ulink
-url="http://research.microsoft.com/~simonpj/multi.ps.gz" >Type
+url="http://research.microsoft.com/~simonpj/Papers/type-class-design-space" >Type
classes: exploring the design space</ulink > (Simon Peyton Jones, Mark
Jones, Erik Meijer).
</para>
<para>
<emphasis>All of the class type variables must be reachable (in the sense
mentioned in <xref linkend="type-restrictions"/>)
-from the free varibles of each method type
+from the free variables of each method type
</emphasis>. For example:
<para>
Note
that the reachability condition is weaker than saying that <literal>a</literal> is
-functionally dependendent on a type variable free in
+functionally dependent on a type variable free in
<literal>type</literal> (see <xref
linkend="functional-dependencies"/>). The reason for this is there
might be a "hidden" dependency, in a superclass perhaps. So
<sect2 id="instance-decls">
<title>Instance declarations</title>
-<sect3>
+<sect3 id="instance-overlap">
<title>Overlapping instances</title>
<para>
-In general, <emphasis>instance declarations may not overlap</emphasis>. The two instance
-declarations
-
-
-<programlisting>
- instance context1 => C type1 where ...
- instance context2 => C type2 where ...
-</programlisting>
-
-"overlap" if <literal>type1</literal> and <literal>type2</literal> unify.
-</para>
-<para>
-However, if you give the command line option
-<option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
-option</primary></indexterm> then overlapping instance declarations are permitted.
-However, GHC arranges never to commit to using an instance declaration
-if another instance declaration also applies, either now or later.
-
-<itemizedlist>
-<listitem>
-
-<para>
- EITHER <literal>type1</literal> and <literal>type2</literal> do not unify
+In general, <emphasis>GHC requires that that it be unambiguous which instance
+declaration
+should be used to resolve a type-class constraint</emphasis>. This behaviour
+can be modified by two flags: <option>-fallow-overlapping-instances</option>
+<indexterm><primary>-fallow-overlapping-instances
+</primary></indexterm>
+and <option>-fallow-incoherent-instances</option>
+<indexterm><primary>-fallow-incoherent-instances
+</primary></indexterm>, as this section discusses.</para>
+<para>
+When GHC tries to resolve, say, the constraint <literal>C Int Bool</literal>,
+it tries to match every instance declaration against the
+constraint,
+by instantiating the head of the instance declaration. For example, consider
+these declarations:
+<programlisting>
+ instance context1 => C Int a where ... -- (A)
+ instance context2 => C a Bool where ... -- (B)
+ instance context3 => C Int [a] where ... -- (C)
+ instance context4 => C Int [Int] where ... -- (D)
+</programlisting>
+The instances (A) and (B) match the constraint <literal>C Int Bool</literal>,
+but (C) and (D) do not. When matching, GHC takes
+no account of the context of the instance declaration
+(<literal>context1</literal> etc).
+GHC's default behaviour is that <emphasis>exactly one instance must match the
+constraint it is trying to resolve</emphasis>.
+It is fine for there to be a <emphasis>potential</emphasis> of overlap (by
+including both declarations (A) and (B), say); an error is only reported if a
+particular constraint matches more than one.
+</para>
+
+<para>
+The <option>-fallow-overlapping-instances</option> flag instructs GHC to allow
+more than one instance to match, provided there is a most specific one. For
+example, the constraint <literal>C Int [Int]</literal> matches instances (A),
+(C) and (D), but the last is more specific, and hence is chosen. If there is no
+most-specific match, the program is rejected.
+</para>
+<para>
+However, GHC is conservative about committing to an overlapping instance. For example:
+<programlisting>
+ f :: [b] -> [b]
+ f x = ...
+</programlisting>
+Suppose that from the RHS of <literal>f</literal> we get the constraint
+<literal>C Int [b]</literal>. But
+GHC does not commit to instance (C), because in a particular
+call of <literal>f</literal>, <literal>b</literal> might be instantiate
+to <literal>Int</literal>, in which case instance (D) would be more specific still.
+So GHC rejects the program. If you add the flag <option>-fallow-incoherent-instances</option>,
+GHC will instead pick (C), without complaining about
+the problem of subsequent instantiations.
</para>
-</listitem>
-<listitem>
-
<para>
- OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
-(but not identical to <literal>type1</literal>), or vice versa.
-</para>
-</listitem>
-</itemizedlist>
-Notice that these rules
+The willingness to be overlapped or incoherent is a property of
+the <emphasis>instance declaration</emphasis> itself, controlled by the
+presence or otherwise of the <option>-fallow-overlapping-instances</option>
+and <option>-fallow-incoherent-instances</option> flags when that mdodule is
+being defined. Neither flag is required in a module that imports and uses the
+instance declaration. Specifically, during the lookup process:
<itemizedlist>
-<listitem>
-
-<para>
- make it clear which instance decl to use
-(pick the most specific one that matches)
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- do not mention the contexts <literal>context1</literal>, <literal>context2</literal>
-Reason: you can pick which instance decl
-"matches" based on the type.
-</para>
-</listitem>
-
+<listitem><para>
+An instance declaration is ignored during the lookup process if (a) a more specific
+match is found, and (b) the instance declaration was compiled with
+<option>-fallow-overlapping-instances</option>. The flag setting for the
+more-specific instance does not matter.
+</para></listitem>
+<listitem><para>
+Suppose an instance declaration does not matche the constraint being looked up, but
+does unify with it, so that it might match when the constraint is further
+instantiated. Usually GHC will regard this as a reason for not committing to
+some other constraint. But if the instance declaration was compiled with
+<option>-fallow-incoherent-instances</option>, GHC will skip the "does-it-unify?"
+check for that declaration.
+</para></listitem>
</itemizedlist>
-However the rules are over-conservative. Two instance declarations can overlap,
-but it can still be clear in particular situations which to use. For example:
-<programlisting>
- instance C (Int,a) where ...
- instance C (a,Bool) where ...
-</programlisting>
-These are rejected by GHC's rules, but it is clear what to do when trying
-to solve the constraint <literal>C (Int,Int)</literal> because the second instance
-cannot apply. Yell if this restriction bites you.
+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.
</para>
-<para>
-GHC is also conservative about committing to an overlapping instance. For example:
-<programlisting>
- class C a where { op :: a -> a }
- instance C [Int] where ...
- instance C a => C [a] where ...
-
- f :: C b => [b] -> [b]
- f x = op x
-</programlisting>
-From the RHS of f we get the constraint <literal>C [b]</literal>. But
-GHC does not commit to the second instance declaration, because in a paricular
-call of f, b might be instantiate to Int, so the first instance declaration
-would be appropriate. So GHC rejects the program. If you add <option>-fallow-incoherent-instances</option>
-GHC will instead silently pick the second instance, without complaining about
-the problem of subsequent instantiations.
-</para>
-<para>
-Regrettably, GHC doesn't guarantee to detect overlapping instance
-declarations if they appear in different modules. GHC can "see" the
-instance declarations in the transitive closure of all the modules
-imported by the one being compiled, so it can "see" all instance decls
-when it is compiling <literal>Main</literal>. However, it currently chooses not
-to look at ones that can't possibly be of use in the module currently
-being compiled, in the interests of efficiency. (Perhaps we should
-change that decision, at least for <literal>Main</literal>.)
+<para>The <option>-fallow-incoherent-instances</option> flag implies the
+<option>-fallow-overlapping-instances</option> flag, but not vice versa.
</para>
</sect3>
<sect2 id="implicit-parameters">
<title>Implicit parameters</title>
-<para> Implicit paramters are implemented as described in
+<para> Implicit parameters are implemented as described in
"Implicit parameters: dynamic scoping with static types",
J Lewis, MB Shields, E Meijer, J Launchbury,
27th ACM Symposium on Principles of Programming Languages (POPL'00),
</para>
</sect3>
+
+<sect3><title>Implicit parameters and polymorphic recursion</title>
+
+<para>
+Consider these two definitions:
+<programlisting>
+ len1 :: [a] -> Int
+ len1 xs = let ?acc = 0 in len_acc1 xs
+
+ len_acc1 [] = ?acc
+ len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs
+
+ ------------
+
+ len2 :: [a] -> Int
+ len2 xs = let ?acc = 0 in len_acc2 xs
+
+ len_acc2 :: (?acc :: Int) => [a] -> Int
+ len_acc2 [] = ?acc
+ len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs
+</programlisting>
+The only difference between the two groups is that in the second group
+<literal>len_acc</literal> is given a type signature.
+In the former case, <literal>len_acc1</literal> is monomorphic in its own
+right-hand side, so the implicit parameter <literal>?acc</literal> is not
+passed to the recursive call. In the latter case, because <literal>len_acc2</literal>
+has a type signature, the recursive call is made to the
+<emphasis>polymoprhic</emphasis> version, which takes <literal>?acc</literal>
+as an implicit parameter. So we get the following results in GHCi:
+<programlisting>
+ Prog> len1 "hello"
+ 0
+ Prog> len2 "hello"
+ 5
+</programlisting>
+Adding a type signature dramatically changes the result! This is a rather
+counter-intuitive phenomenon, worth watching out for.
+</para>
+</sect3>
+
+<sect3><title>Implicit parameters and monomorphism</title>
+
+<para>GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the
+Haskell Report) to implicit parameters. For example, consider:
+<programlisting>
+ f :: Int -> Int
+ f v = let ?x = 0 in
+ let y = ?x + v in
+ let ?x = 5 in
+ y
+</programlisting>
+Since the binding for <literal>y</literal> falls under the Monomorphism
+Restriction it is not generalised, so the type of <literal>y</literal> is
+simply <literal>Int</literal>, not <literal>(?x::Int) => Int</literal>.
+Hence, <literal>(f 9)</literal> returns result <literal>9</literal>.
+If you add a type signature for <literal>y</literal>, then <literal>y</literal>
+will get type <literal>(?x::Int) => Int</literal>, so the occurrence of
+<literal>y</literal> in the body of the <literal>let</literal> will see the
+inner binding of <literal>?x</literal>, so <literal>(f 9)</literal> will return
+<literal>14</literal>.
+</para>
+</sect3>
</sect2>
<sect2 id="linear-implicit-parameters">
</para>
<itemizedlist>
<listitem> <para> distributing a supply of unique names </para> </listitem>
-<listitem> <para> distributing a suppply of random numbers </para> </listitem>
+<listitem> <para> distributing a supply of random numbers </para> </listitem>
<listitem> <para> distributing an oracle (as in QuickCheck) </para> </listitem>
</itemizedlist>
</para>
<para>
The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
-the <literal>forall</literal> is on the left of a function arrrow. As <literal>g2</literal>
+the <literal>forall</literal> is on the left of a function arrow. As <literal>g2</literal>
shows, the polymorphic type on the left of the function arrow can be overloaded.
</para>
<para>
<title>Type inference</title>
<para>
-In general, type inference for arbitrary-rank types is undecideable.
+In general, type inference for arbitrary-rank types is undecidable.
GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
to get a decidable algorithm by requiring some help from the programmer.
We do not yet have a formal specification of "some help" but the rule is this:
</title>
<para>
-A <emphasis>pattern type signature</emphasis> can introduce a <emphasis>scoped type
-variable</emphasis>. For example
-</para>
-
-<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:
<programlisting>
f (xs::[a]) = ys ++ ys
where
ys :: [a]
ys = reverse xs
</programlisting>
-
-</para>
-
-<para>
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>.
</para>
<para>
- Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures. The two can be used independently or together.
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
</para>
<sect3>
-<title>What a pattern type signature means</title>
+<title>What a scoped type variable means</title>
<para>
-A type variable brought into scope by a pattern type signature is simply
-the name for a type. The restriction they express is that all occurrences
+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
</sect3>
-<sect3>
+<sect3 id="decl-type-sigs">
+<title>Declaration type signatures</title>
+<para>A declaration type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the definition of the named function(s). For example:
+<programlisting>
+ f :: forall a. [a] -> [a]
+ f (x:xs) = xs ++ [ x :: a ]
+</programlisting>
+The "<literal>forall a</literal>" brings "<literal>a</literal>" into scope in
+the definition of "<literal>f</literal>".
+</para>
+<para>This only happens if the quantification in <literal>f</literal>'s type
+signature is explicit. For example:
+<programlisting>
+ g :: [a] -> [a]
+ g (x:xs) = xs ++ [ x :: a ]
+</programlisting>
+This program will be rejected, because "<literal>a</literal>" does not scope
+over the definition of "<literal>f</literal>", so "<literal>x::a</literal>"
+means "<literal>x::forall a. a</literal>" by Haskell's usual implicit
+quantification rules.
+</para>
+</sect3>
+
+<sect3 id="pattern-type-sigs">
<title>Where a pattern type signature can occur</title>
<para>
<listitem>
<para>
A pattern type signature can be on an arbitrary sub-pattern, not
-ust on a variable:
+just on a variable:
<programlisting>
</listitem>
</itemizedlist>
</para>
+<para>Pattern type signatures are completely orthogonal to ordinary, separate
+type signatures. The two can be used independently or together.</para>
</sect3>
-<sect3>
+<sect3 id="result-type-sigs">
<title>Result type signatures</title>
<para>
GHC extends this list with two more classes that may be automatically derived
(provided the <option>-fglasgow-exts</option> flag is specified):
<literal>Typeable</literal>, and <literal>Data</literal>. These classes are defined in the library
-modules <literal>Data.Dynamic</literal> and <literal>Data.Generics</literal> respectively, and the
+modules <literal>Data.Typeable</literal> and <literal>Data.Generics</literal> respectively, and the
appropriate class must be in scope before it can be mentioned in the <literal>deriving</literal> clause.
</para>
</sect2>
<para>
As a result of this extension, all derived instances in newtype
-declarations are treated uniformly (and implemented just by reusing
+ declarations are treated uniformly (and implemented just by reusing
the dictionary for the representation type), <emphasis>except</emphasis>
<literal>Show</literal> and <literal>Read</literal>, which really behave differently for
the newtype and its representation.
classes usually have one "main" parameter for which deriving new
instances is most interesting.
</para>
+<para>Lastly, all of this applies only for classes other than
+<literal>Read</literal>, <literal>Show</literal>, <literal>Typeable</literal>,
+and <literal>Data</literal>, for which the built-in derivation applies (section
+4.3.3. of the Haskell Report).
+(For the standard classes <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Ix</literal>, and <literal>Bounded</literal> it is immaterial whether
+the standard method is used or the one described here.)
+</para>
</sect3>
</sect2>
+<sect2 id="typing-binds">
+<title>Generalised typing of mutually recursive bindings</title>
+
+<para>
+The Haskell Report specifies that a group of bindings (at top level, or in a
+<literal>let</literal> or <literal>where</literal>) should be sorted into
+strongly-connected components, and then type-checked in dependency order
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.1">Haskell
+Report, Section 4.5.1</ulink>).
+As each group is type-checked, any binders of the group that
+have
+an explicit type signature are put in the type environment with the specified
+polymorphic type,
+and all others are monomorphic until the group is generalised
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.2">Haskell Report, Section 4.5.2</ulink>).
+</para>
+
+<para>Following a suggestion of Mark Jones, in his paper
+<ulink url="http://www.cse.ogi.edu/~mpj/thih/">Typing Haskell in
+Haskell</ulink>,
+GHC implements a more general scheme. If <option>-fglasgow-exts</option> is
+specified:
+<emphasis>the dependency analysis ignores references to variables that have an explicit
+type signature</emphasis>.
+As a result of this refined dependency analysis, the dependency groups are smaller, and more bindings will
+typecheck. For example, consider:
+<programlisting>
+ f :: Eq a => a -> Bool
+ f x = (x == x) || g True || g "Yes"
+
+ g y = (y <= y) || f True
+</programlisting>
+This is rejected by Haskell 98, but under Jones's scheme the definition for
+<literal>g</literal> is typechecked first, separately from that for
+<literal>f</literal>,
+because the reference to <literal>f</literal> in <literal>g</literal>'s right
+hand side is ingored by the dependency analysis. Then <literal>g</literal>'s
+type is generalised, to get
+<programlisting>
+ g :: Ord a => a -> Bool
+</programlisting>
+Now, the defintion for <literal>f</literal> is typechecked, with this type for
+<literal>g</literal> in the type environment.
+</para>
+
+<para>
+The same refined dependency analysis also allows the type signatures of
+mutually-recursive functions to have different contexts, something that is illegal in
+Haskell 98 (Section 4.5.2, last sentence). With
+<option>-fglasgow-exts</option>
+GHC only insists that the type signatures of a <emphasis>refined</emphasis> group have identical
+type signatures; in practice this means that only variables bound by the same
+pattern binding must have the same context. For example, this is fine:
+<programlisting>
+ f :: Eq a => a -> Bool
+ f x = (x == x) || g True
+
+ g :: Ord a => a -> Bool
+ g y = (y <= y) || f True
+</programlisting>
+</para>
+</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 i) = eval i == 0
+ eval (If b e1 e2) = if eval b then eval e1 else eval e2
+ eval (Pair e1 e2) = (eval e2, 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 cannot use record syntax on a GADT-style data type declaration. (
+It's not clear what these it would mean. For example,
+the record selectors might ill-typed.)
+However, 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>
+
+<para>Notice that GADTs generalise existential types. For example, these two declarations are equivalent:
+<programlisting>
+ data T a = forall b. MkT b (b->a)
+ data T' a where { MKT :: b -> (b->a) -> T' a }
+</programlisting>
+</para>
+</sect1>
+
+<!-- ====================== End of Generalised algebraic data types ======================= -->
+
<!-- ====================== TEMPLATE HASKELL ======================= -->
<sect1 id="template-haskell">
<itemizedlist>
<listitem><para> an expression; the spliced expression must have type <literal>Expr</literal></para></listitem>
<listitem><para> a list of top-level declarations; ; the spliced expression must have type <literal>Q [Dec]</literal></para></listitem>
- <listitem><para> a type; the spliced expression must have type <literal>Type</literal>.</para></listitem>
+ <listitem><para> [Planned, but not implemented yet.] a type; the spliced expression must have type <literal>Type</literal>.</para></listitem>
</itemizedlist>
(Note that the syntax for a declaration splice uses "<literal>$</literal>" not "<literal>splice</literal>" as in
the paper. Also the type of the enclosed expression must be <literal>Q [Dec]</literal>, not <literal>[Q Dec]</literal>
the quotation has type <literal>Expr</literal>.</para></listitem>
<listitem><para> <literal>[d| ... |]</literal>, where the "..." is a list of top-level declarations;
the quotation has type <literal>Q [Dec]</literal>.</para></listitem>
- <listitem><para> <literal>[t| ... |]</literal>, where the "..." is a type;
+ <listitem><para> [Planned, but not implemented yet.] <literal>[t| ... |]</literal>, where the "..." is a type;
the quotation has type <literal>Type</literal>.</para></listitem>
</itemizedlist></para></listitem>
-- you intend to use it.
-- Import some Template Haskell syntax
-import Language.Haskell.TH.Syntax
+import Language.Haskell.TH
-- Describe a format string
data Format = D | S | L String
</screen>
which is equivalent to
<screen>
-arr (\ x -> (f, x+1)) >>> app
+arr (\ x -> (f x, x+1)) >>> app
</screen>
so in this case the arrow must belong to the <literal>ArrowApply</literal>
class.
</listitem>
<listitem>
- <para>You can deprecate a function, class, or type, with the
+ <para>You can deprecate a function, class, type, or data constructor, with the
following top-level declaration:</para>
<programlisting>
{-# DEPRECATED f, C, T "Don't use these" #-}
</programlisting>
<para>When you compile any module that imports and uses any
- of the specifed entities, GHC will print the specified
+ of the specified entities, GHC will print the specified
message.</para>
+ <para> You can only depecate entities declared at top level in the module
+ being compiled, and you can only use unqualified names in the list of
+ entities being deprecated. A capitalised name, such as <literal>T</literal>
+ refers to <emphasis>either</emphasis> the type constructor <literal>T</literal>
+ <emphasis>or</emphasis> the data constructor <literal>T</literal>, or both if
+ both are in scope. If both are in scope, there is currently no way to deprecate
+ one without the other (c.f. fixities <xref linkend="infix-tycons"/>).</para>
</listitem>
</itemizedlist>
Any use of the deprecated item, or of anything from a deprecated
<option>-fno-warn-deprecations</option>.</para>
</sect2>
+ <sect2 id="include-pragma">
+ <title>INCLUDE pragma</title>
+
+ <para>The <literal>INCLUDE</literal> pragma is for specifying the names
+ of C header files that should be <literal>#include</literal>'d into
+ the C source code generated by the compiler for the current module (if
+ compiling via C). For example:</para>
+
+<programlisting>
+{-# INCLUDE "foo.h" #-}
+{-# INCLUDE <stdio.h> #-}</programlisting>
+
+ <para>The <literal>INCLUDE</literal> pragma(s) must appear at the top of
+ your source file with any <literal>OPTIONS_GHC</literal>
+ pragma(s).</para>
+
+ <para>An <literal>INCLUDE</literal> pragma is the preferred alternative
+ to the <option>-#include</option> option (<xref
+ linkend="options-C-compiler" />), because the
+ <literal>INCLUDE</literal> pragma is understood by other
+ compilers. Yet another alternative is to add the include file to each
+ <literal>foreign import</literal> declaration in your code, but we
+ don't recommend using this approach with GHC.</para>
+ </sect2>
+
<sect2 id="inline-noinline-pragma">
<title>INLINE and NOINLINE pragmas</title>
The normal unfolding machinery will then be very keen to
inline it.</para>
- <para>Syntactially, an <literal>INLINE</literal> pragma for a
+ <para>Syntactically, an <literal>INLINE</literal> pragma for a
function can be put anywhere its type signature could be
put.</para>
you're very cautious about code size.</para>
<para><literal>NOTINLINE</literal> is a synonym for
- <literal>NOINLINE</literal> (<literal>NOTINLINE</literal> is
+ <literal>NOINLINE</literal> (<literal>NOINLINE</literal> is
specified by Haskell 98 as the standard way to disable
inlining, so it should be used if you want your code to be
portable).</para>
number</emphasis>; the phase number decreases towards zero.
If you use <option>-dverbose-core2core</option> you'll see the
sequence of phase numbers for successive runs of the
- simpifier. In an INLINE pragma you can optionally specify a
+ simplifier. In an INLINE pragma you can optionally specify a
phase number, thus:</para>
<itemizedlist>
</sect2>
<sect2 id="options-pragma">
- <title>OPTIONS pragma</title>
- <indexterm><primary>OPTIONS</primary>
+ <title>OPTIONS_GHC pragma</title>
+ <indexterm><primary>OPTIONS_GHC</primary>
</indexterm>
- <indexterm><primary>pragma</primary><secondary>OPTIONS</secondary>
+ <indexterm><primary>pragma</primary><secondary>OPTIONS_GHC</secondary>
</indexterm>
- <para>The <literal>OPTIONS</literal> pragma is used to specify
+ <para>The <literal>OPTIONS_GHC</literal> pragma is used to specify
additional options that are given to the compiler when compiling
this source file. See <xref linkend="source-file-options"/> for
details.</para>
+
+ <para>Previous versions of GHC accepted <literal>OPTIONS</literal> rather
+ than <literal>OPTIONS_GHC</literal>, but that is now deprecated.</para>
</sect2>
<sect2 id="rules">
overloaded function:</para>
<programlisting>
-hammeredLookup :: Ord key => [(key, value)] -> key -> value
+ hammeredLookup :: Ord key => [(key, value)] -> key -> value
</programlisting>
<para>If it is heavily used on lists with
follows:</para>
<programlisting>
-{-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
+ {-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
</programlisting>
<para>A <literal>SPECIALIZE</literal> pragma for a function can
(see <xref linkend="rewrite-rules"/>) that rewrites a call to the
un-specialised function into a call to the specialised one.</para>
- <para>In earlier versions of GHC, it was possible to provide your own
+ <para>The type in a SPECIALIZE pragma can be any type that is less
+ polymorphic than the type of the original function. In concrete terms,
+ if the original function is <literal>f</literal> then the pragma
+<programlisting>
+ {-# SPECIALIZE f :: <type> #-}
+</programlisting>
+ is valid if and only if the defintion
+<programlisting>
+ f_spec :: <type>
+ f_spec = f
+</programlisting>
+ is valid. Here are some examples (where we only give the type signature
+ for the original function, not its code):
+<programlisting>
+ f :: Eq a => a -> b -> b
+ {-# SPECIALISE g :: Int -> b -> b #-}
+
+ g :: (Eq a, Ix b) => a -> b -> b
+ {-# SPECIALISE g :: (Eq a) => a -> Int -> Int #-}
+
+ h :: Eq a => a -> a -> a
+ {-# SPECIALISE h :: (Eq a) => [a] -> [a] -> [a] #-}
+</programlisting>
+The last of these examples will generate a
+RULE with a somewhat-complex left-hand side (try it yourself), so it might not fire very
+well. If you use this kind of specialisation, let us know how well it works.
+</para>
+
+ <para>Note: In earlier versions of GHC, it was possible to provide your own
specialised function for a given type:
<programlisting>
<sect1 id="rewrite-rules">
<title>Rewrite rules
-<indexterm><primary>RULES pagma</primary></indexterm>
+<indexterm><primary>RULES pragma</primary></indexterm>
<indexterm><primary>pragma, RULES</primary></indexterm>
<indexterm><primary>rewrite rules</primary></indexterm></title>
<para>
GHC makes absolutely no attempt to verify that the LHS and RHS
-of a rule have the same meaning. That is undecideable in general, and
+of a rule have the same meaning. That is undecidable in general, and
infeasible in most interesting cases. The responsibility is entirely the programmer's!
</para>
for matching a rule LHS with an expression. It seeks a substitution
which makes the LHS and expression syntactically equal modulo alpha
conversion. The pattern (rule), but not the expression, is eta-expanded if
-necessary. (Eta-expanding the epression can lead to laziness bugs.)
+necessary. (Eta-expanding the expression can lead to laziness bugs.)
But not beta conversion (that's called higher-order matching).
</para>
<listitem>
<para>
- The defintion of (say) <function>build</function> in <filename>GHC/Base.lhs</filename> looks llike this:
+ The definition of (say) <function>build</function> in <filename>GHC/Base.lhs</filename> looks llike this:
<programlisting>
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
f x = ({-# CORE "foo" #-} show) ({-# CORE "bar" #-} x)
</programlisting>
- Sematically, this is equivalent to:
+ Semantically, this is equivalent to:
<programlisting>
g x = show x