</varlistentry>
<varlistentry>
+ <term><option>-foverloaded-strings</option></term>
+ <listitem>
+ <para>Enables overloaded string literals (see <xref
+ linkend="overloaded-strings"/>).</para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
<term><option>-fscoped-type-variables</option></term>
<listitem>
<para>Enables lexically-scoped type variables (see <xref
linkend="search-path"/>.</para>
<para>GHC comes with a large collection of libraries arranged
- hierarchically; see the accompanying library documentation.
- There is an ongoing project to create and maintain a stable set
- of <quote>core</quote> libraries used by several Haskell
- compilers, and the libraries that GHC comes with represent the
- current status of that project. For more details, see <ulink
- url="http://www.haskell.org/~simonmar/libraries/libraries.html">Haskell
- Libraries</ulink>.</para>
-
+ hierarchically; see the accompanying <ulink
+ url="../libraries/index.html">library
+ documentation</ulink>. More libraries to install are available
+ from <ulink
+ url="http://hackage.haskell.org/packages/hackage.html">HackageDB</ulink>.</para>
</sect2>
<!-- ====================== PATTERN GUARDS ======================= -->
</para>
<programlisting>
-clunky env var1 var1 = case lookup env var1 of
+clunky env var1 var2 = case lookup env var1 of
Nothing -> fail
Just val1 -> case lookup env var2 of
Nothing -> fail
</para>
<programlisting>
-clunky env var1 var1
+clunky env var1 var2
| Just val1 <- lookup env var1
, Just val2 <- lookup env var2
= val1 + val2
<!-- TYPE SYSTEM EXTENSIONS -->
-<sect1 id="type-extensions">
-<title>Type system extensions</title>
-
-
-<sect2>
-<title>Data types and type synonyms</title>
+<sect1 id="data-type-extensions">
+<title>Extensions to data types and type synonyms</title>
-<sect3 id="nullary-types">
+<sect2 id="nullary-types">
<title>Data types with no constructors</title>
<para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
<para>Syntactically, the declaration lacks the "= constrs" part. The
type can be parameterised over types of any kind, but if the kind is
not <literal>*</literal> then an explicit kind annotation must be used
-(see <xref linkend="sec-kinding"/>).</para>
+(see <xref linkend="kinding"/>).</para>
<para>Such data types have only one value, namely bottom.
Nevertheless, they can be useful when defining "phantom types".</para>
-</sect3>
+</sect2>
-<sect3 id="infix-tycons">
+<sect2 id="infix-tycons">
<title>Infix type constructors, classes, and type variables</title>
<para>
</itemizedlist>
</para>
-</sect3>
+</sect2>
-<sect3 id="type-synonyms">
+<sect2 id="type-synonyms">
<title>Liberalised type synonyms</title>
<para>
</programlisting>
because GHC does not allow unboxed tuples on the left of a function arrow.
</para>
-</sect3>
+</sect2>
-<sect3 id="existential-quantification">
+<sect2 id="existential-quantification">
<title>Existentially quantified data constructors
</title>
quite a bit of object-oriented-like programming this way.
</para>
-<sect4 id="existential">
+<sect3 id="existential">
<title>Why existential?
</title>
adding a new existential quantification construct.
</para>
-</sect4>
+</sect3>
-<sect4>
+<sect3>
<title>Type classes</title>
<para>
universal quantification earlier.
</para>
-</sect4>
+</sect3>
-<sect4>
+<sect3 id="existential-records">
<title>Record Constructors</title>
<para>
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
+<literal>_inc</literal> or <literal>_display</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
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:
</para>
-</sect4>
+</sect3>
-<sect4>
+<sect3>
<title>Restrictions</title>
<para>
You can't use <literal>deriving</literal> to define instances of a
data type with existentially quantified data constructors.
-Reason: in most cases it would not make sense. For example:#
+Reason: in most cases it would not make sense. For example:;
<programlisting>
data T = forall a. MkT [a] deriving( Eq )
</para>
-</sect4>
</sect3>
-
</sect2>
+<!-- ====================== Generalised algebraic data types ======================= -->
+<sect2 id="gadt-style">
+<title>Declaring data types with explicit constructor signatures</title>
-<sect2 id="multi-param-type-classes">
-<title>Class declarations</title>
-
-<para>
-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>
-All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
-</para>
-
-<sect3>
-<title>Multi-parameter type classes</title>
-<para>
-Multi-parameter type classes are permitted. For example:
-
-
+<para>GHC allows you to declare an algebraic data type by
+giving the type signatures of constructors explicitly. For example:
<programlisting>
- class Collection c a where
- union :: c a -> c a -> c a
- ...etc.
+ data Maybe a where
+ Nothing :: Maybe a
+ Just :: a -> Maybe a
</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:
-
-
+The form is called a "GADT-style declaration"
+because Generalised Algebraic Data Types, described in <xref linkend="gadt"/>,
+can only be declared using this form.</para>
+<para>Notice that GADT-style syntax generalises existential types (<xref linkend="existential-quantification"/>).
+For example, these two declarations are equivalent:
<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
+ data Foo = forall a. MkFoo a (a -> Bool)
+ data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
</programlisting>
-
-
</para>
-<para>
-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:
-
-
+<para>Any data type that can be declared in standard Haskell-98 syntax
+can also be declared using GADT-style syntax.
+The choice is largely stylistic, but GADT-style declarations differ in one important respect:
+they treat class constraints on the data constructors differently.
+Specifically, if the constructor is given a type-class context, that
+context is made available by pattern matching. For example:
<programlisting>
- class C a where {
- op :: D b => a -> b -> b
- }
-
- class C a => D a where { ... }
-</programlisting>
+ data Set a where
+ MkSet :: Eq a => [a] -> Set a
+ makeSet :: Eq a => [a] -> Set a
+ makeSet xs = MkSet (nub xs)
-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>.)
+ insert :: a -> Set a -> Set a
+ insert a (MkSet as) | a `elem` as = MkSet as
+ | otherwise = MkSet (a:as)
+</programlisting>
+A use of <literal>MkSet</literal> as a constructor (e.g. in the definition of <literal>makeSet</literal>)
+gives rise to a <literal>(Eq a)</literal>
+constraint, as you would expect. The new feature is that pattern-matching on <literal>MkSet</literal>
+(as in the definition of <literal>insert</literal>) makes <emphasis>available</emphasis> an <literal>(Eq a)</literal>
+context. In implementation terms, the <literal>MkSet</literal> constructor has a hidden field that stores
+the <literal>(Eq a)</literal> dictionary that is passed to <literal>MkSet</literal>; so
+when pattern-matching that dictionary becomes available for the right-hand side of the match.
+In the example, the equality dictionary is used to satisfy the equality constraint
+generated by the call to <literal>elem</literal>, so that the type of
+<literal>insert</literal> itself has no <literal>Eq</literal> constraint.
</para>
-</sect3>
-
-
-
-
-<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:
+<para>This behaviour contrasts with Haskell 98's peculiar treament of
+contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report).
+In Haskell 98 the defintion
<programlisting>
- class Seq s a where
- fromList :: [a] -> s a
- elem :: Eq a => a -> s a -> Bool
+ data Eq a => Set' a = MkSet' [a]
</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>
-
-
-</sect3>
-</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>
+gives <literal>MkSet'</literal> the same type as <literal>MkSet</literal> above. But instead of
+<emphasis>making available</emphasis> an <literal>(Eq a)</literal> constraint, pattern-matching
+on <literal>MkSet'</literal> <emphasis>requires</emphasis> an <literal>(Eq a)</literal> constraint!
+GHC faithfully implements this behaviour, odd though it is. But for GADT-style declarations,
+GHC's behaviour is much more useful, as well as much more intuitive.</para>
<para>
-Functional dependencies are introduced by a vertical bar in the syntax of a
-class declaration; e.g.
+For example, a possible application of GHC's behaviour is to reify dictionaries:
<programlisting>
- class (Monad m) => MonadState s m | m -> s where ...
+ data NumInst a where
+ MkNumInst :: Num a => NumInst a
- class Foo a b c | a b -> c where ...
+ intInst :: NumInst Int
+ intInst = MkNumInst
+
+ plus :: NumInst a -> a -> a -> a
+ plus MkNumInst p q = p + q
</programlisting>
-There should be more documentation, but there isn't (yet). Yell if you need it.
+Here, a value of type <literal>NumInst a</literal> is equivalent
+to an explicit <literal>(Num a)</literal> dictionary.
</para>
-<sect3><title>Rules for functional dependencies </title>
<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:
+The rest of this section gives further details about GADT-style data
+type declarations.
+
+<itemizedlist>
+<listitem><para>
+The result type of each data constructor must begin with the type constructor being defined.
+If the result type of all constructors
+has the form <literal>T a1 ... an</literal>, where <literal>a1 ... an</literal>
+are distinct type variables, then the data type is <emphasis>ordinary</emphasis>;
+otherwise is a <emphasis>generalised</emphasis> data type (<xref linkend="gadt"/>).
+</para></listitem>
+<listitem><para>
+The type signature of
+each constructor is independent, and is implicitly universally quantified as usual.
+Different constructors may have different universally-quantified type variables
+and different type-class constraints.
+For example, this is fine:
<programlisting>
- class Coll s a where
- empty :: s
- insert :: s -> a -> s
+ data T a where
+ T1 :: Eq b => b -> T b
+ T2 :: (Show c, Ix c) => c -> [c] -> T c
</programlisting>
+</para></listitem>
-is not OK, because the type of <literal>empty</literal> doesn't mention
-<literal>a</literal>. Functional dependencies can make the type variable
-reachable:
+<listitem><para>
+Unlike a Haskell-98-style
+data type declaration, the type variable(s) in the "<literal>data Set a where</literal>" header
+have no scope. Indeed, one can write a kind signature instead:
<programlisting>
- class Coll s a | s -> a where
- empty :: s
- insert :: s -> a -> s
+ data Set :: * -> * where ...
</programlisting>
-
-Alternatively <literal>Coll</literal> might be rewritten
-
+or even a mixture of the two:
<programlisting>
- class Coll s a where
- empty :: s a
- insert :: s a -> a -> s a
+ data Foo a :: (* -> *) -> * where ...
</programlisting>
-
-
-which makes the connection between the type of a collection of
-<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
-Occasionally this really doesn't work, in which case you can split the
-class like this:
-
-
+The type variables (if given) may be explicitly kinded, so we could also write the header for <literal>Foo</literal>
+like this:
<programlisting>
- class CollE s where
- empty :: s
-
- class CollE s => Coll s a where
- insert :: s -> a -> s
+ data Foo a (b :: * -> *) where ...
</programlisting>
-</para>
-</sect3>
-
+</para></listitem>
-<sect3>
-<title>Background on functional dependencies</title>
-<para>The following description of the motivation and use of functional dependencies is taken
-from the Hugs user manual, reproduced here (with minor changes) by kind
-permission of Mark Jones.
-</para>
-<para>
-Consider the following class, intended as part of a
-library for collection types:
+<listitem><para>
+You can use strictness annotations, in the obvious places
+in the constructor type:
<programlisting>
- class Collects e ce where
- empty :: ce
- insert :: e -> ce -> ce
- member :: e -> ce -> Bool
+ 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>
-The type variable e used here represents the element type, while ce is the type
-of the container itself. Within this framework, we might want to define
-instances of this class for lists or characteristic functions (both of which
-can be used to represent collections of any equality type), bit sets (which can
-be used to represent collections of characters), or hash tables (which can be
-used to represent any collection whose elements have a hash function). Omitting
-standard implementation details, this would lead to the following declarations:
+</para></listitem>
+
+<listitem><para>
+You can use a <literal>deriving</literal> clause on a GADT-style data type
+declaration. For example, these two declarations are equivalent
<programlisting>
- instance Eq e => Collects e [e] where ...
- instance Eq e => Collects e (e -> Bool) where ...
- instance Collects Char BitSet where ...
- instance (Hashable e, Collects a ce)
- => Collects e (Array Int ce) where ...
+ data Maybe1 a where {
+ Nothing1 :: Maybe1 a ;
+ Just1 :: a -> Maybe1 a
+ } deriving( Eq, Ord )
+
+ data Maybe2 a = Nothing2 | Just2 a
+ deriving( Eq, Ord )
</programlisting>
-All this looks quite promising; we have a class and a range of interesting
-implementations. Unfortunately, there are some serious problems with the class
-declaration. First, the empty function has an ambiguous type:
+</para></listitem>
+
+<listitem><para>
+You can use record syntax on a GADT-style data type declaration:
+
<programlisting>
- empty :: Collects e ce => ce
+ data Person where
+ Adult { name :: String, children :: [Person] } :: Person
+ Child { name :: String } :: Person
</programlisting>
-By "ambiguous" we mean that there is a type variable e that appears on the left
-of the <literal>=></literal> symbol, but not on the right. The problem with
-this is that, according to the theoretical foundations of Haskell overloading,
-we cannot guarantee a well-defined semantics for any term with an ambiguous
-type.
+As usual, for every constructor that has a field <literal>f</literal>, the type of
+field <literal>f</literal> must be the same (modulo alpha conversion).
</para>
<para>
-We can sidestep this specific problem by removing the empty member from the
-class declaration. However, although the remaining members, insert and member,
-do not have ambiguous types, we still run into problems when we try to use
-them. For example, consider the following two functions:
+At the moment, record updates are not yet possible with GADT-style declarations,
+so support is limited to record construction, selection and pattern matching.
+For exmaple
<programlisting>
- f x y = insert x . insert y
- g = f True 'a'
+ aPerson = Adult { name = "Fred", children = [] }
+
+ shortName :: Person -> Bool
+ hasChildren (Adult { children = kids }) = not (null kids)
+ hasChildren (Child {}) = False
</programlisting>
-for which GHC infers the following types:
+</para></listitem>
+
+<listitem><para>
+As in the case of existentials declared using the Haskell-98-like record syntax
+(<xref linkend="existential-records"/>),
+record-selector functions are generated only for those fields that have well-typed
+selectors.
+Here is the example of that section, in GADT-style syntax:
<programlisting>
- f :: (Collects a c, Collects b c) => a -> b -> c -> c
- g :: (Collects Bool c, Collects Char c) => c -> c
+data Counter a where
+ NewCounter { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+ :: Counter a
+</programlisting>
+As before, only one selector function is generated here, that for <literal>tag</literal>.
+Nevertheless, you can still use all the field names in pattern matching and record construction.
+</para></listitem>
+</itemizedlist></para>
+</sect2>
+
+<sect2 id="gadt">
+<title>Generalised Algebraic Data Types (GADTs)</title>
+
+<para>Generalised Algebraic Data Types generalise ordinary algebraic data types
+by allowing constructors to have richer return types. Here is an 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 data types. This generality allows us to
+write a well-typed <literal>eval</literal> function
+for these <literal>Terms</literal>:
+<programlisting>
+ eval :: Term a -> a
+ eval (Lit i) = i
+ eval (Succ t) = 1 + eval t
+ eval (IsZero t) = eval t == 0
+ eval (If b e1 e2) = if eval b then eval e1 else eval e2
+ eval (Pair e1 e2) = (eval e1, eval e2)
+</programlisting>
+The key point about GADTs is that <emphasis>pattern matching causes type refinement</emphasis>.
+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 the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
+unification-based type inference for GADTs</ulink>,
+(ICFP 2006).
+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>
+<para>
+These and many other examples are given in papers by Hongwei Xi, and
+Tim Sheard. There is a longer introduction
+<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
+and Ralf Hinze's
+<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
+may use different notation to that implemented in GHC.
+</para>
+<para>
+The rest of this section outlines the extensions to GHC that support GADTs.
+<itemizedlist>
+<listitem><para>
+A GADT can only be declared using GADT-style syntax (<xref linkend="gadt-style"/>);
+the old Haskell-98 syntax for data declarations always declares an ordinary data type.
+The result type of each constructor must begin with the type constructor being defined,
+but for a GADT the arguments to the type constructor can be arbitrary monotypes.
+For example, in the <literal>Term</literal> data
+type above, the type of each constructor must end with <literal>Term ty</literal>, but
+the <literal>ty</literal> may not be a type variable (e.g. the <literal>Lit</literal>
+constructor).
+</para></listitem>
+
+<listitem><para>
+You cannot use a <literal>deriving</literal> clause for a GADT; only for
+an ordianary data type.
+</para></listitem>
+
+<listitem><para>
+As mentioned in <xref linkend="gadt-style"/>, record syntax is supported.
+For example:
+<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>
+However, for GADTs there is the following additional constraint:
+every constructor that has a field <literal>f</literal> must have
+the same result type (modulo alpha conversion)
+Hence, in the above 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>
+</para></listitem>
+
+</itemizedlist>
+</para>
+
+</sect2>
+
+<!-- ====================== End of Generalised algebraic data types ======================= -->
+
+
+<sect2 id="deriving-typeable">
+<title>Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal></title>
+
+<para>
+Haskell 98 allows the programmer to add "<literal>deriving( Eq, Ord )</literal>" to a data type
+declaration, to generate a standard instance declaration for classes specified in the <literal>deriving</literal> clause.
+In Haskell 98, the only classes that may appear in the <literal>deriving</literal> clause are the standard
+classes <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal>, <literal>Ix</literal>, <literal>Bounded</literal>, <literal>Read</literal>, and <literal>Show</literal>.
+</para>
+<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.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">
+<title>Generalised derived instances for newtypes</title>
+
+<para>
+When you define an abstract type using <literal>newtype</literal>, you may want
+the new type to inherit some instances from its representation. In
+Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
+other classes you have to write an explicit instance declaration. For
+example, if you define
+
+<programlisting>
+ newtype Dollars = Dollars Int
+</programlisting>
+
+and you want to use arithmetic on <literal>Dollars</literal>, you have to
+explicitly define an instance of <literal>Num</literal>:
+
+<programlisting>
+ instance Num Dollars where
+ Dollars a + Dollars b = Dollars (a+b)
+ ...
+</programlisting>
+All the instance does is apply and remove the <literal>newtype</literal>
+constructor. It is particularly galling that, since the constructor
+doesn't appear at run-time, this instance declaration defines a
+dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
+dictionary, only slower!
+</para>
+
+
+<sect3> <title> Generalising the deriving clause </title>
+<para>
+GHC now permits such instances to be derived instead, so one can write
+<programlisting>
+ newtype Dollars = Dollars Int deriving (Eq,Show,Num)
+</programlisting>
+
+and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
+for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
+derives an instance declaration of the form
+
+<programlisting>
+ instance Num Int => Num Dollars
+</programlisting>
+
+which just adds or removes the <literal>newtype</literal> constructor according to the type.
+</para>
+<para>
+
+We can also derive instances of constructor classes in a similar
+way. For example, suppose we have implemented state and failure monad
+transformers, such that
+
+<programlisting>
+ instance Monad m => Monad (State s m)
+ instance Monad m => Monad (Failure m)
+</programlisting>
+In Haskell 98, we can define a parsing monad by
+<programlisting>
+ type Parser tok m a = State [tok] (Failure m) a
+</programlisting>
+
+which is automatically a monad thanks to the instance declarations
+above. With the extension, we can make the parser type abstract,
+without needing to write an instance of class <literal>Monad</literal>, via
+
+<programlisting>
+ newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+ deriving Monad
+</programlisting>
+In this case the derived instance declaration is of the form
+<programlisting>
+ instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
+</programlisting>
+
+Notice that, since <literal>Monad</literal> is a constructor class, the
+instance is a <emphasis>partial application</emphasis> of the new type, not the
+entire left hand side. We can imagine that the type declaration is
+``eta-converted'' to generate the context of the instance
+declaration.
+</para>
+<para>
+
+We can even derive instances of multi-parameter classes, provided the
+newtype is the last class parameter. In this case, a ``partial
+application'' of the class appears in the <literal>deriving</literal>
+clause. For example, given the class
+
+<programlisting>
+ class StateMonad s m | m -> s where ...
+ instance Monad m => StateMonad s (State s m) where ...
+</programlisting>
+then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by
+<programlisting>
+ newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+ deriving (Monad, StateMonad [tok])
+</programlisting>
+
+The derived instance is obtained by completing the application of the
+class to the new type:
+
+<programlisting>
+ instance StateMonad [tok] (State [tok] (Failure m)) =>
+ StateMonad [tok] (Parser tok m)
+</programlisting>
+</para>
+<para>
+
+As a result of this extension, all derived instances in newtype
+ 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.
+</para>
+</sect3>
+
+<sect3> <title> A more precise specification </title>
+<para>
+Derived instance declarations are constructed as follows. Consider the
+declaration (after expansion of any type synonyms)
+
+<programlisting>
+ newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm)
+</programlisting>
+
+where
+ <itemizedlist>
+<listitem><para>
+ The <literal>ci</literal> are partial applications of
+ classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
+ is exactly <literal>j+1</literal>. That is, <literal>C</literal> lacks exactly one type argument.
+</para></listitem>
+<listitem><para>
+ The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.
+</para></listitem>
+<listitem><para>
+ The type <literal>t</literal> is an arbitrary type.
+</para></listitem>
+<listitem><para>
+ The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>,
+ nor in the <literal>ci</literal>, and
+</para></listitem>
+<listitem><para>
+ None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>,
+ <literal>Typeable</literal>, or <literal>Data</literal>. These classes
+ should not "look through" the type or its constructor. You can still
+ derive these classes for a newtype, but it happens in the usual way, not
+ via this new mechanism.
+</para></listitem>
+</itemizedlist>
+Then, for each <literal>ci</literal>, the derived instance
+declaration is:
+<programlisting>
+ instance ci t => ci (T v1...vk)
+</programlisting>
+As an example which does <emphasis>not</emphasis> work, consider
+<programlisting>
+ newtype NonMonad m s = NonMonad (State s m s) deriving Monad
+</programlisting>
+Here we cannot derive the instance
+<programlisting>
+ instance Monad (State s m) => Monad (NonMonad m)
+</programlisting>
+
+because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
+and so cannot be "eta-converted" away. It is a good thing that this
+<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
+not, in fact, a monad --- for the same reason. Try defining
+<literal>>>=</literal> with the correct type: you won't be able to.
+</para>
+<para>
+
+Notice also that the <emphasis>order</emphasis> of class parameters becomes
+important, since we can only derive instances for the last one. If the
+<literal>StateMonad</literal> class above were instead defined as
+
+<programlisting>
+ class StateMonad m s | m -> s where ...
+</programlisting>
+
+then we would not have been able to derive an instance for the
+<literal>Parser</literal> type above. We hypothesise that multi-parameter
+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="stand-alone-deriving">
+<title>Stand-alone deriving declarations</title>
+
+<para>
+GHC now allows stand-alone <literal>deriving</literal> declarations, enabled by <literal>-fglasgow-exts</literal>:
+<programlisting>
+ data Foo a = Bar a | Baz String
+
+ derive instance Eq (Foo a)
+</programlisting>
+The token "<literal>derive</literal>" is a keyword only when followed by "<literal>instance</literal>";
+you can use it as a variable name elsewhere.</para>
+<para>The stand-alone syntax is generalised for newtypes in exactly the same
+way that ordinary <literal>deriving</literal> clauses are generalised (<xref linkend="newtype-deriving"/>).
+For example:
+<programlisting>
+ newtype Foo a = MkFoo (State Int a)
+
+ derive instance MonadState Int Foo
+</programlisting>
+GHC always treats the <emphasis>last</emphasis> parameter of the instance
+(<literal>Foo</literal> in this exmample) as the type whose instance is being derived.
+</para>
+
+</sect2>
+
+</sect1>
+
+
+<!-- TYPE SYSTEM EXTENSIONS -->
+<sect1 id="other-type-extensions">
+<title>Other type system extensions</title>
+
+<sect2 id="multi-param-type-classes">
+<title>Class declarations</title>
+
+<para>
+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>
+All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
+</para>
+
+<sect3>
+<title>Multi-parameter type classes</title>
+<para>
+Multi-parameter type classes are permitted. For example:
+
+
+<programlisting>
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...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:
+
+
+<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>
+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:
+
+
+<programlisting>
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
+</programlisting>
+
+
+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>
+</sect3>
+
+
+
+
+<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>
+
+
+</sect3>
+</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>
+
+<sect3><title>Rules for functional dependencies </title>
+<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
+ empty :: s
+ insert :: s -> a -> s
+</programlisting>
+
+is not OK, because the type of <literal>empty</literal> doesn't mention
+<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
+ empty :: s a
+ insert :: s a -> a -> s a
+</programlisting>
+
+
+which makes the connection between the type of a collection of
+<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
+
+
+<programlisting>
+ class CollE s where
+ empty :: s
+
+ class CollE s => Coll s a where
+ insert :: s -> a -> s
+</programlisting>
+</para>
+</sect3>
+
+
+<sect3>
+<title>Background on functional dependencies</title>
+
+<para>The following description of the motivation and use of functional dependencies is taken
+from the Hugs user manual, reproduced here (with minor changes) by kind
+permission of Mark Jones.
+</para>
+<para>
+Consider the following class, intended as part of a
+library for collection types:
+<programlisting>
+ class Collects e ce where
+ empty :: ce
+ insert :: e -> ce -> ce
+ member :: e -> ce -> Bool
+</programlisting>
+The type variable e used here represents the element type, while ce is the type
+of the container itself. Within this framework, we might want to define
+instances of this class for lists or characteristic functions (both of which
+can be used to represent collections of any equality type), bit sets (which can
+be used to represent collections of characters), or hash tables (which can be
+used to represent any collection whose elements have a hash function). Omitting
+standard implementation details, this would lead to the following declarations:
+<programlisting>
+ instance Eq e => Collects e [e] where ...
+ instance Eq e => Collects e (e -> Bool) where ...
+ instance Collects Char BitSet where ...
+ instance (Hashable e, Collects a ce)
+ => Collects e (Array Int ce) where ...
+</programlisting>
+All this looks quite promising; we have a class and a range of interesting
+implementations. Unfortunately, there are some serious problems with the class
+declaration. First, the empty function has an ambiguous type:
+<programlisting>
+ empty :: Collects e ce => ce
+</programlisting>
+By "ambiguous" we mean that there is a type variable e that appears on the left
+of the <literal>=></literal> symbol, but not on the right. The problem with
+this is that, according to the theoretical foundations of Haskell overloading,
+we cannot guarantee a well-defined semantics for any term with an ambiguous
+type.
+</para>
+<para>
+We can sidestep this specific problem by removing the empty member from the
+class declaration. However, although the remaining members, insert and member,
+do not have ambiguous types, we still run into problems when we try to use
+them. For example, consider the following two functions:
+<programlisting>
+ f x y = insert x . insert y
+ g = f True 'a'
+</programlisting>
+for which GHC infers the following types:
+<programlisting>
+ f :: (Collects a c, Collects b c) => a -> b -> c -> c
+ g :: (Collects Bool c, Collects Char c) => c -> c
</programlisting>
Notice that the type for f allows the two parameters x and y to be assigned
different types, even though it attempts to insert each of the two values, one
following rules:
<orderedlist>
<listitem><para>
-For each assertion in the context:
+The Paterson Conditions: for each assertion in the context
<orderedlist>
<listitem><para>No type variable has more occurrences in the assertion than in the head</para></listitem>
<listitem><para>The assertion has fewer constructors and variables (taken together
</orderedlist>
</para></listitem>
-<listitem><para>The coverage condition. For each functional dependency,
+<listitem><para>The Coverage Condition. For each functional dependency,
<replaceable>tvs</replaceable><subscript>left</subscript> <literal>-></literal>
<replaceable>tvs</replaceable><subscript>right</subscript>, of the class,
every type variable in
</orderedlist>
These restrictions ensure that context reduction terminates: each reduction
step makes the problem smaller by at least one
-constructor. For example, the following would make the type checker
-loop if it wasn't excluded:
-<programlisting>
- instance C a => C a where ...
-</programlisting>
+constructor. Both the Paterson Conditions and the Coverage Condition are lifted
+if you give the <option>-fallow-undecidable-instances</option>
+flag (<xref linkend="undecidable-instances"/>).
+You can find lots of background material about the reason for these
+restrictions in the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
+Understanding functional dependencies via Constraint Handling Rules</ulink>.
+</para>
+<para>
For example, these are OK:
<programlisting>
instance C Int [a] -- Multiple parameters
op = ... -- Default
</programlisting>
</para>
-<para>You can find lots of background material about the reason for these
-restrictions in the paper <ulink
-url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
-Understanding functional dependencies via Constraint Handling Rules</ulink>.
-</para>
</sect3>
<sect3 id="undecidable-instances">
Nevertheless, GHC allows you to experiment 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
+option</primary></indexterm>, both the Paterson Conditions and the Coverage Condition
+(described in <xref linkend="instance-rules"/>) are lifted. 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>
</listitem>
-</orderedlist>
-
-</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>
- type Discard a = forall b. a -> b -> a
-
- g :: Int -> Discard Int
- g x y z = x+y
-</programlisting>
-Simply expanding the type synonym would give
-<programlisting>
- g :: Int -> (forall b. Int -> b -> Int)
-</programlisting>
-but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
-<programlisting>
- g :: forall b. Int -> Int -> b -> Int
-</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>
-<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>
-</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:
-<programlisting>
- g :: Int -> Int -> forall b. b -> Int
-</programlisting>
-</para>
-<para>
-When doing this hoisting operation, GHC eliminates duplicate constraints. For
-example:
-<programlisting>
- type Foo a = (?x::Int) => Bool -> a
- g :: Foo (Foo Int)
-</programlisting>
-means
-<programlisting>
- g :: (?x::Int) => Bool -> Bool -> Int
-</programlisting>
+</orderedlist>
+
</para>
</sect3>
+
</sect2>
<sect2 id="implicit-parameters">
x' = newName ns2
env = extend env x x'
</programlisting>
-Notice the call to 'split' introduced by the type checker.
-How did it know to use 'splitNS'? Because what it really did
-was to introduce a call to the overloaded function 'split',
-defined by the class <literal>Splittable</literal>:
-<programlisting>
- class Splittable a where
- split :: a -> (a,a)
-</programlisting>
-The instance for <literal>Splittable NameSupply</literal> tells GHC how to implement
-split for name supplies. But we can simply write
-<programlisting>
- g x = (x, %ns, %ns)
-</programlisting>
-and GHC will infer
-<programlisting>
- g :: (Splittable a, %ns :: a) => b -> (b,a,a)
-</programlisting>
-The <literal>Splittable</literal> class is built into GHC. It's exported by module
-<literal>GHC.Exts</literal>.
-</para>
-<para>
-Other points:
-<itemizedlist>
-<listitem> <para> '<literal>?x</literal>' and '<literal>%x</literal>'
-are entirely distinct implicit parameters: you
- can use them together and they won't intefere with each other. </para>
-</listitem>
-
-<listitem> <para> You can bind linear implicit parameters in 'with' clauses. </para> </listitem>
-
-<listitem> <para>You cannot have implicit parameters (whether linear or not)
- in the context of a class or instance declaration. </para></listitem>
-</itemizedlist>
-</para>
-
-<sect3><title>Warnings</title>
-
-<para>
-The monomorphism restriction is even more important than usual.
-Consider the example above:
-<programlisting>
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam x' (f env e)
- where
- x' = newName %ns
- env' = extend env x x'
-</programlisting>
-If we replaced the two occurrences of x' by (newName %ns), which is
-usually a harmless thing to do, we get:
-<programlisting>
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam (newName %ns) (f env e)
- where
- env' = extend env x (newName %ns)
-</programlisting>
-But now the name supply is consumed in <emphasis>three</emphasis> places
-(the two calls to newName,and the recursive call to f), so
-the result is utterly different. Urk! We don't even have
-the beta rule.
-</para>
-<para>
-Well, this is an experimental change. With implicit
-parameters we have already lost beta reduction anyway, and
-(as John Launchbury puts it) we can't sensibly reason about
-Haskell programs without knowing their typing.
-</para>
-
-</sect3>
-
-<sect3><title>Recursive functions</title>
-<para>Linear implicit parameters can be particularly tricky when you have a recursive function
-Consider
-<programlisting>
- foo :: %x::T => Int -> [Int]
- foo 0 = []
- foo n = %x : foo (n-1)
-</programlisting>
-where T is some type in class Splittable.</para>
-<para>
-Do you get a list of all the same T's or all different T's
-(assuming that split gives two distinct T's back)?
-</para><para>
-If you supply the type signature, taking advantage of polymorphic
-recursion, you get what you'd probably expect. Here's the
-translated term, where the implicit param is made explicit:
-<programlisting>
- foo x 0 = []
- foo x n = let (x1,x2) = split x
- in x1 : foo x2 (n-1)
-</programlisting>
-But if you don't supply a type signature, GHC uses the Hindley
-Milner trick of using a single monomorphic instance of the function
-for the recursive calls. That is what makes Hindley Milner type inference
-work. So the translation becomes
-<programlisting>
- foo x = let
- foom 0 = []
- foom n = x : foom (n-1)
- in
- foom
-</programlisting>
-Result: 'x' is not split, and you get a list of identical T's. So the
-semantics of the program depends on whether or not foo has a type signature.
-Yikes!
-</para><para>
-You may say that this is a good reason to dislike linear implicit parameters
-and you'd be right. That is why they are an experimental feature.
-</para>
-</sect3>
-
-</sect2>
-
-================ END OF Linear Implicit Parameters commented out -->
-
-<sect2 id="sec-kinding">
-<title>Explicitly-kinded quantification</title>
-
-<para>
-Haskell infers the kind of each type variable. Sometimes it is nice to be able
-to give the kind explicitly as (machine-checked) documentation,
-just as it is nice to give a type signature for a function. On some occasions,
-it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
-John Hughes had to define the data type:
-<screen>
- data Set cxt a = Set [a]
- | Unused (cxt a -> ())
-</screen>
-The only use for the <literal>Unused</literal> constructor was to force the correct
-kind for the type variable <literal>cxt</literal>.
-</para>
-<para>
-GHC now instead allows you to specify the kind of a type variable directly, wherever
-a type variable is explicitly bound. Namely:
-<itemizedlist>
-<listitem><para><literal>data</literal> declarations:
-<screen>
- data Set (cxt :: * -> *) a = Set [a]
-</screen></para></listitem>
-<listitem><para><literal>type</literal> declarations:
-<screen>
- type T (f :: * -> *) = f Int
-</screen></para></listitem>
-<listitem><para><literal>class</literal> declarations:
-<screen>
- class (Eq a) => C (f :: * -> *) a where ...
-</screen></para></listitem>
-<listitem><para><literal>forall</literal>'s in type signatures:
-<screen>
- f :: forall (cxt :: * -> *). Set cxt Int
-</screen></para></listitem>
-</itemizedlist>
-</para>
-
-<para>
-The parentheses are required. Some of the spaces are required too, to
-separate the lexemes. If you write <literal>(f::*->*)</literal> you
-will get a parse error, because "<literal>::*->*</literal>" is a
-single lexeme in Haskell.
-</para>
-
-<para>
-As part of the same extension, you can put kind annotations in types
-as well. Thus:
-<screen>
- f :: (Int :: *) -> Int
- g :: forall a. a -> (a :: *)
-</screen>
-The syntax is
-<screen>
- atype ::= '(' ctype '::' kind ')
-</screen>
-The parentheses are required.
-</para>
-</sect2>
-
-
-<sect2 id="universal-quantification">
-<title>Arbitrary-rank polymorphism
-</title>
-
-<para>
-Haskell type signatures are implicitly quantified. The new keyword <literal>forall</literal>
-allows us to say exactly what this means. For example:
-</para>
-<para>
-<programlisting>
- g :: b -> b
-</programlisting>
-means this:
-<programlisting>
- g :: forall b. (b -> b)
-</programlisting>
-The two are treated identically.
-</para>
-
-<para>
-However, GHC's type system supports <emphasis>arbitrary-rank</emphasis>
-explicit universal quantification in
-types.
-For example, all the following types are legal:
-<programlisting>
- f1 :: forall a b. a -> b -> a
- g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
-
- f2 :: (forall a. a->a) -> Int -> Int
- g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
-
- f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
-</programlisting>
-Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
-can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
-The <literal>forall</literal> makes explicit the universal quantification that
-is implicitly added by Haskell.
-</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 arrow. As <literal>g2</literal>
-shows, the polymorphic type on the left of the function arrow can be overloaded.
-</para>
-<para>
-The function <literal>f3</literal> has a rank-3 type;
-it has rank-2 types on the left of a function arrow.
-</para>
-<para>
-GHC allows types of arbitrary rank; you can nest <literal>forall</literal>s
-arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
-that restriction has now been lifted.)
-In particular, a forall-type (also called a "type scheme"),
-including an operational type class context, is legal:
-<itemizedlist>
-<listitem> <para> On the left of a function arrow </para> </listitem>
-<listitem> <para> On the right of a function arrow (see <xref linkend="hoist"/>) </para> </listitem>
-<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
-example, any of the <literal>f1,f2,f3,g1,g2</literal> above would be valid
-field type signatures.</para> </listitem>
-<listitem> <para> As the type of an implicit parameter </para> </listitem>
-<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables"/>) </para> </listitem>
-</itemizedlist>
-There is one place you cannot put a <literal>forall</literal>:
-you cannot instantiate a type variable with a forall-type. So you cannot
-make a forall-type the argument of a type constructor. So these types are illegal:
-<programlisting>
- x1 :: [forall a. a->a]
- x2 :: (forall a. a->a, Int)
- x3 :: Maybe (forall a. a->a)
-</programlisting>
-Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
-a type variable any more!
-</para>
-
-
-<sect3 id="univ">
-<title>Examples
-</title>
-
-<para>
-In a <literal>data</literal> or <literal>newtype</literal> declaration one can quantify
-the types of the constructor arguments. Here are several examples:
-</para>
-
-<para>
-
+Notice the call to 'split' introduced by the type checker.
+How did it know to use 'splitNS'? Because what it really did
+was to introduce a call to the overloaded function 'split',
+defined by the class <literal>Splittable</literal>:
<programlisting>
-data T a = T1 (forall b. b -> b -> b) a
-
-data MonadT m = MkMonad { return :: forall a. a -> m a,
- bind :: forall a b. m a -> (a -> m b) -> m b
- }
-
-newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
+ class Splittable a where
+ split :: a -> (a,a)
</programlisting>
-
-</para>
-
-<para>
-The constructors have rank-2 types:
+The instance for <literal>Splittable NameSupply</literal> tells GHC how to implement
+split for name supplies. But we can simply write
+<programlisting>
+ g x = (x, %ns, %ns)
+</programlisting>
+and GHC will infer
+<programlisting>
+ g :: (Splittable a, %ns :: a) => b -> (b,a,a)
+</programlisting>
+The <literal>Splittable</literal> class is built into GHC. It's exported by module
+<literal>GHC.Exts</literal>.
</para>
-
<para>
+Other points:
+<itemizedlist>
+<listitem> <para> '<literal>?x</literal>' and '<literal>%x</literal>'
+are entirely distinct implicit parameters: you
+ can use them together and they won't intefere with each other. </para>
+</listitem>
-<programlisting>
-T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
-MkMonad :: forall m. (forall a. a -> m a)
- -> (forall a b. m a -> (a -> m b) -> m b)
- -> MonadT m
-MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
-</programlisting>
+<listitem> <para> You can bind linear implicit parameters in 'with' clauses. </para> </listitem>
+<listitem> <para>You cannot have implicit parameters (whether linear or not)
+ in the context of a class or instance declaration. </para></listitem>
+</itemizedlist>
</para>
-<para>
-Notice that you don't need to use a <literal>forall</literal> if there's an
-explicit context. For example in the first argument of the
-constructor <function>MkSwizzle</function>, an implicit "<literal>forall a.</literal>" is
-prefixed to the argument type. The implicit <literal>forall</literal>
-quantifies all type variables that are not already in scope, and are
-mentioned in the type quantified over.
-</para>
+<sect3><title>Warnings</title>
<para>
-As for type signatures, implicit quantification happens for non-overloaded
-types too. So if you write this:
-
+The monomorphism restriction is even more important than usual.
+Consider the example above:
<programlisting>
- data T a = MkT (Either a b) (b -> b)
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
</programlisting>
-
-it's just as if you had written this:
-
+If we replaced the two occurrences of x' by (newName %ns), which is
+usually a harmless thing to do, we get:
<programlisting>
- data T a = MkT (forall b. Either a b) (forall b. b -> b)
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam (newName %ns) (f env e)
+ where
+ env' = extend env x (newName %ns)
</programlisting>
-
-That is, since the type variable <literal>b</literal> isn't in scope, it's
-implicitly universally quantified. (Arguably, it would be better
-to <emphasis>require</emphasis> explicit quantification on constructor arguments
-where that is what is wanted. Feedback welcomed.)
+But now the name supply is consumed in <emphasis>three</emphasis> places
+(the two calls to newName,and the recursive call to f), so
+the result is utterly different. Urk! We don't even have
+the beta rule.
</para>
-
<para>
-You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
-the constructor to suitable values, just as usual. For example,
+Well, this is an experimental change. With implicit
+parameters we have already lost beta reduction anyway, and
+(as John Launchbury puts it) we can't sensibly reason about
+Haskell programs without knowing their typing.
</para>
-<para>
+</sect3>
+<sect3><title>Recursive functions</title>
+<para>Linear implicit parameters can be particularly tricky when you have a recursive function
+Consider
<programlisting>
- a1 :: T Int
- a1 = T1 (\xy->x) 3
-
- a2, a3 :: Swizzle
- a2 = MkSwizzle sort
- a3 = MkSwizzle reverse
-
- a4 :: MonadT Maybe
- a4 = let r x = Just x
- b m k = case m of
- Just y -> k y
- Nothing -> Nothing
- in
- MkMonad r b
-
- mkTs :: (forall b. b -> b -> b) -> a -> [T a]
- mkTs f x y = [T1 f x, T1 f y]
+ foo :: %x::T => Int -> [Int]
+ foo 0 = []
+ foo n = %x : foo (n-1)
</programlisting>
-
-</para>
-
-<para>
-The type of the argument can, as usual, be more general than the type
-required, as <literal>(MkSwizzle reverse)</literal> shows. (<function>reverse</function>
-does not need the <literal>Ord</literal> constraint.)
-</para>
-
-<para>
-When you use pattern matching, the bound variables may now have
-polymorphic types. For example:
-</para>
-
+where T is some type in class Splittable.</para>
<para>
-
+Do you get a list of all the same T's or all different T's
+(assuming that split gives two distinct T's back)?
+</para><para>
+If you supply the type signature, taking advantage of polymorphic
+recursion, you get what you'd probably expect. Here's the
+translated term, where the implicit param is made explicit:
<programlisting>
- f :: T a -> a -> (a, Char)
- f (T1 w k) x = (w k x, w 'c' 'd')
-
- g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
- g (MkSwizzle s) xs f = s (map f (s xs))
-
- h :: MonadT m -> [m a] -> m [a]
- h m [] = return m []
- h m (x:xs) = bind m x $ \y ->
- bind m (h m xs) $ \ys ->
- return m (y:ys)
+ foo x 0 = []
+ foo x n = let (x1,x2) = split x
+ in x1 : foo x2 (n-1)
</programlisting>
-
-</para>
-
-<para>
-In the function <function>h</function> we use the record selectors <literal>return</literal>
-and <literal>bind</literal> to extract the polymorphic bind and return functions
-from the <literal>MonadT</literal> data structure, rather than using pattern
-matching.
+But if you don't supply a type signature, GHC uses the Hindley
+Milner trick of using a single monomorphic instance of the function
+for the recursive calls. That is what makes Hindley Milner type inference
+work. So the translation becomes
+<programlisting>
+ foo x = let
+ foom 0 = []
+ foom n = x : foom (n-1)
+ in
+ foom
+</programlisting>
+Result: 'x' is not split, and you get a list of identical T's. So the
+semantics of the program depends on whether or not foo has a type signature.
+Yikes!
+</para><para>
+You may say that this is a good reason to dislike linear implicit parameters
+and you'd be right. That is why they are an experimental feature.
</para>
</sect3>
-<sect3>
-<title>Type inference</title>
+</sect2>
+
+================ END OF Linear Implicit Parameters commented out -->
+
+<sect2 id="kinding">
+<title>Explicitly-kinded quantification</title>
<para>
-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:
+Haskell infers the kind of each type variable. Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation,
+just as it is nice to give a type signature for a function. On some occasions,
+it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+<screen>
+ data Set cxt a = Set [a]
+ | Unused (cxt a -> ())
+</screen>
+The only use for the <literal>Unused</literal> constructor was to force the correct
+kind for the type variable <literal>cxt</literal>.
</para>
<para>
-<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
-provides an explicit polymorphic type for x, or GHC's type inference will assume
-that x's type has no foralls in it</emphasis>.
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound. Namely:
+<itemizedlist>
+<listitem><para><literal>data</literal> declarations:
+<screen>
+ data Set (cxt :: * -> *) a = Set [a]
+</screen></para></listitem>
+<listitem><para><literal>type</literal> declarations:
+<screen>
+ type T (f :: * -> *) = f Int
+</screen></para></listitem>
+<listitem><para><literal>class</literal> declarations:
+<screen>
+ class (Eq a) => C (f :: * -> *) a where ...
+</screen></para></listitem>
+<listitem><para><literal>forall</literal>'s in type signatures:
+<screen>
+ f :: forall (cxt :: * -> *). Set cxt Int
+</screen></para></listitem>
+</itemizedlist>
</para>
+
<para>
-What does it mean to "provide" an explicit type for x? You can do that by
-giving a type signature for x directly, using a pattern type signature
-(<xref linkend="scoped-type-variables"/>), thus:
-<programlisting>
- \ f :: (forall a. a->a) -> (f True, f 'c')
-</programlisting>
-Alternatively, you can give a type signature to the enclosing
-context, which GHC can "push down" to find the type for the variable:
-<programlisting>
- (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
-</programlisting>
-Here the type signature on the expression can be pushed inwards
-to give a type signature for f. Similarly, and more commonly,
-one can give a type signature for the function itself:
-<programlisting>
- h :: (forall a. a->a) -> (Bool,Char)
- h f = (f True, f 'c')
-</programlisting>
-You don't need to give a type signature if the lambda bound variable
-is a constructor argument. Here is an example we saw earlier:
-<programlisting>
- f :: T a -> a -> (a, Char)
- f (T1 w k) x = (w k x, w 'c' 'd')
-</programlisting>
-Here we do not need to give a type signature to <literal>w</literal>, because
-it is an argument of constructor <literal>T1</literal> and that tells GHC all
-it needs to know.
+The parentheses are required. Some of the spaces are required too, to
+separate the lexemes. If you write <literal>(f::*->*)</literal> you
+will get a parse error, because "<literal>::*->*</literal>" is a
+single lexeme in Haskell.
</para>
-</sect3>
+<para>
+As part of the same extension, you can put kind annotations in types
+as well. Thus:
+<screen>
+ f :: (Int :: *) -> Int
+ g :: forall a. a -> (a :: *)
+</screen>
+The syntax is
+<screen>
+ atype ::= '(' ctype '::' kind ')
+</screen>
+The parentheses are required.
+</para>
+</sect2>
-<sect3 id="implicit-quant">
-<title>Implicit quantification</title>
+<sect2 id="universal-quantification">
+<title>Arbitrary-rank polymorphism
+</title>
<para>
-GHC performs implicit quantification as follows. <emphasis>At the top level (only) of
-user-written types, if and only if there is no explicit <literal>forall</literal>,
-GHC finds all the type variables mentioned in the type that are not already
-in scope, and universally quantifies them.</emphasis> For example, the following pairs are
-equivalent:
-<programlisting>
- f :: a -> a
- f :: forall a. a -> a
-
- g (x::a) = let
- h :: a -> b -> b
- h x y = y
- in ...
- g (x::a) = let
- h :: forall b. a -> b -> b
- h x y = y
- in ...
-</programlisting>
+Haskell type signatures are implicitly quantified. The new keyword <literal>forall</literal>
+allows us to say exactly what this means. For example:
</para>
<para>
-Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
-point. For example:
<programlisting>
- f :: (a -> a) -> Int
- -- MEANS
- f :: forall a. (a -> a) -> Int
- -- NOT
- f :: (forall a. a -> a) -> Int
-
-
- g :: (Ord a => a -> a) -> Int
- -- MEANS the illegal type
- g :: forall a. (Ord a => a -> a) -> Int
- -- NOT
- g :: (forall a. Ord a => a -> a) -> Int
+ g :: b -> b
</programlisting>
-The latter produces an illegal type, which you might think is silly,
-but at least the rule is simple. If you want the latter type, you
-can write your for-alls explicitly. Indeed, doing so is strongly advised
-for rank-2 types.
-</para>
-</sect3>
-</sect2>
-
-
-<sect2 id="impredicative-polymorphism">
-<title>Impredicative polymorphism
-</title>
-<para>GHC supports <emphasis>impredicative polymorphism</emphasis>. This means
-that you can call a polymorphic function at a polymorphic type, and
-parameterise data structures over polymorphic types. For example:
+means this:
<programlisting>
- f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
- f (Just g) = Just (g [3], g "hello")
- f Nothing = Nothing
+ g :: forall b. (b -> b)
</programlisting>
-Notice here that the <literal>Maybe</literal> type is parameterised by the
-<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
-[a])</literal>.
-</para>
-<para>The technical details of this extension are described in the paper
-<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy">Boxy types:
-type inference for higher-rank types and impredicativity</ulink>,
-which appeared at ICFP 2006.
+The two are treated identically.
</para>
-</sect2>
-
-<sect2 id="scoped-type-variables">
-<title>Lexically scoped type variables
-</title>
<para>
-GHC supports <emphasis>lexically scoped type variables</emphasis>, without
-which some type signatures are simply impossible to write. For example:
+However, GHC's type system supports <emphasis>arbitrary-rank</emphasis>
+explicit universal quantification in
+types.
+For example, all the following types are legal:
<programlisting>
-f :: forall a. [a] -> [a]
-f xs = ys ++ ys
- where
- ys :: [a]
- ys = reverse xs
+ f1 :: forall a b. a -> b -> a
+ g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
+
+ f2 :: (forall a. a->a) -> Int -> Int
+ g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+
+ f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+
+ f4 :: Int -> (forall a. a -> a)
</programlisting>
-The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope; it scopes over
-the entire definition of <literal>f</literal>.
-In particular, it is in scope at the type signature for <varname>ys</varname>.
-In Haskell 98 it is not possible to declare
-a type for <varname>ys</varname>; a major benefit of scoped type variables is that
-it becomes possible to do so.
+Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
+can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
+The <literal>forall</literal> makes explicit the universal quantification that
+is implicitly added by Haskell.
</para>
-<para>Lexically-scoped type variables are enabled by
-<option>-fglasgow-exts</option>.
+<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 arrow. As <literal>g2</literal>
+shows, the polymorphic type on the left of the function arrow can be overloaded.
</para>
-<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
-variables work, compared to earlier releases. Read this section
-carefully!</para>
-
-<sect3>
-<title>Overview</title>
-
-<para>The design follows the following principles
-<itemizedlist>
-<listitem><para>A scoped type variable stands for a type <emphasis>variable</emphasis>, and not for
-a <emphasis>type</emphasis>. (This is a change from GHC's earlier
-design.)</para></listitem>
-<listitem><para>Furthermore, distinct lexical type variables stand for distinct
-type variables. This means that every programmer-written type signature
-(includin one that contains free scoped type variables) denotes a
-<emphasis>rigid</emphasis> type; that is, the type is fully known to the type
-checker, and no inference is involved.</para></listitem>
-<listitem><para>Lexical type variables may be alpha-renamed freely, without
-changing the program.</para></listitem>
-</itemizedlist>
+<para>
+The function <literal>f3</literal> has a rank-3 type;
+it has rank-2 types on the left of a function arrow.
</para>
<para>
-A <emphasis>lexically scoped type variable</emphasis> can be bound by:
+GHC allows types of arbitrary rank; you can nest <literal>forall</literal>s
+arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
+that restriction has now been lifted.)
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
<itemizedlist>
-<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
-<listitem><para>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
-<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
-<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
+<listitem> <para> On the left or right (see <literal>f4</literal>, for example)
+of a function arrow </para> </listitem>
+<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the <literal>f1,f2,f3,g1,g2</literal> above would be valid
+field type signatures.</para> </listitem>
+<listitem> <para> As the type of an implicit parameter </para> </listitem>
+<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables"/>) </para> </listitem>
</itemizedlist>
+Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
+a type variable any more!
</para>
+
+
+<sect3 id="univ">
+<title>Examples
+</title>
+
<para>
-In Haskell, a programmer-written type signature is implicitly quantifed over
-its free type variables (<ulink
-url="http://haskell.org/onlinereport/decls.html#sect4.1.2">Section
-4.1.2</ulink>
-of the Haskel Report).
-Lexically scoped type variables affect this implicit quantification rules
-as follows: any type variable that is in scope is <emphasis>not</emphasis> universally
-quantified. For example, if type variable <literal>a</literal> is in scope,
-then
-<programlisting>
- (e :: a -> a) means (e :: a -> a)
- (e :: b -> b) means (e :: forall b. b->b)
- (e :: a -> b) means (e :: forall b. a->b)
-</programlisting>
+In a <literal>data</literal> or <literal>newtype</literal> declaration one can quantify
+the types of the constructor arguments. Here are several examples:
</para>
+<para>
-</sect3>
+<programlisting>
+data T a = T1 (forall b. b -> b -> b) a
+data MonadT m = MkMonad { return :: forall a. a -> m a,
+ bind :: forall a b. m a -> (a -> m b) -> m b
+ }
-<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 ]
+newtype Swizzle = MkSwizzle (Ord a => [a] -> [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>
+The constructors have rank-2 types:
</para>
-</sect3>
-<sect3 id="exp-type-sigs">
-<title>Expression type signatures</title>
+<para>
-<para>An expression type signature that has <emphasis>explicit</emphasis>
-quantification (using <literal>forall</literal>) brings into scope the
-explicitly-quantified
-type variables, in the annotated expression. For example:
<programlisting>
- f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
+T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
+MkMonad :: forall m. (forall a. a -> m a)
+ -> (forall a b. m a -> (a -> m b) -> m b)
+ -> MonadT m
+MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
</programlisting>
-Here, the type signature <literal>forall a. ST s Bool</literal> brings the
-type variable <literal>s</literal> into scope, in the annotated expression
-<literal>(op >>= \(x :: STRef s Int) -> g x)</literal>.
-</para>
-</sect3>
+</para>
-<sect3 id="pattern-type-sigs">
-<title>Pattern type signatures</title>
<para>
-A type signature may occur in any pattern; this is a <emphasis>pattern type
-signature</emphasis>.
-For example:
-<programlisting>
- -- f and g assume that 'a' is already in scope
- f = \(x::Int, y::a) -> x
- g (x::a) = x
- h ((x,y) :: (Int,Bool)) = (y,x)
-</programlisting>
-In the case where all the type variables in the pattern type sigature are
-already in scope (i.e. bound by the enclosing context), matters are simple: the
-signature simply constrains the type of the pattern in the obvious way.
+Notice that you don't need to use a <literal>forall</literal> if there's an
+explicit context. For example in the first argument of the
+constructor <function>MkSwizzle</function>, an implicit "<literal>forall a.</literal>" is
+prefixed to the argument type. The implicit <literal>forall</literal>
+quantifies all type variables that are not already in scope, and are
+mentioned in the type quantified over.
</para>
+
<para>
-There is only one situation in which you can write a pattern type signature that
-mentions a type variable that is not already in scope, namely in pattern match
-of an existential data constructor. For example:
+As for type signatures, implicit quantification happens for non-overloaded
+types too. So if you write this:
+
<programlisting>
- data T = forall a. MkT [a]
+ data T a = MkT (Either a b) (b -> b)
+</programlisting>
- k :: T -> T
- k (MkT [t::a]) = MkT t3
- where
- t3::[a] = [t,t,t]
+it's just as if you had written this:
+
+<programlisting>
+ data T a = MkT (forall b. Either a b) (forall b. b -> b)
</programlisting>
-Here, the pattern type signature <literal>(t::a)</literal> mentions a lexical type
-variable that is not already in scope. Indeed, it cannot already be in scope,
-because it is bound by the pattern match. GHC's rule is that in this situation
-(and only then), a pattern type signature can mention a type variable that is
-not already in scope; the effect is to bring it into scope, standing for the
-existentially-bound type variable.
+
+That is, since the type variable <literal>b</literal> isn't in scope, it's
+implicitly universally quantified. (Arguably, it would be better
+to <emphasis>require</emphasis> explicit quantification on constructor arguments
+where that is what is wanted. Feedback welcomed.)
</para>
+
<para>
-If this seems a little odd, we think so too. But we must have
-<emphasis>some</emphasis> way to bring such type variables into scope, else we
-could not name existentially-bound type variables in subequent type signatures.
+You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
+the constructor to suitable values, just as usual. For example,
</para>
+
<para>
-This is (now) the <emphasis>only</emphasis> situation in which a pattern type
-signature is allowed to mention a lexical variable that is not already in
-scope.
-For example, both <literal>f</literal> and <literal>g</literal> would be
-illegal if <literal>a</literal> was not already in scope.
-</para>
+<programlisting>
+ a1 :: T Int
+ a1 = T1 (\xy->x) 3
+
+ a2, a3 :: Swizzle
+ a2 = MkSwizzle sort
+ a3 = MkSwizzle reverse
+
+ a4 :: MonadT Maybe
+ a4 = let r x = Just x
+ b m k = case m of
+ Just y -> k y
+ Nothing -> Nothing
+ in
+ MkMonad r b
-</sect3>
+ mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+ mkTs f x y = [T1 f x, T1 f y]
+</programlisting>
-<!-- ==================== Commented out part about result type signatures
+</para>
-<sect3 id="result-type-sigs">
-<title>Result type signatures</title>
+<para>
+The type of the argument can, as usual, be more general than the type
+required, as <literal>(MkSwizzle reverse)</literal> shows. (<function>reverse</function>
+does not need the <literal>Ord</literal> constraint.)
+</para>
+
+<para>
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example:
+</para>
<para>
-The result type of a function, lambda, or case expression alternative can be given a signature, thus:
<programlisting>
- {- f assumes that 'a' is already in scope -}
- f x y :: [a] = [x,y,x]
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
- g = \ x :: [Int] -> [3,4]
+ g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
+ g (MkSwizzle s) xs f = s (map f (s xs))
- h :: forall a. [a] -> a
- h xs = case xs of
- (y:ys) :: a -> y
+ h :: MonadT m -> [m a] -> m [a]
+ h m [] = return m []
+ h m (x:xs) = bind m x $ \y ->
+ bind m (h m xs) $ \ys ->
+ return m (y:ys)
</programlisting>
-The final <literal>:: [a]</literal> after the patterns of <literal>f</literal> gives the type of
-the result of the function. Similarly, the body of the lambda in the RHS of
-<literal>g</literal> is <literal>[Int]</literal>, and the RHS of the case
-alternative in <literal>h</literal> is <literal>a</literal>.
+
</para>
-<para> A result type signature never brings new type variables into scope.</para>
+
<para>
-There are a couple of syntactic wrinkles. First, notice that all three
-examples would parse quite differently with parentheses:
-<programlisting>
- {- f assumes that 'a' is already in scope -}
- f x (y :: [a]) = [x,y,x]
+In the function <function>h</function> we use the record selectors <literal>return</literal>
+and <literal>bind</literal> to extract the polymorphic bind and return functions
+from the <literal>MonadT</literal> data structure, rather than using pattern
+matching.
+</para>
+</sect3>
- g = \ (x :: [Int]) -> [3,4]
+<sect3>
+<title>Type inference</title>
- h :: forall a. [a] -> a
- h xs = case xs of
- ((y:ys) :: a) -> y
+<para>
+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:
+</para>
+<para>
+<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it</emphasis>.
+</para>
+<para>
+What does it mean to "provide" an explicit type for x? You can do that by
+giving a type signature for x directly, using a pattern type signature
+(<xref linkend="scoped-type-variables"/>), thus:
+<programlisting>
+ \ f :: (forall a. a->a) -> (f True, f 'c')
</programlisting>
-Now the signature is on the <emphasis>pattern</emphasis>; and
-<literal>h</literal> would certainly be ill-typed (since the pattern
-<literal>(y:ys)</literal> cannot have the type <literal>a</literal>.
-
-Second, to avoid ambiguity, the type after the “<literal>::</literal>” in a result
-pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
-token or a parenthesised type of some sort). To see why,
-consider how one would parse this:
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
<programlisting>
- \ x :: a -> b -> x
+ (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
+</programlisting>
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f. Similarly, and more commonly,
+one can give a type signature for the function itself:
+<programlisting>
+ h :: (forall a. a->a) -> (Bool,Char)
+ h f = (f True, f 'c')
+</programlisting>
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument. Here is an example we saw earlier:
+<programlisting>
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
</programlisting>
+Here we do not need to give a type signature to <literal>w</literal>, because
+it is an argument of constructor <literal>T1</literal> and that tells GHC all
+it needs to know.
</para>
-</sect3>
- -->
+</sect3>
-<sect3 id="cls-inst-scoped-tyvars">
-<title>Class and instance declarations</title>
-<para>
-The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
-scope over the methods defined in the <literal>where</literal> part. For example:
+<sect3 id="implicit-quant">
+<title>Implicit quantification</title>
+<para>
+GHC performs implicit quantification as follows. <emphasis>At the top level (only) of
+user-written types, if and only if there is no explicit <literal>forall</literal>,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them.</emphasis> For example, the following pairs are
+equivalent:
+<programlisting>
+ f :: a -> a
+ f :: forall a. a -> a
+ g (x::a) = let
+ h :: a -> b -> b
+ h x y = y
+ in ...
+ g (x::a) = let
+ h :: forall b. a -> b -> b
+ h x y = y
+ in ...
+</programlisting>
+</para>
+<para>
+Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
+point. For example:
<programlisting>
- class C a where
- op :: [a] -> a
+ f :: (a -> a) -> Int
+ -- MEANS
+ f :: forall a. (a -> a) -> Int
+ -- NOT
+ f :: (forall a. a -> a) -> Int
- op xs = let ys::[a]
- ys = reverse xs
- in
- head ys
+
+ g :: (Ord a => a -> a) -> Int
+ -- MEANS the illegal type
+ g :: forall a. (Ord a => a -> a) -> Int
+ -- NOT
+ g :: (forall a. Ord a => a -> a) -> Int
</programlisting>
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple. If you want the latter type, you
+can write your for-alls explicitly. Indeed, doing so is strongly advised
+for rank-2 types.
</para>
</sect3>
-
</sect2>
-<sect2 id="deriving-typeable">
-<title>Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal></title>
-<para>
-Haskell 98 allows the programmer to add "<literal>deriving( Eq, Ord )</literal>" to a data type
-declaration, to generate a standard instance declaration for classes specified in the <literal>deriving</literal> clause.
-In Haskell 98, the only classes that may appear in the <literal>deriving</literal> clause are the standard
-classes <literal>Eq</literal>, <literal>Ord</literal>,
-<literal>Enum</literal>, <literal>Ix</literal>, <literal>Bounded</literal>, <literal>Read</literal>, and <literal>Show</literal>.
-</para>
-<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.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.
+<sect2 id="impredicative-polymorphism">
+<title>Impredicative polymorphism
+</title>
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>. This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types. For example:
+<programlisting>
+ f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+ f (Just g) = Just (g [3], g "hello")
+ f Nothing = Nothing
+</programlisting>
+Notice here that the <literal>Maybe</literal> type is parameterised by the
+<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
+[a])</literal>.
+</para>
+<para>The technical details of this extension are described in the paper
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy">Boxy types:
+type inference for higher-rank types and impredicativity</ulink>,
+which appeared at ICFP 2006.
</para>
</sect2>
-<sect2 id="newtype-deriving">
-<title>Generalised derived instances for newtypes</title>
+<sect2 id="scoped-type-variables">
+<title>Lexically scoped type variables
+</title>
<para>
-When you define an abstract type using <literal>newtype</literal>, you may want
-the new type to inherit some instances from its representation. In
-Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
-<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
-other classes you have to write an explicit instance declaration. For
-example, if you define
-
-<programlisting>
- newtype Dollars = Dollars Int
-</programlisting>
-
-and you want to use arithmetic on <literal>Dollars</literal>, you have to
-explicitly define an instance of <literal>Num</literal>:
-
-<programlisting>
- instance Num Dollars where
- Dollars a + Dollars b = Dollars (a+b)
- ...
+GHC supports <emphasis>lexically scoped type variables</emphasis>, without
+which some type signatures are simply impossible to write. For example:
+<programlisting>
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
</programlisting>
-All the instance does is apply and remove the <literal>newtype</literal>
-constructor. It is particularly galling that, since the constructor
-doesn't appear at run-time, this instance declaration defines a
-dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
-dictionary, only slower!
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope; it scopes over
+the entire definition of <literal>f</literal>.
+In particular, it is in scope at the type signature for <varname>ys</varname>.
+In Haskell 98 it is not possible to declare
+a type for <varname>ys</varname>; a major benefit of scoped type variables is that
+it becomes possible to do so.
+</para>
+<para>Lexically-scoped type variables are enabled by
+<option>-fglasgow-exts</option>.
</para>
+<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
+variables work, compared to earlier releases. Read this section
+carefully!</para>
+<sect3>
+<title>Overview</title>
-<sect3> <title> Generalising the deriving clause </title>
+<para>The design follows the following principles
+<itemizedlist>
+<listitem><para>A scoped type variable stands for a type <emphasis>variable</emphasis>, and not for
+a <emphasis>type</emphasis>. (This is a change from GHC's earlier
+design.)</para></listitem>
+<listitem><para>Furthermore, distinct lexical type variables stand for distinct
+type variables. This means that every programmer-written type signature
+(includin one that contains free scoped type variables) denotes a
+<emphasis>rigid</emphasis> type; that is, the type is fully known to the type
+checker, and no inference is involved.</para></listitem>
+<listitem><para>Lexical type variables may be alpha-renamed freely, without
+changing the program.</para></listitem>
+</itemizedlist>
+</para>
<para>
-GHC now permits such instances to be derived instead, so one can write
-<programlisting>
- newtype Dollars = Dollars Int deriving (Eq,Show,Num)
-</programlisting>
-
-and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
-for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
-derives an instance declaration of the form
-
-<programlisting>
- instance Num Int => Num Dollars
-</programlisting>
-
-which just adds or removes the <literal>newtype</literal> constructor according to the type.
+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>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
+<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
+<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
+</itemizedlist>
</para>
<para>
+In Haskell, a programmer-written type signature is implicitly quantifed over
+its free type variables (<ulink
+url="http://haskell.org/onlinereport/decls.html#sect4.1.2">Section
+4.1.2</ulink>
+of the Haskel Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is <emphasis>not</emphasis> universally
+quantified. For example, if type variable <literal>a</literal> is in scope,
+then
+<programlisting>
+ (e :: a -> a) means (e :: a -> a)
+ (e :: b -> b) means (e :: forall b. b->b)
+ (e :: a -> b) means (e :: forall b. a->b)
+</programlisting>
+</para>
-We can also derive instances of constructor classes in a similar
-way. For example, suppose we have implemented state and failure monad
-transformers, such that
-<programlisting>
- instance Monad m => Monad (State s m)
- instance Monad m => Monad (Failure m)
-</programlisting>
-In Haskell 98, we can define a parsing monad by
-<programlisting>
- type Parser tok m a = State [tok] (Failure m) a
-</programlisting>
+</sect3>
-which is automatically a monad thanks to the instance declarations
-above. With the extension, we can make the parser type abstract,
-without needing to write an instance of class <literal>Monad</literal>, via
-<programlisting>
- newtype Parser tok m a = Parser (State [tok] (Failure m) a)
- deriving Monad
+<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>
-In this case the derived instance declaration is of the form
-<programlisting>
- instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
-</programlisting>
-
-Notice that, since <literal>Monad</literal> is a constructor class, the
-instance is a <emphasis>partial application</emphasis> of the new type, not the
-entire left hand side. We can imagine that the type declaration is
-``eta-converted'' to generate the context of the instance
-declaration.
+The "<literal>forall a</literal>" brings "<literal>a</literal>" into scope in
+the definition of "<literal>f</literal>".
</para>
-<para>
-
-We can even derive instances of multi-parameter classes, provided the
-newtype is the last class parameter. In this case, a ``partial
-application'' of the class appears in the <literal>deriving</literal>
-clause. For example, given the class
-
-<programlisting>
- class StateMonad s m | m -> s where ...
- instance Monad m => StateMonad s (State s m) where ...
-</programlisting>
-then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by
-<programlisting>
- newtype Parser tok m a = Parser (State [tok] (Failure m) a)
- deriving (Monad, StateMonad [tok])
+<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>
-The derived instance is obtained by completing the application of the
-class to the new type:
+<sect3 id="exp-type-sigs">
+<title>Expression type signatures</title>
-<programlisting>
- instance StateMonad [tok] (State [tok] (Failure m)) =>
- StateMonad [tok] (Parser tok m)
+<para>An expression type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression. For example:
+<programlisting>
+ f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
</programlisting>
+Here, the type signature <literal>forall a. ST s Bool</literal> brings the
+type variable <literal>s</literal> into scope, in the annotated expression
+<literal>(op >>= \(x :: STRef s Int) -> g x)</literal>.
</para>
-<para>
-As a result of this extension, all derived instances in newtype
- 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.
-</para>
</sect3>
-<sect3> <title> A more precise specification </title>
+<sect3 id="pattern-type-sigs">
+<title>Pattern type signatures</title>
<para>
-Derived instance declarations are constructed as follows. Consider the
-declaration (after expansion of any type synonyms)
-
-<programlisting>
- newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm)
-</programlisting>
-
-where
- <itemizedlist>
-<listitem><para>
- The <literal>ci</literal> are partial applications of
- classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
- is exactly <literal>j+1</literal>. That is, <literal>C</literal> lacks exactly one type argument.
-</para></listitem>
-<listitem><para>
- The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.
-</para></listitem>
-<listitem><para>
- The type <literal>t</literal> is an arbitrary type.
-</para></listitem>
-<listitem><para>
- The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>,
- nor in the <literal>ci</literal>, and
-</para></listitem>
-<listitem><para>
- None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>,
- <literal>Typeable</literal>, or <literal>Data</literal>. These classes
- should not "look through" the type or its constructor. You can still
- derive these classes for a newtype, but it happens in the usual way, not
- via this new mechanism.
-</para></listitem>
-</itemizedlist>
-Then, for each <literal>ci</literal>, the derived instance
-declaration is:
-<programlisting>
- instance ci t => ci (T v1...vk)
-</programlisting>
-As an example which does <emphasis>not</emphasis> work, consider
-<programlisting>
- newtype NonMonad m s = NonMonad (State s m s) deriving Monad
-</programlisting>
-Here we cannot derive the instance
-<programlisting>
- instance Monad (State s m) => Monad (NonMonad m)
-</programlisting>
-
-because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
-and so cannot be "eta-converted" away. It is a good thing that this
-<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
-not, in fact, a monad --- for the same reason. Try defining
-<literal>>>=</literal> with the correct type: you won't be able to.
+A type signature may occur in any pattern; this is a <emphasis>pattern type
+signature</emphasis>.
+For example:
+<programlisting>
+ -- f and g assume that 'a' is already in scope
+ f = \(x::Int, y::a) -> x
+ g (x::a) = x
+ h ((x,y) :: (Int,Bool)) = (y,x)
+</programlisting>
+In the case where all the type variables in the pattern type sigature are
+already in scope (i.e. bound by the enclosing context), matters are simple: the
+signature simply constrains the type of the pattern in the obvious way.
</para>
<para>
+There is only one situation in which you can write a pattern type signature that
+mentions a type variable that is not already in scope, namely in pattern match
+of an existential data constructor. For example:
+<programlisting>
+ data T = forall a. MkT [a]
-Notice also that the <emphasis>order</emphasis> of class parameters becomes
-important, since we can only derive instances for the last one. If the
-<literal>StateMonad</literal> class above were instead defined as
-
-<programlisting>
- class StateMonad m s | m -> s where ...
+ k :: T -> T
+ k (MkT [t::a]) = MkT t3
+ where
+ t3::[a] = [t,t,t]
</programlisting>
-
-then we would not have been able to derive an instance for the
-<literal>Parser</literal> type above. We hypothesise that multi-parameter
-classes usually have one "main" parameter for which deriving new
-instances is most interesting.
+Here, the pattern type signature <literal>(t::a)</literal> mentions a lexical type
+variable that is not already in scope. Indeed, it cannot already be in scope,
+because it is bound by the pattern match. GHC's rule is that in this situation
+(and only then), a pattern type signature can mention a type variable that is
+not already in scope; the effect is to bring it into scope, standing for the
+existentially-bound type variable.
</para>
-<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>
+If this seems a little odd, we think so too. But we must have
+<emphasis>some</emphasis> way to bring such type variables into scope, else we
+could not name existentially-bound type variables in subequent type signatures.
+</para>
+<para>
+This is (now) the <emphasis>only</emphasis> situation in which a pattern type
+signature is allowed to mention a lexical variable that is not already in
+scope.
+For example, both <literal>f</literal> and <literal>g</literal> would be
+illegal if <literal>a</literal> was not already in scope.
</para>
+
+
</sect3>
-</sect2>
+<!-- ==================== Commented out part about result type signatures
-<sect2 id="stand-alone-deriving">
-<title>Stand-alone deriving declarations</title>
+<sect3 id="result-type-sigs">
+<title>Result type signatures</title>
<para>
-GHC now allows stand-alone <literal>deriving</literal> declarations:
-</para>
+The result type of a function, lambda, or case expression alternative can be given a signature, thus:
<programlisting>
- data Foo = Bar Int | Baz String
+ {- f assumes that 'a' is already in scope -}
+ f x y :: [a] = [x,y,x]
- deriving Eq for Foo
+ g = \ x :: [Int] -> [3,4]
+
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ (y:ys) :: a -> y
</programlisting>
+The final <literal>:: [a]</literal> after the patterns of <literal>f</literal> gives the type of
+the result of the function. Similarly, the body of the lambda in the RHS of
+<literal>g</literal> is <literal>[Int]</literal>, and the RHS of the case
+alternative in <literal>h</literal> is <literal>a</literal>.
+</para>
+<para> A result type signature never brings new type variables into scope.</para>
+<para>
+There are a couple of syntactic wrinkles. First, notice that all three
+examples would parse quite differently with parentheses:
+<programlisting>
+ {- f assumes that 'a' is already in scope -}
+ f x (y :: [a]) = [x,y,x]
-<para>Deriving instances of multi-parameter type classes for newtypes is
-also allowed:</para>
+ g = \ (x :: [Int]) -> [3,4]
-<programlisting>
- newtype Foo a = MkFoo (State Int a)
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ ((y:ys) :: a) -> y
+</programlisting>
+Now the signature is on the <emphasis>pattern</emphasis>; and
+<literal>h</literal> would certainly be ill-typed (since the pattern
+<literal>(y:ys)</literal> cannot have the type <literal>a</literal>.
- deriving (MonadState Int) for Foo
+Second, to avoid ambiguity, the type after the “<literal>::</literal>” in a result
+pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
+token or a parenthesised type of some sort). To see why,
+consider how one would parse this:
+<programlisting>
+ \ x :: a -> b -> x
</programlisting>
+</para>
+</sect3>
+
+ -->
+<sect3 id="cls-inst-scoped-tyvars">
+<title>Class and instance declarations</title>
<para>
+
+The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
+scope over the methods defined in the <literal>where</literal> part. For example:
+
+
+<programlisting>
+ class C a where
+ op :: [a] -> a
+
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
+</programlisting>
</para>
+</sect3>
</sect2>
+
<sect2 id="typing-binds">
<title>Generalised typing of mutually recursive bindings</title>
</para>
</sect2>
-</sect1>
-<!-- ==================== End of type system extensions ================= -->
-
-<!-- ====================== Generalised algebraic data types ======================= -->
-
-<sect1 id="gadt">
-<title>Generalised Algebraic Data Types (GADTs)</title>
+<sect2 id="overloaded-strings">
+<title>Overloaded string literals
+</title>
-<para>Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you
-to give the type signatures of constructors explicitly. For example:
+<para>
+GHC supports <emphasis>overloaded string literals</emphasis>. Normally a
+string literal has type <literal>String</literal>, but with overloaded string
+literals enabled (with <literal>-foverloaded-strings</literal>)
+ a string literal has type <literal>(IsString a) => a</literal>.
+</para>
+<para>
+This means that the usual string syntax can be used, e.g., for packed strings
+and other variations of string like types. String literals behave very much
+like integer literals, i.e., they can be used in both expressions and patterns.
+If used in a pattern the literal with be replaced by an equality test, in the same
+way as an integer literal is.
+</para>
+<para>
+The class <literal>IsString</literal> is defined as:
<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)
+class IsString a where
+ fromString :: String -> a
</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>:
+The only predefined instance is the obvious one to make strings work as usual:
<programlisting>
- eval :: Term a -> a
- eval (Lit i) = i
- eval (Succ t) = 1 + eval t
- eval (IsZero t) = eval t == 0
- eval (If b e1 e2) = if eval b then eval e1 else eval e2
- eval (Pair e1 e2) = (eval e1, eval e2)
+instance IsString [Char] where
+ fromString cs = cs
</programlisting>
-These and many other examples are given in papers by Hongwei Xi, and
-Tim Sheard. There is a longer introduction
-<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
-and Ralf Hinze's
-<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
-may use different notation to that implemented in GHC.
+The class <literal>IsString</literal> is not in scope by default. If you want to mention
+it explicitly (for exmaple, to give an instance declaration for it), you can import it
+from module <literal>GHC.Exts</literal>.
</para>
<para>
-The rest of this section outlines the extensions to GHC that support GADTs.
-It is far from comprehensive, but the design closely follows that described in
-the paper <ulink
-url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
-unification-based type inference for GADTs</ulink>,
-which appeared in ICFP 2006.
+Haskell's defaulting mechanism is extended to cover string literals, when <option>-foverloaded-strings</option> is specified.
+Specifically:
<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>.
+Each type in a default declaration must be an
+instance of <literal>Num</literal> <emphasis>or</emphasis> of <literal>IsString</literal>.
</para></listitem>
<listitem><para>
-You can use record syntax on a GADT-style data type declaration:
-
-<programlisting>
- data Term a where
- Lit { val :: Int } :: Term Int
- Succ { num :: Term Int } :: Term Int
- Pred { num :: Term Int } :: Term Int
- IsZero { arg :: Term Int } :: Term Bool
- Pair { arg1 :: Term a
- , arg2 :: Term b
- } :: Term (a,b)
- If { cnd :: Term Bool
- , tru :: Term a
- , fls :: Term a
- } :: Term a
-</programlisting>
-For every constructor that has a field <literal>f</literal>, (a) the type of
-field <literal>f</literal> must be the same; and (b) the
-result type of the constructor must be the same; both modulo alpha conversion.
-Hence, in our example, we cannot merge the <literal>num</literal> and <literal>arg</literal>
-fields above into a
-single name. Although their field types are both <literal>Term Int</literal>,
-their selector functions actually have different types:
-
-<programlisting>
- num :: Term Int -> Term Int
- arg :: Term Bool -> Term Int
-</programlisting>
-
-At the moment, record updates are not yet possible with GADT, so support is
-limited to record construction, selection and pattern matching:
-
-<programlisting>
- someTerm :: Term Bool
- someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } }
-
- eval :: Term a -> a
- eval Lit { val = i } = i
- eval Succ { num = t } = eval t + 1
- eval Pred { num = t } = eval t - 1
- eval IsZero { arg = t } = eval t == 0
- eval Pair { arg1 = t1, arg2 = t2 } = (eval t1, eval t2)
- eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t)
-</programlisting>
-
+The standard defaulting rule (<ulink url="http://haskell.org/onlinereport/decls.html#sect4.3.4">Haskell Report, Section 4.3.4</ulink>)
+is extended thus: defaulting applies when all the unresolved constraints involve standard classes
+<emphasis>or</emphasis> <literal>IsString</literal>; and at least one is a numeric class
+<emphasis>or</emphasis> <literal>IsString</literal>.
</para></listitem>
-
-<listitem><para>
-You can use strictness annotations, in the obvious places
-in the constructor type:
+</itemizedlist>
+</para>
+<para>
+A small example:
<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>
+module Main where
-<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 :: Maybe1 a ;
- Just1 :: a -> Maybe1 a
- } deriving( Eq, Ord )
+import GHC.Exts( IsString(..) )
- 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>
+newtype MyString = MyString String deriving (Eq, Show)
+instance IsString MyString where
+ fromString = MyString
-<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>
+greet :: MyString -> MyString
+greet "hello" = "world"
+greet other = other
-<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
+main = do
+ print $ greet "hello"
+ print $ greet "fool"
</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>
+Note that deriving <literal>Eq</literal> is necessary for the pattern matching
+to work since it gets translated into an equality comparison.
</para>
+</sect2>
-<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 ======================= -->
-
+<!-- ==================== End of type system extensions ================= -->
+
<!-- ====================== TEMPLATE HASKELL ======================= -->
<sect1 id="template-haskell">
(It would make sense to do so, but it's hard to implement.)
</para></listitem>
+ <listitem><para>
+ Furthermore, you can only run a function at compile time if it is imported
+ from another module <emphasis>that is not part of a mutually-recursive group of modules
+ that includes the module currently being compiled</emphasis>. For example, when compiling module A,
+ you can only run Template Haskell functions imported from B if B does not import A (directly or indirectly).
+ The reason should be clear: to run B we must compile and run A, but we are currently type-checking A.
+ </para></listitem>
+
<listitem><para>
The flag <literal>-ddump-splices</literal> shows the expansion of all top-level splices as they happen.
</para></listitem>
<!-- ==================== BANG PATTERNS ================= -->
-<sect1 id="sec-bang-patterns">
+<sect1 id="bang-patterns">
<title>Bang patterns
<indexterm><primary>Bang patterns</primary></indexterm>
</title>
Bang patterns are enabled by the flag <option>-fbang-patterns</option>.
</para>
-<sect2 id="sec-bang-patterns-informal">
+<sect2 id="bang-patterns-informal">
<title>Informal description of bang patterns
</title>
<para>
</sect2>
-<sect2 id="sec-bang-patterns-sem">
+<sect2 id="bang-patterns-sem">
<title>Syntax and semantics
</title>
<para>
<!-- ==================== ASSERTIONS ================= -->
-<sect1 id="sec-assertions">
+<sect1 id="assertions">
<title>Assertions
<indexterm><primary>Assertions</primary></indexterm>
</title>
<listitem>
<para>
- <function>length</function>
-</para>
-</listitem>
-<listitem>
-
-<para>
<function>++</function> (on its first argument)
</para>
</listitem>