</para>
</sect2>
+<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="class-method-types">
<title>Class method types
</title>
min = let ?cmp = (<=) in least
</programlisting>
<para>
-Note the following additional constraints:
+Note the following points:
<itemizedlist>
+<listitem><para>
+You may not mix implicit-parameter bindings with ordinary bindings in a
+single <literal>let</literal>
+expression; use two nested <literal>let</literal>s instead.
+</para></listitem>
+
+<listitem><para>
+You may put multiple implicit-parameter bindings in a
+single <literal>let</literal> expression; they are <emphasis>not</emphasis> treated
+as a mutually recursive group (as ordinary <literal>let</literal> bindings are).
+Instead they are treated as a non-recursive group, each scoping over the bindings that
+follow. For example, consider:
+<programlisting>
+ f y = let { ?x = y; ?x = ?x+1 } in ?x
+</programlisting>
+This function adds one to its argument.
+</para></listitem>
+
+<listitem><para>
+You may not have an implicit-parameter binding in a <literal>where</literal> clause,
+only in a <literal>let</literal> binding.
+</para></listitem>
+
<listitem>
<para> You can't have an implicit parameter in the context of a class or instance
declaration. For example, both these declarations are illegal:
</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>
<sect2 id="functional-dependencies">
</title>
<para> Functional dependencies are implemented as described by Mark Jones
-in "Type Classes with Functional Dependencies", Mark P. 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.
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
+.
</para>
<para>
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>
+</para>
</sect2>
</sect3>
</sect2>
-<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>
</sect1>
<!-- ==================== End of type system extensions ================= -->
</para>
</sect2>
+<!-- ===================== Recursive do-notation =================== -->
+
+<sect2 id="mdo-notation">
+<title>The recursive do-notation
+</title>
+
+<para> The recursive do-notation (also known as mdo-notation) is implemented as described in
+"A recursive do for Haskell",
+Levent Erkok, John Launchbury",
+Haskell Workshop 2002, pages: 29-37. Pittsburgh, Pennsylvania.
+</para>
+<para>
+The do-notation of Haskell does not allow <emphasis>recursive bindings</emphasis>,
+that is, the variables bound in a do-expression are visible only in the textually following
+code block. Compare this to a let-expression, where bound variables are visible in the entire binding
+group. It turns out that several applications can benefit from recursive bindings in
+the do-notation, and this extension provides the necessary syntactic support.
+</para>
+<para>
+Here is a simple (yet contrived) example:
+</para>
+<programlisting>
+justOnes = mdo xs <- Just (1:xs)
+ return xs
+</programlisting>
+<para>
+As you can guess <literal>justOnes</literal> will evaluate to <literal>Just [1,1,1,...</literal>.
+</para>
+
+<para>
+The MonadFix library introduces the <literal>MonadFix</literal> class. It's definition is:
+</para>
+<programlisting>
+class Monad m => MonadFix m where
+ mfix :: (a -> m a) -> m a
+</programlisting>
+<para>
+The function <literal>mfix</literal>
+dictates how the required recursion operation should be performed. If recursive bindings are required for a monad,
+then that monad must be declared an instance of the <literal>MonadFix</literal> class.
+For details, see the above mentioned reference.
+</para>
+<para>
+The <literal>MonadFix</literal> library automatically declares List, Maybe, IO, and
+state monads (both lazy and strict) as instances of the <literal>MonadFix</literal> class.
+</para>
+<para>
+There are three important points in using the recursive-do notation:
+<itemizedlist>
+<listitem><para>
+The recursive version of the do-notation uses the keyword <literal>mdo</literal> (rather
+than <literal>do</literal>).
+</para></listitem>
+
+<listitem><para>
+If you want to declare an instance of the <literal>MonadFix</literal> class for one of
+your own monads, or you need to refer to the class name <literal>MonadFix</literal> in any other way (for instance in
+writing a type constraint), then your program should <literal>import Control.Monad.MonadFix</literal>.
+Otherwise, you don't need to import any special libraries to use the mdo-notation. That is,
+as long as you only use the predefined instances mentioned above, the mdo-notation will
+be automatically available. (Note: This differs from the Hugs implementation, where
+<literal>MonadFix</literal> should always be imported.)
+</para></listitem>
+
+<listitem><para>
+As with other extensions, ghc should be given the flag <literal>-fglasgow-exts</literal>
+</para></listitem>
+</itemizedlist>
+</para>
+
+<para>
+Historical note: The originial implementation of the mdo-notation, and most
+of the existing documents, use the names
+<literal>MonadRec</literal> for the class, and
+<literal>Control.Monad.MonadRec</literal> for the library. These names
+are no longer supported.
+</para>
+
+<para>
+The web page: <ulink url="http://www.cse.ogi.edu/PacSoft/projects/rmb">http://www.cse.ogi.edu/PacSoft/projects/rmb</ulink>
+contains up to date information on recursive monadic bindings.
+</para>
+
+</sect2>
+
<!-- ===================== PARALLEL LIST COMPREHENSIONS =================== -->
<sect2 id="parallel-list-comprehensions">
"<literal>fromRational 3.2</literal>", not the
Prelude-qualified versions; both in expressions and in
patterns. </para>
+ <para>However, the standard Prelude <literal>Eq</literal> class
+ is still used for the equality test necessary for literal patterns.</para>
</listitem>
<listitem>
instances is most interesting.
</para>
</sect2>
+
</sect1>