Fix scoped type variables for expression type signatures

[ghc-hetmet.git] / docs / users_guide / glasgow_exts.xml

diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 5339c43..f8ad5c1 100644 (file)
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -905,6 +905,38 @@ fromInteger :: Integer -> Bool -> Bool
             you should be all right.</para>
 
 </sect2>
             you should be all right.</para>
 
 </sect2>

+
+<sect2 id="postfix-operators">
+<title>Postfix operators</title>
+
+<para>
+GHC allows a small extension to the syntax of left operator sections, which
+allows you to define postfix operators.  The extension is this:  the left section
+<programlisting>
+  (e !)
+</programlisting> 
+is equivalent (from the point of view of both type checking and execution) to the expression
+<programlisting>
+  ((!) e)
+</programlisting> 
+(for any expression <literal>e</literal> and operator <literal>(!)</literal>.
+The strict Haskell 98 interpretation is that the section is equivalent to
+<programlisting>
+  (\y -> (!) e y)
+</programlisting> 
+That is, the operator must be a function of two arguments.  GHC allows it to
+take only one argument, and that in turn allows you to write the function
+postfix.
+</para>
+<para>Since this extension goes beyond Haskell 98, it should really be enabled
+by a flag; but in fact it is enabled all the time.  (No Haskell 98 programs
+change their behaviour, of course.)
+</para>
+<para>The extension does not extend to the left-hand side of function
+definitions; you must define such a function in prefix form.</para>
+
+</sect2>
+

 </sect1>
 
 
 </sect1>
 
 

@@ -3198,7 +3230,27 @@ for rank-2 types.
 </sect2>
 
 
 </sect2>
 
 

-
+<sect2 id="impredicative-polymorphism">
+<title>Impredicative polymorphism
+</title>
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>.  This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types.  For example:
+<programlisting>
+  f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+  f (Just g) = Just (g [3], g "hello")
+  f Nothing  = Nothing
+</programlisting>
+Notice here that the <literal>Maybe</literal> type is parameterised by the
+<emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
+[a])</literal>.
+</para>
+<para>The technical details of this extension are described in the paper
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy">Boxy types:
+type inference for higher-rank types and impredicativity</ulink>,
+which appeared at ICFP 2006.  
+</para>
+</sect2>

 
 <sect2 id="scoped-type-variables">
 <title>Lexically scoped type variables
 
 <sect2 id="scoped-type-variables">
 <title>Lexically scoped type variables

@@ -3216,7 +3268,7 @@ f xs = ys ++ ys
 </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>.
 </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>y</varname>. 
+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.
 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.

@@ -3249,11 +3301,10 @@ changing the program.</para></listitem>
 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>
 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>
 <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>

-In addition, GHC supports result type signatures (<xref
-linkend="result-type-sigs"/>), although they never bind type variables.

 </para>
 <para>
 In Haskell, a programmer-written type signature is implicitly quantifed over
 </para>
 <para>
 In Haskell, a programmer-written type signature is implicitly quantifed over

@@ -3302,6 +3353,23 @@ quantification rules.
 </para>
 </sect3>
 
 </para>
 </sect3>
 

+<sect3 id="exp-type-sigs">
+<title>Expression type signatures</title>
+
+<para>An expression type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression.  For example:
+<programlisting>
+  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>
+
+</sect3>
+

 <sect3 id="pattern-type-sigs">
 <title>Pattern type signatures</title>
 <para>
 <sect3 id="pattern-type-sigs">
 <title>Pattern type signatures</title>
 <para>

@@ -3310,7 +3378,7 @@ signature</emphasis>.
 For example:
 <programlisting>
   -- f and g assume that 'a' is already in scope
 For example:
 <programlisting>
   -- f and g assume that 'a' is already in scope

-  f = \(x::Int, y) -> x
+  f = \(x::Int, y::a) -> x

   g (x::a) = x
   h ((x,y) :: (Int,Bool)) = (y,x)
 </programlisting>
   g (x::a) = x
   h ((x,y) :: (Int,Bool)) = (y,x)
 </programlisting>

@@ -3352,6 +3420,9 @@ illegal if <literal>a</literal> was not already in scope.
 
 
 </sect3>
 
 
 </sect3>

+
+<!-- ==================== Commented out part about result type signatures 
+

 <sect3 id="result-type-sigs">
 <title>Result type signatures</title>
 
 <sect3 id="result-type-sigs">
 <title>Result type signatures</title>
 

@@ -3359,7 +3430,7 @@ illegal if <literal>a</literal> was not already in scope.
 The result type of a function, lambda, or case expression alternative can be given a signature, thus:
 
 <programlisting>
 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 assumes that 'a' is already in scope -}

   f x y :: [a] = [x,y,x]
 
   g = \ x :: [Int] -> [3,4]
   f x y :: [a] = [x,y,x]
 
   g = \ x :: [Int] -> [3,4]

@@ -3378,7 +3449,7 @@ alternative in <literal>h</literal> is <literal>a</literal>.
 There are a couple of syntactic wrinkles.  First, notice that all three
 examples would parse quite differently with parentheses:
 <programlisting>
 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 assumes that 'a' is already in scope -}

   f x (y :: [a]) = [x,y,x]
 
   g = \ (x :: [Int]) -> [3,4]
   f x (y :: [a]) = [x,y,x]
 
   g = \ (x :: [Int]) -> [3,4]

@@ -3401,6 +3472,8 @@ consider how one would parse this:
 </para>
 </sect3>
 
 </para>
 </sect3>
 

+ -->
+

 <sect3 id="cls-inst-scoped-tyvars">
 <title>Class and instance declarations</title>
 <para>
 <sect3 id="cls-inst-scoped-tyvars">
 <title>Class and instance declarations</title>
 <para>

@@ -3585,16 +3658,19 @@ declaration (after expansion of any type synonyms)
 where 
  <itemizedlist>
 <listitem><para>
 where 
  <itemizedlist>
 <listitem><para>

-  The type <literal>t</literal> is an arbitrary type
+  The <literal>ci</literal> are partial applications of
+  classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
+  is exactly <literal>j+1</literal>.  That is, <literal>C</literal> lacks exactly one type argument.

 </para></listitem>
 <listitem><para>
 </para></listitem>
 <listitem><para>

-  The <literal>vk+1...vn</literal> are type variables which do not occur in 
-  <literal>t</literal>, and
+  The <literal>k</literal> is chosen so that <literal>ci (T v1...vk)</literal> is well-kinded.

 </para></listitem>
 <listitem><para>
 </para></listitem>
 <listitem><para>

-  The <literal>ci</literal> are partial applications of
-  classes of the form <literal>C t1'...tj'</literal>, where the arity of <literal>C</literal>
-  is exactly <literal>j+1</literal>.  That is, <literal>C</literal> lacks exactly one type argument.
+  The type <literal>t</literal> is an arbitrary type.
+</para></listitem>
+<listitem><para>
+  The type variables <literal>vk+1...vn</literal> do not occur in <literal>t</literal>, 
+  nor in the <literal>ci</literal>, and

 </para></listitem>
 <listitem><para>
   None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>, 
 </para></listitem>
 <listitem><para>
   None of the <literal>ci</literal> is <literal>Read</literal>, <literal>Show</literal>, 

@@ -3607,13 +3683,8 @@ where
 Then, for each <literal>ci</literal>, the derived instance
 declaration is:
 <programlisting> 
 Then, for each <literal>ci</literal>, the derived instance
 declaration is:
 <programlisting> 

-  instance ci (t vk+1...v) => ci (T v1...vp)
+  instance ci t => ci (T v1...vk)

 </programlisting>
 </programlisting>

-where <literal>p</literal> is chosen so that <literal>T v1...vp</literal> is of the 
-right <emphasis>kind</emphasis> for the last parameter of class <literal>Ci</literal>.
-</para>
-<para>
-

 As an example which does <emphasis>not</emphasis> work, consider 
 <programlisting> 
   newtype NonMonad m s = NonMonad (State s m s) deriving Monad 
 As an example which does <emphasis>not</emphasis> work, consider 
 <programlisting> 
   newtype NonMonad m s = NonMonad (State s m s) deriving Monad 

@@ -3725,9 +3796,9 @@ pattern binding must have the same context.  For example, this is fine:
 <!-- ====================== Generalised algebraic data types =======================  -->
 
 <sect1 id="gadt">
 <!-- ====================== Generalised algebraic data types =======================  -->
 
 <sect1 id="gadt">

-<title>Generalised Algebraic Data Types</title>
+<title>Generalised Algebraic Data Types (GADTs)</title>

 
 

-<para>Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you
+<para>Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you

 to give the type signatures of constructors explicitly.  For example:
 <programlisting>
   data Term a where
 to give the type signatures of constructors explicitly.  For example:
 <programlisting>
   data Term a where

@@ -3748,9 +3819,20 @@ for these <literal>Terms</literal>:
   eval (If b e1 e2) = if eval b then eval e1 else eval e2
   eval (Pair e1 e2) = (eval e1, eval e2)
 </programlisting>
   eval (If b e1 e2) = if eval b then eval e1 else eval e2
   eval (Pair e1 e2) = (eval e1, eval e2)
 </programlisting>

-These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
+These and many other examples are given in papers by Hongwei Xi, and
+Tim Sheard. There is a longer introduction
+<ulink url="http://haskell.org/haskellwiki/GADT">on the wiki</ulink>,
+and Ralf Hinze's
+<ulink url="http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf">Fun with phantom types</ulink> also has a number of examples. Note that papers
+may use different notation to that implemented in GHC.

 </para>
 </para>

-<para> The extensions to GHC are these:
+<para>
+The rest of this section outlines the extensions to GHC that support GADTs. 
+It is far from comprehensive, but the design closely follows that described in
+the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm">Simple
+unification-based type inference for GADTs</ulink>,
+which appeared in ICFP 2006.

 <itemizedlist>
 <listitem><para>
   Data type declarations have a 'where' form, as exemplified above.  The type signature of
 <itemizedlist>
 <listitem><para>
   Data type declarations have a 'where' form, as exemplified above.  The type signature of

@@ -3842,8 +3924,8 @@ 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 {
 Haskell-98 syntax.   For example, these two declarations are equivalent
 <programlisting>
   data Maybe1 a where {

-      Nothing1 :: Maybe a ;
-      Just1    :: a -> Maybe a
+      Nothing1 :: Maybe1 a ;
+      Just1    :: a -> Maybe1 a

     } deriving( Eq, Ord )
 
   data Maybe2 a = Nothing2 | Just2 a 
     } deriving( Eq, Ord )
 
   data Maybe2 a = Nothing2 | Just2 a 

@@ -3893,19 +3975,26 @@ the result type of the <literal>case</literal> expression.  Hence the addition <
 <sect1 id="template-haskell">
 <title>Template Haskell</title>
 
 <sect1 id="template-haskell">
 <title>Template Haskell</title>
 

-<para>Template Haskell allows you to do compile-time meta-programming in Haskell.  There is a "home page" for
-Template Haskell at <ulink url="http://www.haskell.org/th/">
-http://www.haskell.org/th/</ulink>, while
-the background to
+<para>Template Haskell allows you to do compile-time meta-programming in
+Haskell.  
+The background to

 the main technical innovations is discussed in "<ulink
 url="http://research.microsoft.com/~simonpj/papers/meta-haskell">
 Template Meta-programming for Haskell</ulink>" (Proc Haskell Workshop 2002).
 the main technical innovations is discussed in "<ulink
 url="http://research.microsoft.com/~simonpj/papers/meta-haskell">
 Template Meta-programming for Haskell</ulink>" (Proc Haskell Workshop 2002).

-The details of the Template Haskell design are still in flux.  Make sure you
-consult the <ulink url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online library reference material</ulink> 
+</para>
+<para>
+There is a Wiki page about
+Template Haskell at <ulink url="http://haskell.org/haskellwiki/Template_Haskell">
+http://www.haskell.org/th/</ulink>, and that is the best place to look for
+further details.
+You may also 
+consult the <ulink
+url="http://www.haskell.org/ghc/docs/latest/html/libraries/index.html">online
+Haskell library reference material</ulink> 

 (search for the type ExpQ).
 [Temporary: many changes to the original design are described in 
       <ulink url="http://research.microsoft.com/~simonpj/tmp/notes2.ps">"http://research.microsoft.com/~simonpj/tmp/notes2.ps"</ulink>.
 (search for the type ExpQ).
 [Temporary: many changes to the original design are described in 
       <ulink url="http://research.microsoft.com/~simonpj/tmp/notes2.ps">"http://research.microsoft.com/~simonpj/tmp/notes2.ps"</ulink>.

-Not all of these changes are in GHC 6.2.]
+Not all of these changes are in GHC 6.6.]

 </para>
 
 <para> The first example from that paper is set out below as a worked example to help get you started. 
 </para>
 
 <para> The first example from that paper is set out below as a worked example to help get you started. 

@@ -5994,7 +6083,7 @@ r)
                    GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
 r) ->
               tpl2})
                    GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
 r) ->
               tpl2})

-        (%note "foo"
+        (%note "bar"

          eta);
 </programlisting>
 
          eta);
 </programlisting>
 

@@ -6096,9 +6185,6 @@ that it is well typed.
 <sect1 id="generic-classes">
 <title>Generic classes</title>
 
 <sect1 id="generic-classes">
 <title>Generic classes</title>
 

-    <para>(Note: support for generic classes is currently broken in
-    GHC 5.02).</para>
-

 <para>
 The ideas behind this extension are described in detail in "Derivable type classes",
 Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
 <para>
 The ideas behind this extension are described in detail in "Derivable type classes",
 Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.