Documentation for class contexts in data-constructor declarations
authorsimonpj@microsoft.com <unknown>
Fri, 22 Dec 2006 09:34:31 +0000 (09:34 +0000)
committersimonpj@microsoft.com <unknown>
Fri, 22 Dec 2006 09:34:31 +0000 (09:34 +0000)
docs/users_guide/glasgow_exts.xml

index b2daa16..6f54d1e 100644 (file)
@@ -1309,7 +1309,7 @@ universal quantification earlier.
 
 </sect4>
 
 
 </sect4>
 
-<sect4>
+<sect4 id="existential-records">
 <title>Record Constructors</title>
 
 <para>
 <title>Record Constructors</title>
 
 <para>
@@ -1361,20 +1361,6 @@ main = do
     display (inc (inc counterB))   -- prints "##"
 </programlisting>
 
     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:
 
 At the moment, record update syntax is only supported for Haskell 98 data types,
 so the following function does <emphasis>not</emphasis> work:
 
@@ -1515,7 +1501,7 @@ are convincing reasons to change it.
  You can't use <literal>deriving</literal> to define instances of a
 data type with existentially quantified data constructors.
 
  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:&num;
+Reason: in most cases it would not make sense. For example:;
 
 <programlisting>
 data T = forall a. MkT [a] deriving( Eq )
 
 <programlisting>
 data T = forall a. MkT [a] deriving( Eq )
@@ -1543,6 +1529,315 @@ declarations.  Define your own instances!
 </sect4>
 </sect3>
 
 </sect4>
 </sect3>
 
+<!-- ====================== Generalised algebraic data types =======================  -->
+
+<sect3 id="gadt-style">
+<title>Declaring data types with explicit constructor signatures</title>
+
+<para>GHC allows you to declare an algebraic data type by 
+giving the type signatures of constructors explicitly.  For example:
+<programlisting>
+  data Maybe a where
+      Nothing :: Maybe a
+      Just    :: a -> Maybe a
+</programlisting>
+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>
+  data Foo = forall a. MkFoo a (a -> Bool)
+  data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
+</programlisting>
+</para>
+<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>
+  data Set a where
+    MkSet :: Eq a => [a] -> Set a
+
+  makeSet :: Eq a => [a] -> Set a
+  makeSet xs = MkSet (nub xs)
+
+  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>
+<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>
+  data Eq a => Set' a = MkSet' [a]
+</programlisting>
+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>
+For example, a possible application of GHC's behaviour is to reify dictionaries:
+<programlisting>
+   data NumInst a where
+     MkNumInst :: Num a => NumInst a
+
+   intInst :: NumInst Int
+   intInst = MkNumInst
+
+   plus :: NumInst a -> a -> a -> a
+   plus MkNumInst p q = p + q
+</programlisting>
+Here, a value of type <literal>NumInst a</literal> is equivalent 
+to an explicit <literal>(Num a)</literal> dictionary.
+</para>
+
+<para>
+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>
+  data T a where
+    T1 :: Eq b => b -> T b
+    T2 :: (Show c, Ix c) => c -> [c] -> T c
+</programlisting>
+</para></listitem>
+
+<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>
+  data Set :: * -> * 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>
+You can use strictness annotations, in the obvious places
+in the constructor type:
+<programlisting>
+  data Term a where
+      Lit    :: !Int -> Term Int
+      If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
+      Pair   :: Term a -> Term b -> Term (a,b)
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can use a <literal>deriving</literal> clause on a GADT-style data type
+declaration.   For example, these two declarations are equivalent
+<programlisting>
+  data Maybe1 a where {
+      Nothing1 :: Maybe1 a ;
+      Just1    :: a -> Maybe1 a
+    } deriving( Eq, Ord )
+
+  data Maybe2 a = Nothing2 | Just2 a 
+       deriving( Eq, Ord )
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can use record syntax on a GADT-style data type declaration:
+
+<programlisting>
+  data Person where
+      Adult { name :: String, children :: [Person] } :: Person
+      Child { name :: String } :: Person
+</programlisting>
+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>
+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>
+  aPerson = Adult { name = "Fred", children = [] }
+
+  shortName :: Person -> Bool
+  hasChildren (Adult { children = kids }) = not (null kids)
+  hasChildren (Child {})                  = False
+</programlisting>
+</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>
+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>
+</sect3>
+
+<sect3 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>
+
+</sect3>
+
+<!-- ====================== End of Generalised algebraic data types =======================  -->
+
+
 </sect2>
 
 
 </sect2>
 
 
@@ -3818,183 +4113,6 @@ pattern binding must have the same context.  For example, this is fine:
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
   
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
   
-<!-- ====================== Generalised algebraic data types =======================  -->
-
-<sect1 id="gadt">
-<title>Generalised Algebraic Data Types (GADTs)</title>
-
-<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
-      Lit    :: Int -> Term Int
-      Succ   :: Term Int -> Term Int
-      IsZero :: Term Int -> Term Bool  
-      If     :: Term Bool -> Term a -> Term a -> Term a
-      Pair   :: Term a -> Term b -> Term (a,b)
-</programlisting>
-Notice that the return type of the constructors is not always <literal>Term a</literal>, as is the
-case with ordinary vanilla data types.  Now we can write a well-typed <literal>eval</literal> function
-for these <literal>Terms</literal>:
-<programlisting>
-  eval :: Term a -> a
-  eval (Lit i)             = i
-  eval (Succ t)     = 1 + eval t
-  eval (IsZero 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>
-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. 
-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
-each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal
-Haskell data type declaration, the type variable(s) in the "<literal>data Term a where</literal>" header 
-have no scope.  Indeed, one can write a kind signature instead:
-<programlisting>
-  data Term :: * -> * where ...
-</programlisting>
-or even a mixture of the two:
-<programlisting>
-  data Foo a :: (* -> *) -> * where ...
-</programlisting>
-The type variables (if given) may be explicitly kinded, so we could also write the header for <literal>Foo</literal>
-like this:
-<programlisting>
-  data Foo a (b :: * -> *) where ...
-</programlisting>
-</para></listitem>
-
-<listitem><para>
-There are no restrictions on the type of the data constructor, except that the result
-type must begin with the type constructor being defined.  For example, in the <literal>Term</literal> data
-type above, the type of each constructor must end with <literal> ... -> Term ...</literal>.
-</para></listitem>
-
-<listitem><para>
-You can use record syntax on a GADT-style data type declaration:
-
-<programlisting>
-  data Term a where
-      Lit    { val  :: Int }      :: Term Int
-      Succ   { num  :: Term Int } :: Term Int
-      Pred   { num  :: Term Int } :: Term Int
-      IsZero { arg  :: Term Int } :: Term Bool 
-      Pair   { arg1 :: Term a
-             , arg2 :: Term b
-             }                    :: Term (a,b)
-      If     { cnd  :: Term Bool
-             , tru  :: Term a
-             , fls  :: Term a
-             }                    :: Term a
-</programlisting>
-For every constructor that has a field <literal>f</literal>, (a) the type of
-field <literal>f</literal> must be the same; and (b) the
-result type of the constructor must be the same; both modulo alpha conversion.
-Hence, in our example, we cannot merge the <literal>num</literal> and <literal>arg</literal>
-fields above into a 
-single name.  Although their field types are both <literal>Term Int</literal>,
-their selector functions actually have different types:
-
-<programlisting>
-  num :: Term Int -> Term Int
-  arg :: Term Bool -> Term Int
-</programlisting>
-
-At the moment, record updates are not yet possible with GADT, so support is 
-limited to record construction, selection and pattern matching:
-
-<programlisting>
-  someTerm :: Term Bool
-  someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } }
-
-  eval :: Term a -> a
-  eval Lit    { val = i } = i
-  eval Succ   { num = t } = eval t + 1
-  eval Pred   { num = t } = eval t - 1
-  eval IsZero { arg = t } = eval t == 0
-  eval Pair   { arg1 = t1, arg2 = t2 } = (eval t1, eval t2)
-  eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t)
-</programlisting>
-
-</para></listitem>
-
-<listitem><para>
-You can use strictness annotations, in the obvious places
-in the constructor type:
-<programlisting>
-  data Term a where
-      Lit    :: !Int -> Term Int
-      If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
-      Pair   :: Term a -> Term b -> Term (a,b)
-</programlisting>
-</para></listitem>
-
-<listitem><para>
-You can use a <literal>deriving</literal> clause on a GADT-style data type
-declaration, but only if the data type could also have been declared in
-Haskell-98 syntax.   For example, these two declarations are equivalent
-<programlisting>
-  data Maybe1 a where {
-      Nothing1 :: Maybe1 a ;
-      Just1    :: a -> Maybe1 a
-    } deriving( Eq, Ord )
-
-  data Maybe2 a = Nothing2 | Just2 a 
-       deriving( Eq, Ord )
-</programlisting>
-This simply allows you to declare a vanilla Haskell-98 data type using the
-<literal>where</literal> form without losing the <literal>deriving</literal> clause.
-</para></listitem>
-
-<listitem><para>
-Pattern matching causes type refinement.  For example, in the right hand side of the equation
-<programlisting>
-  eval :: Term a -> a
-  eval (Lit i) =  ...
-</programlisting>
-the type <literal>a</literal> is refined to <literal>Int</literal>.  (That's the whole point!)
-A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper
-about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page.</para>
-
-<para> The general principle is this: <emphasis>type refinement is only carried out based on user-supplied type annotations</emphasis>.
-So if no type signature is supplied for <literal>eval</literal>, no type refinement happens, and lots of obscure error messages will
-occur.  However, the refinement is quite general.  For example, if we had:
-<programlisting>
-  eval :: Term a -> a -> a
-  eval (Lit i) j =  i+j
-</programlisting>
-the pattern match causes the type <literal>a</literal> to be refined to <literal>Int</literal> (because of the type
-of the constructor <literal>Lit</literal>, and that refinement also applies to the type of <literal>j</literal>, and
-the result type of the <literal>case</literal> expression.  Hence the addition <literal>i+j</literal> is legal.
-</para>
-</listitem>
-</itemizedlist>
-</para>
-
-<para>Notice that GADTs generalise existential types.  For example, these two declarations are equivalent:
-<programlisting>
-  data T a = forall b. MkT b (b->a)
-  data T' a where { MKT :: b -> (b->a) -> T' a }
-</programlisting>
-</para>
-</sect1>
-
-<!-- ====================== End of Generalised algebraic data types =======================  -->
-
 <!-- ====================== TEMPLATE HASKELL =======================  -->
 
 <sect1 id="template-haskell">
 <!-- ====================== TEMPLATE HASKELL =======================  -->
 
 <sect1 id="template-haskell">