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>
<listitem>
- <para>Similarly recursive do notation (see
- <xref linkend="mdo-notation"/>) uses whatever
- <literal>mfix</literal> function is in scope, and arrow
+ <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.</para>
- </listitem>
+ <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>
-
- <para>The functions with these names that GHC finds in scope
- must have types matching those of the originals, namely:
- <screen>
- fromInteger :: Integer -> N
- fromRational :: Rational -> N
- negate :: N -> N
- (-) :: N -> N -> N
- (>>=) :: forall a b. M a -> (a -> M b) -> M b
- (>>) :: forall a b. M a -> M b -> M b
- return :: forall a. a -> M a
- fail :: forall a. String -> M a
- </screen>
- (Here <literal>N</literal> may be any type,
- and <literal>M</literal> any type constructor.)</para>
-
+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
</sect3>
<sect3 id="infix-tycons">
-<title>Infix type constructors and classes</title>
+<title>Infix type constructors, classes, and type variables</title>
<para>
-GHC allows type constructors and classes 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 or class can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
</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
as for expressions, both for type constructors and type variables; e.g. <literal>Int `Either` Bool</literal>, or
<literal>Int `a` Bool</literal>. Similarly, parentheses work the same; e.g. <literal>(:*:) Int Bool</literal>.
<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>
- 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>
<para>
The idea of using existential quantification in data type declarations
-was suggested by Laufer (I believe, thought doubtless someone will
-correct me), and implemented in Hope+. It's been in Lennart
+was suggested by Perry, and implemented in Hope+ (Nigel Perry, <emphasis>The Implementation
+of Practical Functional Programming Languages</emphasis>, PhD Thesis, University of
+London, 1991). It was later formalised by Laufer and Odersky
+(<emphasis>Polymorphic type inference and abstract data types</emphasis>,
+TOPLAS, 16(5), pp1411-1430, 1994).
+It's been in Lennart
Augustsson's <command>hbc</command> Haskell compiler for several years, and
proved very useful. Here's the idea. Consider the declaration:
</para>
<title>Type classes</title>
<para>
-An easy extension (implemented in <command>hbc</command>) is to allow
+An easy extension is to allow
arbitrary contexts before the constructor. For example:
</para>
</sect4>
<sect4>
+<title>Record Constructors</title>
+
+<para>
+GHC allows existentials to be used with records syntax as well. For example:
+
+<programlisting>
+data Counter a = forall self. NewCounter
+ { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+</programlisting>
+Here <literal>tag</literal> is a public field, with a well-typed selector
+function <literal>tag :: Counter a -> a</literal>. The <literal>self</literal>
+type is hidden from the outside; any attempt to apply <literal>_this</literal>,
+<literal>_inc</literal> or <literal>_output</literal> as functions will raise a
+compile-time error. In other words, <emphasis>GHC defines a record selector function
+only for fields whose type does not mention the existentially-quantified variables</emphasis>.
+(This example used an underscore in the fields for which record selectors
+will not be defined, but that is only programming style; GHC ignores them.)
+</para>
+
+<para>
+To make use of these hidden fields, we need to create some helper functions:
+
+<programlisting>
+inc :: Counter a -> Counter a
+inc (NewCounter x i d t) = NewCounter
+ { _this = i x, _inc = i, _display = d, tag = t }
+
+display :: Counter a -> IO ()
+display NewCounter{ _this = x, _display = d } = d x
+</programlisting>
+
+Now we can define counters with different underlying implementations:
+
+<programlisting>
+counterA :: Counter String
+counterA = NewCounter
+ { _this = 0, _inc = (1+), _display = print, tag = "A" }
+
+counterB :: Counter String
+counterB = NewCounter
+ { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
+
+main = do
+ display (inc counterA) -- prints "1"
+ display (inc (inc counterB)) -- prints "##"
+</programlisting>
+
+In GADT declarations (see <xref linkend="gadt"/>), the explicit
+<literal>forall</literal> may be omitted. For example, we can express
+the same <literal>Counter a</literal> using GADT:
+
+<programlisting>
+data Counter a where
+ NewCounter { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+ :: Counter a
+</programlisting>
+
+At the moment, record update syntax is only supported for Haskell 98 data types,
+so the following function does <emphasis>not</emphasis> work:
+
+<programlisting>
+-- This is invalid; use explicit NewCounter instead for now
+setTag :: Counter a -> a -> Counter a
+setTag obj t = obj{ tag = t }
+</programlisting>
+
+</para>
+
+</sect4>
+
+
+<sect4>
<title>Restrictions</title>
<para>
<title>Class declarations</title>
<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
+This section, and the next one, documents GHC's type-class extensions.
+There's lots of background in the paper <ulink
+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>
-There are the following constraints on class declarations:
-<orderedlist>
-<listitem>
+All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
+</para>
+<sect3>
+<title>Multi-parameter type classes</title>
<para>
- <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+Multi-parameter type classes are permitted. For example:
<programlisting>
...etc.
</programlisting>
+</para>
+</sect3>
+
+<sect3>
+<title>The superclasses of a class declaration</title>
+<para>
+There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic. So these class declarations are OK:
-</para>
-</listitem>
-<listitem>
+<programlisting>
+ class Functor (m k) => FiniteMap m k where
+ ...
+
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
+</programlisting>
+
+
+</para>
<para>
- <emphasis>The class hierarchy must be acyclic</emphasis>. However, the definition
+As in Haskell 98, The class hierarchy must be acyclic. However, the definition
of "acyclic" involves only the superclass relationships. For example,
this is OK:
Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>. (It
would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
-
</para>
-</listitem>
-<listitem>
+</sect3>
-<para>
- <emphasis>There are no restrictions on the context in a class declaration
-(which introduces superclasses), except that the class hierarchy must
-be acyclic</emphasis>. So these class declarations are OK:
-<programlisting>
- class Functor (m k) => FiniteMap m k where
- ...
- class (Monad m, Monad (t m)) => Transform t m where
- lift :: m a -> (t m) a
+<sect3 id="class-method-types">
+<title>Class method types</title>
+
+<para>
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
+<programlisting>
+ class Seq s a where
+ fromList :: [a] -> s a
+ elem :: Eq a => a -> s a -> Bool
</programlisting>
+The type of <literal>elem</literal> is illegal in Haskell 98, because it
+contains the constraint <literal>Eq a</literal>, constrains only the
+class type variable (in this case <literal>a</literal>).
+GHC lifts this restriction.
+</para>
-</para>
-</listitem>
+</sect3>
-<listitem>
+<sect3 id="functional-dependencies">
+<title>Functional dependencies
+</title>
+
+<para> Functional dependencies are implemented as described by Mark Jones
+in “<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>”, Mark P. Jones,
+In Proceedings of the 9th European Symposium on Programming,
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
+.
+</para>
<para>
- <emphasis>All of the class type variables must be reachable (in the sense
-mentioned in <xref linkend="type-restrictions"/>)
-from the free variables of each method type
-</emphasis>. For example:
+Functional dependencies are introduced by a vertical bar in the syntax of a
+class declaration; e.g.
+<programlisting>
+ class (Monad m) => MonadState s m | m -> s where ...
+ class Foo a b c | a b -> c where ...
+</programlisting>
+There should be more documentation, but there isn't (yet). Yell if you need it.
+</para>
+<para>
+In a class declaration, all of the class type variables must be reachable (in the sense
+mentioned in <xref linkend="type-restrictions"/>)
+from the free variables of each method type.
+For example:
<programlisting>
class Coll s a where
insert :: s -> a -> s
</programlisting>
-
is not OK, because the type of <literal>empty</literal> doesn't mention
-<literal>a</literal>. This rule is a consequence of Rule 1(a), above, for
-types, and has the same motivation.
-
-Sometimes, offending class declarations exhibit misunderstandings. For
-example, <literal>Coll</literal> might be rewritten
+<literal>a</literal>. Functional dependencies can make the type variable
+reachable:
+<programlisting>
+ class Coll s a | s -> a where
+ empty :: s
+ insert :: s -> a -> s
+</programlisting>
+Alternatively <literal>Coll</literal> might be rewritten
<programlisting>
class Coll s a where
class CollE s => Coll s a where
insert :: s -> a -> s
</programlisting>
+</para>
+</sect3>
-</para>
-</listitem>
-</orderedlist>
-</para>
-<sect3 id="class-method-types">
-<title>Class method types</title>
+
+</sect2>
+
+<sect2 id="instance-decls">
+<title>Instance declarations</title>
+
+<sect3 id="instance-heads">
+<title>Instance heads</title>
+
<para>
-Haskell 98 prohibits class method types to mention constraints on the
-class type variable, thus:
-<programlisting>
- class Seq s a where
- fromList :: [a] -> s a
- elem :: Eq a => a -> s a -> Bool
-</programlisting>
-The type of <literal>elem</literal> is illegal in Haskell 98, because it
-contains the constraint <literal>Eq a</literal>, constrains only the
-class type variable (in this case <literal>a</literal>).
+The <emphasis>head</emphasis> of an instance declaration is the part to the
+right of the "<literal>=></literal>". In Haskell 98 the head of an instance
+declaration
+must be of the form <literal>C (T a1 ... an)</literal>, where
+<literal>C</literal> is the class, <literal>T</literal> is a type constructor,
+and the <literal>a1 ... an</literal> are distinct type variables.
</para>
<para>
-With the <option>-fglasgow-exts</option> GHC lifts this restriction.
-</para>
-
-</sect3>
+The <option>-fglasgow-exts</option> flag lifts this restriction and allows the
+instance head to be of form <literal>C t1 ... tn</literal> where <literal>t1
+... tn</literal> are arbitrary types (provided, of course, everything is
+well-kinded). In particular, types <literal>ti</literal> can be type variables
+or structured types, and can contain repeated occurrences of a single type
+variable.
+Examples:
+<programlisting>
+ instance Eq (T a a) where ...
+ -- Repeated type variable
-</sect2>
+ instance Eq (S [a]) where ...
+ -- Structured type
-<sect2 id="type-restrictions">
-<title>Type signatures</title>
+ instance C Int [a] where ...
+ -- Multiple parameters
+</programlisting>
+</para>
+</sect3>
-<sect3><title>The context of a type signature</title>
+<sect3 id="instance-overlap">
+<title>Overlapping instances</title>
<para>
-Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
-the form <emphasis>(class type-variable)</emphasis> or
-<emphasis>(class (type-variable type-variable ...))</emphasis>. Thus,
-these type signatures are perfectly OK
+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>
- g :: Eq [a] => ...
- g :: Ord (T a ()) => ...
+ 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>
-GHC imposes the following restrictions on the constraints in a type signature.
-Consider the type:
+<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>
- forall tv1..tvn (c1, ...,cn) => type
+ f :: [b] -> [b]
+ f x = ...
</programlisting>
-
-(Here, we write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 98, all the free type variables of an
-explicit source-language type signature are universally quantified,
-except for the class type variables in a class declaration. However,
-in GHC, you can give the foralls if you want. See <xref linkend="universal-quantification"/>).
+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>
-
<para>
+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>
+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>
+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>The <option>-fallow-incoherent-instances</option> flag implies the
+<option>-fallow-overlapping-instances</option> flag, but not vice versa.
+</para>
+</sect3>
-<orderedlist>
-<listitem>
+<sect3>
+<title>Type synonyms in the instance head</title>
<para>
- <emphasis>Each universally quantified type variable
-<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
-
-A type variable <literal>a</literal> is "reachable" if it it appears
-in the same constraint as either a type variable free in in
-<literal>type</literal>, or another reachable type variable.
-A value with a type that does not obey
-this reachability restriction cannot be used without introducing
-ambiguity; that is why the type is rejected.
-Here, for example, is an illegal type:
+<emphasis>Unlike Haskell 98, instance heads may use type
+synonyms</emphasis>. (The instance "head" is the bit after the "=>" in an instance decl.)
+As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition. For example:
<programlisting>
- forall a. Eq a => Int
-</programlisting>
-
-
-When a value with this type was used, the constraint <literal>Eq tv</literal>
-would be introduced where <literal>tv</literal> is a fresh type variable, and
-(in the dictionary-translation implementation) the value would be
-applied to a dictionary for <literal>Eq tv</literal>. The difficulty is that we
-can never know which instance of <literal>Eq</literal> to use because we never
-get any more information about <literal>tv</literal>.
-</para>
-<para>
-Note
-that the reachability condition is weaker than saying that <literal>a</literal> is
-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
-"reachable" is a conservative approximation to "functionally dependent".
-For example, consider:
-<programlisting>
- class C a b | a -> b where ...
- class C a b => D a b where ...
- f :: forall a b. D a b => a -> a
+ type Point = (Int,Int)
+ instance C Point where ...
+ instance C [Point] where ...
</programlisting>
-This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
-but that is not immediately apparent from <literal>f</literal>'s type.
-</para>
-</listitem>
-<listitem>
-<para>
- <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
-universally quantified type variables <literal>tvi</literal></emphasis>.
-For example, this type is OK because <literal>C a b</literal> mentions the
-universally quantified type variable <literal>b</literal>:
+is legal. However, if you added
<programlisting>
- forall a. C a b => burble
+ instance C (Int,Int) where ...
</programlisting>
-The next type is illegal because the constraint <literal>Eq b</literal> does not
-mention <literal>a</literal>:
+as well, then the compiler will complain about the overlapping
+(actually, identical) instance declarations. As always, type synonyms
+must be fully applied. You cannot, for example, write:
<programlisting>
- forall a. Eq b => burble
+ type P a = [[a]]
+ instance Monad P where ...
</programlisting>
-The reason for this restriction is milder than the other one. The
-excluded types are never useful or necessary (because the offending
-context doesn't need to be witnessed at this point; it can be floated
-out). Furthermore, floating them out increases sharing. Lastly,
-excluding them is a conservative choice; it leaves a patch of
-territory free in case we need it later.
+This design decision is independent of all the others, and easily
+reversed, but it makes sense to me.
</para>
-</listitem>
+</sect3>
-</orderedlist>
+<sect3 id="undecidable-instances">
+<title>Undecidable instances</title>
-</para>
-</sect3>
+<para>An instance declaration must normally obey the following rules:
+<orderedlist>
+<listitem><para>At least one of the types in the <emphasis>head</emphasis> of
+an instance declaration <emphasis>must not</emphasis> be a type variable.
+For example, these are OK:
-<sect3 id="hoist">
-<title>For-all hoisting</title>
-<para>
-It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
-end of an arrow, thus:
<programlisting>
- type Discard a = forall b. a -> b -> a
+ instance C Int a where ...
- g :: Int -> Discard Int
- g x y z = x+y
+ instance D (Int, Int) where ...
+
+ instance E [[a]] where ...
</programlisting>
-Simply expanding the type synonym would give
+but this is not:
<programlisting>
- g :: Int -> (forall b. Int -> b -> Int)
+ instance F a where ...
</programlisting>
-but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
+Note that instance heads may contain repeated type variables (<xref linkend="instance-heads"/>).
+For example, this is OK:
<programlisting>
- g :: forall b. Int -> Int -> b -> Int
+ instance Stateful (ST s) (MutVar s) where ...
</programlisting>
-In general, the rule is this: <emphasis>to determine the type specified by any explicit
-user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
-performs the transformation:</emphasis>
+</para>
+</listitem>
+
+
+<listitem>
+<para>All of the types in the <emphasis>context</emphasis> of
+an instance declaration <emphasis>must</emphasis> be type variables, and
+there must be no repeated type variables in any one constraint.
+Thus
<programlisting>
- <emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
-==>
- forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
+instance C a b => Eq (a,b) where ...
</programlisting>
-(In fact, GHC tries to retain as much synonym information as possible for use in
-error messages, but that is a usability issue.) This rule applies, of course, whether
-or not the <literal>forall</literal> comes from a synonym. For example, here is another
-valid way to write <literal>g</literal>'s type signature:
+is OK, but
<programlisting>
- g :: Int -> Int -> forall b. b -> Int
+instance C Int b => Foo [b] where ...
+</programlisting>
+is not OK (because of the non-type-variable <literal>Int</literal> in the context), and nor is
+<programlisting>
+instance C b b => Foo [b] where ...
</programlisting>
+(because of the repeated type variable).
</para>
-<para>
-When doing this hoisting operation, GHC eliminates duplicate constraints. For
-example:
+</listitem>
+</orderedlist>
+These restrictions ensure that
+context reduction terminates: each reduction step removes one type
+constructor. For example, the following would make the type checker
+loop if it wasn't excluded:
<programlisting>
- type Foo a = (?x::Int) => Bool -> a
- g :: Foo (Foo Int)
+ instance C a => C a where ...
</programlisting>
-means
+There are two situations in which the rule is a bit of a pain. First,
+if one allows overlapping instance declarations then it's quite
+convenient to have a "default instance" declaration that applies if
+something more specific does not:
+
+
<programlisting>
- g :: (?x::Int) => Bool -> Bool -> Int
+ instance C a where
+ op = ... -- Default
</programlisting>
+
+
+Second, sometimes you might want to use the following to get the
+effect of a "class synonym":
+
+
+<programlisting>
+ class (C1 a, C2 a, C3 a) => C a where { }
+
+ instance (C1 a, C2 a, C3 a) => C a where { }
+</programlisting>
+
+
+This allows you to write shorter signatures:
+
+
+<programlisting>
+ f :: C a => ...
+</programlisting>
+
+
+instead of
+
+
+<programlisting>
+ f :: (C1 a, C2 a, C3 a) => ...
+</programlisting>
+
+
+Voluminous correspondence on the Haskell mailing list has convinced me
+that it's worth experimenting with more liberal rules. If you use
+the experimental flag <option>-fallow-undecidable-instances</option>
+<indexterm><primary>-fallow-undecidable-instances
+option</primary></indexterm>, you can use arbitrary
+types in both an instance context and instance head. Termination is ensured by having a
+fixed-depth recursion stack. If you exceed the stack depth you get a
+sort of backtrace, and the opportunity to increase the stack depth
+with <option>-fcontext-stack</option><emphasis>N</emphasis>.
+</para>
+<para>
+I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
+allowing these idioms interesting idioms.
</para>
</sect3>
</sect2>
-<sect2 id="instance-decls">
-<title>Instance declarations</title>
+<sect2 id="type-restrictions">
+<title>Type signatures</title>
-<sect3>
-<title>Overlapping instances</title>
-<para>
-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>
+<sect3><title>The context of a type signature</title>
<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:
+Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
+the form <emphasis>(class type-variable)</emphasis> or
+<emphasis>(class (type-variable type-variable ...))</emphasis>. Thus,
+these type signatures are perfectly OK
<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)
+ g :: Eq [a] => ...
+ g :: Ord (T a ()) => ...
</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:
+GHC imposes the following restrictions on the constraints in a type signature.
+Consider the type:
+
<programlisting>
- f :: [b] -> [b]
- f x = ...
+ forall tv1..tvn (c1, ...,cn) => type
</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.
+
+(Here, we write the "foralls" explicitly, although the Haskell source
+language omits them; in Haskell 98, all the free type variables of an
+explicit source-language type signature are universally quantified,
+except for the class type variables in a class declaration. However,
+in GHC, you can give the foralls if you want. See <xref linkend="universal-quantification"/>).
</para>
-</sect3>
-<sect3>
-<title>Type synonyms in the instance head</title>
+<para>
+
+<orderedlist>
+<listitem>
<para>
-<emphasis>Unlike Haskell 98, instance heads may use type
-synonyms</emphasis>. (The instance "head" is the bit after the "=>" in an instance decl.)
-As always, using a type synonym is just shorthand for
-writing the RHS of the type synonym definition. For example:
+ <emphasis>Each universally quantified type variable
+<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
+
+A type variable <literal>a</literal> is "reachable" if it it appears
+in the same constraint as either a type variable free in in
+<literal>type</literal>, or another reachable type variable.
+A value with a type that does not obey
+this reachability restriction cannot be used without introducing
+ambiguity; that is why the type is rejected.
+Here, for example, is an illegal type:
<programlisting>
- type Point = (Int,Int)
- instance C Point where ...
- instance C [Point] where ...
+ forall a. Eq a => Int
+</programlisting>
+
+
+When a value with this type was used, the constraint <literal>Eq tv</literal>
+would be introduced where <literal>tv</literal> is a fresh type variable, and
+(in the dictionary-translation implementation) the value would be
+applied to a dictionary for <literal>Eq tv</literal>. The difficulty is that we
+can never know which instance of <literal>Eq</literal> to use because we never
+get any more information about <literal>tv</literal>.
+</para>
+<para>
+Note
+that the reachability condition is weaker than saying that <literal>a</literal> is
+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
+"reachable" is a conservative approximation to "functionally dependent".
+For example, consider:
+<programlisting>
+ class C a b | a -> b where ...
+ class C a b => D a b where ...
+ f :: forall a b. D a b => a -> a
</programlisting>
+This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
+but that is not immediately apparent from <literal>f</literal>'s type.
+</para>
+</listitem>
+<listitem>
+<para>
+ <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
+universally quantified type variables <literal>tvi</literal></emphasis>.
-is legal. However, if you added
+For example, this type is OK because <literal>C a b</literal> mentions the
+universally quantified type variable <literal>b</literal>:
<programlisting>
- instance C (Int,Int) where ...
+ forall a. C a b => burble
</programlisting>
-as well, then the compiler will complain about the overlapping
-(actually, identical) instance declarations. As always, type synonyms
-must be fully applied. You cannot, for example, write:
+The next type is illegal because the constraint <literal>Eq b</literal> does not
+mention <literal>a</literal>:
<programlisting>
- type P a = [[a]]
- instance Monad P where ...
+ forall a. Eq b => burble
</programlisting>
-This design decision is independent of all the others, and easily
-reversed, but it makes sense to me.
+The reason for this restriction is milder than the other one. The
+excluded types are never useful or necessary (because the offending
+context doesn't need to be witnessed at this point; it can be floated
+out). Furthermore, floating them out increases sharing. Lastly,
+excluding them is a conservative choice; it leaves a patch of
+territory free in case we need it later.
</para>
-</sect3>
+</listitem>
-<sect3 id="undecidable-instances">
-<title>Undecidable instances</title>
+</orderedlist>
-<para>An instance declaration must normally obey the following rules:
-<orderedlist>
-<listitem><para>At least one of the types in the <emphasis>head</emphasis> of
-an instance declaration <emphasis>must not</emphasis> be a type variable.
-For example, these are OK:
+</para>
+</sect3>
+<sect3 id="hoist">
+<title>For-all hoisting</title>
+<para>
+It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
+end of an arrow, thus:
<programlisting>
- instance C Int a where ...
-
- instance D (Int, Int) where ...
+ type Discard a = forall b. a -> b -> a
- instance E [[a]] where ...
+ g :: Int -> Discard Int
+ g x y z = x+y
</programlisting>
-but this is not:
+Simply expanding the type synonym would give
<programlisting>
- instance F a where ...
+ g :: Int -> (forall b. Int -> b -> Int)
</programlisting>
-Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
-For example, this is OK:
+but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
<programlisting>
- instance Stateful (ST s) (MutVar s) where ...
+ g :: forall b. Int -> Int -> b -> Int
</programlisting>
-</para>
-</listitem>
-
-
-<listitem>
-<para>All of the types in the <emphasis>context</emphasis> of
-an instance declaration <emphasis>must</emphasis> be type variables.
-Thus
+In general, the rule is this: <emphasis>to determine the type specified by any explicit
+user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
+performs the transformation:</emphasis>
<programlisting>
-instance C a b => Eq (a,b) where ...
+ <emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
+==>
+ forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
</programlisting>
-is OK, but
+(In fact, GHC tries to retain as much synonym information as possible for use in
+error messages, but that is a usability issue.) This rule applies, of course, whether
+or not the <literal>forall</literal> comes from a synonym. For example, here is another
+valid way to write <literal>g</literal>'s type signature:
<programlisting>
-instance C Int b => Foo b where ...
+ g :: Int -> Int -> forall b. b -> Int
</programlisting>
-is not OK.
</para>
-</listitem>
-</orderedlist>
-These restrictions ensure that
-context reduction terminates: each reduction step removes one type
-constructor. For example, the following would make the type checker
-loop if it wasn't excluded:
-<programlisting>
- instance C a => C a where ...
-</programlisting>
-There are two situations in which the rule is a bit of a pain. First,
-if one allows overlapping instance declarations then it's quite
-convenient to have a "default instance" declaration that applies if
-something more specific does not:
-
-
-<programlisting>
- instance C a where
- op = ... -- Default
-</programlisting>
-
-
-Second, sometimes you might want to use the following to get the
-effect of a "class synonym":
-
-
-<programlisting>
- class (C1 a, C2 a, C3 a) => C a where { }
-
- instance (C1 a, C2 a, C3 a) => C a where { }
-</programlisting>
-
-
-This allows you to write shorter signatures:
-
-
+<para>
+When doing this hoisting operation, GHC eliminates duplicate constraints. For
+example:
<programlisting>
- f :: C a => ...
+ type Foo a = (?x::Int) => Bool -> a
+ g :: Foo (Foo Int)
</programlisting>
-
-
-instead of
-
-
+means
<programlisting>
- f :: (C1 a, C2 a, C3 a) => ...
+ g :: (?x::Int) => Bool -> Bool -> Int
</programlisting>
-
-
-Voluminous correspondence on the Haskell mailing list has convinced me
-that it's worth experimenting with more liberal rules. If you use
-the experimental flag <option>-fallow-undecidable-instances</option>
-<indexterm><primary>-fallow-undecidable-instances
-option</primary></indexterm>, you can use arbitrary
-types in both an instance context and instance head. Termination is ensured by having a
-fixed-depth recursion stack. If you exceed the stack depth you get a
-sort of backtrace, and the opportunity to increase the stack depth
-with <option>-fcontext-stack</option><emphasis>N</emphasis>.
-</para>
-<para>
-I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
-allowing these idioms interesting idioms.
</para>
</sect3>
</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">
</sect2>
-<sect2 id="functional-dependencies">
-<title>Functional dependencies
-</title>
-
-<para> Functional dependencies are implemented as described by Mark Jones
-in “<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>”, Mark P. Jones,
-In Proceedings of the 9th European Symposium on Programming,
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
-.
-</para>
-<para>
-Functional dependencies are introduced by a vertical bar in the syntax of a
-class declaration; e.g.
-<programlisting>
- class (Monad m) => MonadState s m | m -> s where ...
-
- class Foo a b c | a b -> c where ...
-</programlisting>
-There should be more documentation, but there isn't (yet). Yell if you need it.
-</para>
-</sect2>
-
-
-
<sect2 id="sec-kinding">
<title>Explicitly-kinded quantification</title>
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>
+<para>An instance of <literal>Typeable</literal> can only be derived if the
+data type has seven or fewer type parameters, all of kind <literal>*</literal>.
+The reason for this is that the <literal>Typeable</literal> class is derived using the scheme
+described in
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/hmap/gmap2.ps">
+Scrap More Boilerplate: Reflection, Zips, and Generalised Casts
+</ulink>.
+(Section 7.4 of the paper describes the multiple <literal>Typeable</literal> classes that
+are used, and only <literal>Typeable1</literal> up to
+<literal>Typeable7</literal> are provided in the library.)
+In other cases, there is nothing to stop the programmer writing a <literal>TypableX</literal>
+class, whose kind suits that of the data type constructor, and
+then writing the data type instance by hand.
+</para>
</sect2>
<sect2 id="newtype-deriving">
<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 ================= -->
eval :: Term a -> a
eval (Lit i) = i
eval (Succ t) = 1 + eval t
- eval (IsZero i) = eval i == 0
+ 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 e2, 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></listitem>
<listitem><para>
-You cannot use a <literal>deriving</literal> clause on a GADT-style data type declaration,
-nor can you use record syntax. (It's not clear what these constructs would mean. For example,
-the record selectors might ill-typed.) However, you can use strictness annotations, in the obvious places
+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
</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
<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 }
+ data T' a where { MKT :: b -> (b->a) -> T' a }
</programlisting>
</para>
</sect1>
</para>
<para> A splice can occur in place of
<itemizedlist>
- <listitem><para> an expression; the spliced expression must have type <literal>Expr</literal></para></listitem>
+ <listitem><para> an expression; the spliced expression must
+ have type <literal>Q Exp</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>Q Typ</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>
it won't make much sense unless you've read Hughes's paper.
This notation is translated to ordinary Haskell,
using combinators from the
-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>
module.
</para>
</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.
<literal>y</literal>.
In the next line, the output is discarded.
The arrow <function>returnA</function> is defined in the
-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>
module as <literal>arr id</literal>.
The above example is treated as an abbreviation for
<screen>
Note that variables not used later in the composition are projected out.
After simplification using rewrite rules (see <xref linkend="rewrite-rules"/>)
defined in the
-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>
module, this reduces to
<screen>
arr (\ x -> (x+1, x)) >>>
<listitem>
<para>
The module must import
-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>.
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>.
</para>
</listitem>
</para>
<para>
-To have the compiler ignore uses of assert, use the compiler option
-<option>-fignore-asserts</option>. <indexterm><primary>-fignore-asserts
-option</primary></indexterm> That is, expressions of the form
+GHC ignores assertions when optimisation is turned on with the
+ <option>-O</option><indexterm><primary><option>-O</option></primary></indexterm> flag. That is, expressions of the form
<literal>assert pred e</literal> will be rewritten to
-<literal>e</literal>.
-</para>
+<literal>e</literal>. You can also disable assertions using the
+ <option>-fignore-asserts</option>
+ option<indexterm><primary><option>-fignore-asserts</option></primary>
+ </indexterm>.</para>
<para>
Assertion failures can be caught, see the documentation for the
</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" #-}
<para>When you compile any module that imports and uses any
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
</sect3>
</sect2>
+ <sect2 id="language-pragma">
+ <title>LANGUAGE pragma</title>
+
+ <indexterm><primary>LANGUAGE</primary><secondary>pragma</secondary></indexterm>
+ <indexterm><primary>pragma</primary><secondary>LANGUAGE</secondary></indexterm>
+
+ <para>This allows language extensions to be enabled in a portable way.
+ It is the intention that all Haskell compilers support the
+ <literal>LANGUAGE</literal> pragma with the same syntax, although not
+ all extensions are supported by all compilers, of
+ course. The <literal>LANGUAGE</literal> pragma should be used instead
+ of <literal>OPTIONS_GHC</literal>, if possible.</para>
+
+ <para>For example, to enable the FFI and preprocessing with CPP:</para>
+
+<programlisting>{-# LANGUAGE ForeignFunctionInterface, CPP #-}</programlisting>
+
+ <para>Any extension from the <literal>Extension</literal> type defined in
+ <ulink
+ url="../libraries/Cabal/Language-Haskell-Extension.html"><literal>Language.Haskell.Extension</literal></ulink> may be used. GHC will report an error if any of the requested extensions are not supported.</para>
+ </sect2>
+
+
<sect2 id="line-pragma">
<title>LINE pragma</title>
code. It lets you specify the line number and filename of the
original code; for example</para>
-<programlisting>
-{-# LINE 42 "Foo.vhs" #-}
-</programlisting>
+<programlisting>{-# LINE 42 "Foo.vhs" #-}</programlisting>
<para>if you'd generated the current file from something called
<filename>Foo.vhs</filename> and this line corresponds to line
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 f :: 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>A <literal>SPECIALIZE</literal> pragma can optionally be followed with a
+<literal>INLINE</literal> or <literal>NOINLINE</literal> pragma, optionally
+followed by a phase, as described in <xref linkend="inline-noinline-pragma"/>.
+The <literal>INLINE</literal> pragma affects the specialised verison of the
+function (only), and applies even if the function is recursive. The motivating
+example is this:
+<programlisting>
+-- A GADT for arrays with type-indexed representation
+data Arr e where
+ ArrInt :: !Int -> ByteArray# -> Arr Int
+ ArrPair :: !Int -> Arr e1 -> Arr e2 -> Arr (e1, e2)
+
+(!:) :: Arr e -> Int -> e
+{-# SPECIALISE INLINE (!:) :: Arr Int -> Int -> Int #-}
+{-# SPECIALISE INLINE (!:) :: Arr (a, b) -> Int -> (a, b) #-}
+(ArrInt _ ba) !: (I# i) = I# (indexIntArray# ba i)
+(ArrPair _ a1 a2) !: i = (a1 !: i, a2 !: i)
+</programlisting>
+Here, <literal>(!:)</literal> is a recursive function that indexes arrays
+of type <literal>Arr e</literal>. Consider a call to <literal>(!:)</literal>
+at type <literal>(Int,Int)</literal>. The second specialisation will fire, and
+the specialised function will be inlined. It has two calls to
+<literal>(!:)</literal>,
+both at type <literal>Int</literal>. Both these calls fire the first
+specialisation, whose body is also inlined. The result is a type-based
+unrolling of the indexing function.</para>
+<para>Warning: you can make GHC diverge by using <literal>SPECIALISE INLINE</literal>
+on an ordinarily-recursive function.</para>
+
+ <para>Note: In earlier versions of GHC, it was possible to provide your own
specialised function for a given type:
<programlisting>