X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=5d1b5cf5f053bf3a3435740f51ee0a7a1c88d3f0;hp=ca08f58d05f3e09d6b239bf953058625592e273a;hb=432b9c9322181a3644083e3c19b7e240d90659e7;hpb=27444c254fc33a4f72ad0aa78f561a0670567369
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index ca08f58..5d1b5cf 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -210,22 +210,20 @@ in a top-level binding.
in a recursive binding.
You may bind unboxed variables in a (non-recursive,
-non-top-level) pattern binding, but any such variable causes the entire
-pattern-match
-to become strict. For example:
+non-top-level) pattern binding, but you must make any such pattern-match
+strict. For example, rather than:
data Foo = Foo Int Int#
f x = let (Foo a b, w) = ..rhs.. in ..body..
-Since b has type Int#, the entire pattern
-match
-is strict, and the program behaves as if you had written
+you must write:
data Foo = Foo Int Int#
- f x = case ..rhs.. of { (Foo a b, w) -> ..body.. }
+ f x = let !(Foo a b, w) = ..rhs.. in ..body..
+since b has type Int#.
@@ -1008,6 +1006,7 @@ This name is not supported by GHC.
paper
Comprehensive comprehensions: comprehensions with "order by" and "group by",
except that the syntax we use differs slightly from the paper.
+The extension is enabled with the flag .Here is an example:
employees = [ ("Simon", "MS", 80)
@@ -2365,14 +2364,34 @@ In this example we give a single signature for T1 and
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:
+In particular, the type variable(s) in the "data T a where" header
+have no scope, and different constructors may have different universally-quantified type variables:
+
+ data T a where -- The 'a' has no scope
+ T1,T2 :: b -> T b -- Means forall b. b -> T b
+ T3 :: T a -- Means forall a. T a
+
+
+
+
+A constructor signature may mention type class constraints, which can differ for
+different constructors. For example, this is fine:
data T a where
- T1 :: Eq b => b -> T b
+ T1 :: Eq b => b -> b -> T b
T2 :: (Show c, Ix c) => c -> [c] -> T c
+When patten matching, these constraints are made available to discharge constraints
+in the body of the match. For example:
+
+ f :: T a -> String
+ f (T1 x y) | x==y = "yes"
+ | otherwise = "no"
+ f (T2 a b) = show a
+
+Note that f is not overloaded; the Eq constraint arising
+from the use of == is discharged by the pattern match on T1
+and similarly the Show constraint arising from the use of show.
@@ -2384,12 +2403,12 @@ have no scope. Indeed, one can write a kind signature instead:
or even a mixture of the two:
- data Foo a :: (* -> *) -> * where ...
+ data Bar a :: (* -> *) -> * where ...
The type variables (if given) may be explicitly kinded, so we could also write the header for Foo
like this:
- data Foo a (b :: * -> *) where ...
+ data Bar a (b :: * -> *) where ...
@@ -2420,27 +2439,48 @@ declaration. For example, these two declarations are equivalent
+The type signature may have quantified type variables that do not appear
+in the result type:
+
+ data Foo where
+ MkFoo :: a -> (a->Bool) -> Foo
+ Nil :: Foo
+
+Here the type variable a does not appear in the result type
+of either constructor.
+Although it is universally quantified in the type of the constructor, such
+a type variable is often called "existential".
+Indeed, the above declaration declares precisely the same type as
+the data Foo in .
+
+The type may contain a class context too, of course:
+
+ data Showable where
+ MkShowable :: Show a => a -> Showable
+
+
+
+
You can use record syntax on a GADT-style data type declaration:
data Person where
- Adult { name :: String, children :: [Person] } :: Person
- Child { name :: String } :: Person
+ Adult :: { name :: String, children :: [Person] } -> Person
+ Child :: Show a => { name :: !String, funny :: a } -> Person
As usual, for every constructor that has a field f, the type of
field f must be the same (modulo alpha conversion).
-
-
-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 example
-
- aPerson = Adult { name = "Fred", children = [] }
+The Child constructor above shows that the signature
+may have a context, existentially-quantified variables, and strictness annotations,
+just as in the non-record case. (NB: the "type" that follows the double-colon
+is not really a type, because of the record syntax and strictness annotations.
+A "type" of this form can appear only in a constructor signature.)
+
- shortName :: Person -> Bool
- hasChildren (Adult { children = kids }) = not (null kids)
- hasChildren (Child {}) = False
-
+
+Record updates are allowed with GADT-style declarations,
+only fields that have the following property: the type of the field
+mentions no existential type variables.