X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=5339c4323f710fd7589811526e4324c480fe3be3;hb=c949e1a9af96cd5241d8cfc74fe3c622258edd7e;hp=3801f966f3493927d86a437b5fea7bf0d113d224;hpb=09c814ec2c4fa854165f98aff4d29a69cafdc92a;p=ghc-hetmet.git diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 3801f96..5339c43 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -116,11 +116,22 @@ documentation describes all the libraries that come with GHC. - : - + ,: + + + These two flags control how generalisation is done. + See . + + + + + + + : + - Switch off the Haskell 98 monomorphism restriction. + Use GHCi's extended default rules in a regular module (). Independent of the flag. @@ -140,7 +151,7 @@ documentation describes all the libraries that come with GHC. - + @@ -617,7 +628,7 @@ clunky env var1 var1 = case lookup env var1 of Nothing -> fail Just val2 -> val1 + val2 where - fail = val1 + val2 + fail = var1 + var2 @@ -2022,6 +2033,11 @@ something more specific does not: op = ... -- Default +You can find lots of background material about the reason for these +restrictions in the paper +Understanding functional dependencies via Constraint Handling Rules. + @@ -2090,7 +2106,7 @@ option, you can use arbitrary types in both an instance context and instance head. 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 N. +with N. @@ -2107,7 +2123,9 @@ can be modified by two flags: and -fallow-incoherent-instances -, as this section discusses. +, as this section discusses. Both these +flags are dynamic flags, and can be set on a per-module basis, using +an OPTIONS_GHC pragma if desired (). When GHC tries to resolve, say, the constraint C Int Bool, it tries to match every instance declaration against the @@ -2176,8 +2194,20 @@ some other constraint. But if the instance declaration was compiled with check for that declaration. -All this makes it possible for a library author to design a library that relies on -overlapping instances without the library client having to know. +These rules make it possible for a library author to design a library that relies on +overlapping instances without the library client having to know. + + +If an instance declaration is compiled without +, +then that instance can never be overlapped. This could perhaps be +inconvenient. Perhaps the rule should instead say that the +overlapping instance declaration should be compiled in +this way, rather than the overlapped one. Perhaps overlap +at a usage site should be permitted regardless of how the instance declarations +are compiled, if the flag is +used at the usage site. (Mind you, the exact usage site can occasionally be +hard to pin down.) We are interested to receive feedback on these points. The flag implies the flag, but not vice versa. @@ -2464,7 +2494,7 @@ function that called it. For example, our sort function might to pick out the least value in a list: least :: (?cmp :: a -> a -> Bool) => [a] -> a - least xs = fst (sort xs) + least xs = head (sort xs) Without lifting a finger, the ?cmp parameter is propagated to become a parameter of least as well. With explicit @@ -2624,6 +2654,11 @@ inner binding of ?x, so (f 9) will return + + Explicitly-kinded quantification @@ -3164,225 +3201,81 @@ for rank-2 types. -Scoped type variables +<title>Lexically scoped type variables -A lexically scoped type variable can be bound by: - -A declaration type signature () -A pattern type signature () -A result type signature () - -For example: +GHC supports lexically scoped type variables, without +which some type signatures are simply impossible to write. For example: -f (xs::[a]) = ys ++ ys - where - ys :: [a] - ys = reverse xs +f :: forall a. [a] -> [a] +f xs = ys ++ ys + where + ys :: [a] + ys = reverse xs -The pattern (xs::[a]) includes a type signature for xs. -This brings the type variable a into scope; it scopes over -all the patterns and right hand sides for this equation for f. -In particular, it is in scope at the type signature for y. - - - -At ordinary type signatures, such as that for ys, any type variables -mentioned in the type signature that are not in scope are -implicitly universally quantified. (If there are no type variables in -scope, all type variables mentioned in the signature are universally -quantified, which is just as in Haskell 98.) In this case, since a -is in scope, it is not universally quantified, so the type of ys is -the same as that of xs. In Haskell 98 it is not possible to declare +The type signature for f brings the type variable a into scope; it scopes over +the entire definition of f. +In particular, it is in scope at the type signature for y. +In Haskell 98 it is not possible to declare a type for ys; a major benefit of scoped type variables is that it becomes possible to do so. - - -Scoped type variables are implemented in both GHC and Hugs. Where the -implementations differ from the specification below, those differences -are noted. - - - -So much for the basic idea. Here are the details. +Lexically-scoped type variables are enabled by +. +Note: GHC 6.6 contains substantial changes to the way that scoped type +variables work, compared to earlier releases. Read this section +carefully! -What a scoped type variable means - -A lexically-scoped type variable is simply -the name for a type. The restriction it expresses is that all occurrences -of the same name mean the same type. For example: - - f :: [Int] -> Int -> Int - f (xs::[a]) (y::a) = (head xs + y) :: a - -The pattern type signatures on the left hand side of -f express the fact that xs -must be a list of things of some type a; and that y -must have this same type. The type signature on the expression (head xs) -specifies that this expression must have the same type a. -There is no requirement that the type named by "a" is -in fact a type variable. Indeed, in this case, the type named by "a" is -Int. (This is a slight liberalisation from the original rather complex -rules, which specified that a pattern-bound type variable should be universally quantified.) -For example, all of these are legal: - - - t (x::a) (y::a) = x+y*2 - - f (x::a) (y::b) = [x,y] -- a unifies with b - - g (x::a) = x + 1::Int -- a unifies with Int - - h x = let k (y::a) = [x,y] -- a is free in the - in k x -- environment - - k (x::a) True = ... -- a unifies with Int - k (x::Int) False = ... - - w :: [b] -> [b] - w (x::a) = x -- a unifies with [b] - - - - - -Scope and implicit quantification - - +Overview +The design follows the following principles - - - -All the type variables mentioned in a pattern, -that are not already in scope, -are brought into scope by the pattern. We describe this set as -the type variables bound by the pattern. -For example: - - f (x::a) = let g (y::(a,b)) = fst y - in - g (x,True) - -The pattern (x::a) brings the type variable -a into scope, as well as the term -variable x. The pattern (y::(a,b)) -contains an occurrence of the already-in-scope type variable a, -and brings into scope the type variable b. - - - - - -The type variable(s) bound by the pattern have the same scope -as the term variable(s) bound by the pattern. For example: - - let - f (x::a) = <...rhs of f...> - (p::b, q::b) = (1,2) - in <...body of let...> - -Here, the type variable a scopes over the right hand side of f, -just like x does; while the type variable b scopes over the -body of the let, and all the other definitions in the let, -just like p and q do. -Indeed, the newly bound type variables also scope over any ordinary, separate -type signatures in the let group. - - - - - - -The type variables bound by the pattern may be -mentioned in ordinary type signatures or pattern -type signatures anywhere within their scope. - - - - - - - In ordinary type signatures, any type variable mentioned in the -signature that is in scope is not universally quantified. - - - - - - - - Ordinary type signatures do not bring any new type variables -into scope (except in the type signature itself!). So this is illegal: - - - f :: a -> a - f x = x::a - - -It's illegal because a is not in scope in the body of f, -so the ordinary signature x::a is equivalent to x::forall a.a; -and that is an incorrect typing. - +A scoped type variable stands for a type variable, and not for +a type. (This is a change from GHC's earlier +design.) +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 +rigid type; that is, the type is fully known to the type +checker, and no inference is involved. +Lexical type variables may be alpha-renamed freely, without +changing the program. + - - - -The pattern type signature is a monotype: - - +A lexically scoped type variable can be bound by: - -A pattern type signature cannot contain any explicit forall quantification. - - - -The type variables bound by a pattern type signature can only be instantiated to monotypes, -not to type schemes. - - - -There is no implicit universal quantification on pattern type signatures (in contrast to -ordinary type signatures). - - +A declaration type signature () +A pattern type signature () +Class and instance declarations () - - - - +In addition, GHC supports result type signatures (), although they never bind type variables. + - -The type variables in the head of a class or instance declaration -scope over the methods defined in the where part. For example: - - +In Haskell, a programmer-written type signature is implicitly quantifed over +its free type variables (Section +4.1.2 +of the Haskel Report). +Lexically scoped type variables affect this implicit quantification rules +as follows: any type variable that is in scope is not universally +quantified. For example, if type variable a is in scope, +then - class C a where - op :: [a] -> a - - op xs = let ys::[a] - ys = reverse xs - in - head ys + (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) - - -(Not implemented in Hugs yet, Dec 98). - - - - + Declaration type signatures A declaration type signature that has explicit @@ -3410,179 +3303,122 @@ quantification rules. -Where a pattern type signature can occur - - -A pattern type signature can occur in any pattern. For example: - - - - -A pattern type signature can be on an arbitrary sub-pattern, not -just on a variable: - - - - f ((x,y)::(a,b)) = (y,x) :: (b,a) - - - - - - - - - Pattern type signatures, including the result part, can be used -in lambda abstractions: - - - (\ (x::a, y) :: a -> x) - - - - - +Pattern type signatures - Pattern type signatures, including the result part, can be used -in case expressions: - - - case e of { ((x::a, y) :: (a,b)) -> x } - - -Note that the -> symbol in a case alternative -leads to difficulties when parsing a type signature in the pattern: in -the absence of the extra parentheses in the example above, the parser -would try to interpret the -> as a function -arrow and give a parse error later. - - - - - - - -To avoid ambiguity, the type after the “::” in a result -pattern signature on a lambda or case must be atomic (i.e. a single -token or a parenthesised type of some sort). To see why, -consider how one would parse this: - - +A type signature may occur in any pattern; this is a pattern type +signature. +For example: - \ x :: a -> b -> x + -- f and g assume that 'a' is already in scope + f = \(x::Int, y) -> x + g (x::a) = x + h ((x,y) :: (Int,Bool)) = (y,x) - - +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. - - - - - Pattern type signatures can bind existential type variables. -For example: - - +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: data T = forall a. MkT [a] - f :: T -> T - f (MkT [t::a]) = MkT t3 + k :: T -> T + k (MkT [t::a]) = MkT t3 where t3::[a] = [t,t,t] - - +Here, the pattern type signature (t::a) 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. - - - - - -Pattern type signatures -can be used in pattern bindings: - - - f x = let (y, z::a) = x in ... - f1 x = let (y, z::Int) = x in ... - f2 (x::(Int,a)) = let (y, z::a) = x in ... - f3 :: (b->b) = \x -> x - - -In all such cases, the binding is not generalised over the pattern-bound -type variables. Thus f3 is monomorphic; f3 -has type b -> b for some type b, -and not forall b. b -> b. -In contrast, the binding - - f4 :: b->b - f4 = \x -> x - -makes a polymorphic function, but b is not in scope anywhere -in f4's scope. - +If this seems a little odd, we think so too. But we must have +some way to bring such type variables into scope, else we +could not name existentially-bound type variables in subequent type signatures. - - + +This is (now) the only situation in which a pattern type +signature is allowed to mention a lexical variable that is not already in +scope. +For example, both f and g would be +illegal if a was not already in scope. -Pattern type signatures are completely orthogonal to ordinary, separate -type signatures. The two can be used independently or together. - + Result type signatures -The result type of a function can be given a signature, thus: - +The result type of a function, lambda, or case expression alternative can be given a signature, thus: - f (x::a) :: [a] = [x,x,x] - - + -- f assumes that 'a' is already in scope + f x y :: [a] = [x,y,x] -The final :: [a] after all the patterns gives a signature to the -result type. Sometimes this is the only way of naming the type variable -you want: + g = \ x :: [Int] -> [3,4] - - - f :: Int -> [a] -> [a] - f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x) - in \xs -> map g (reverse xs `zip` xs) + h :: forall a. [a] -> a + h xs = case xs of + (y:ys) :: a -> y - +The final :: [a] after the patterns of f gives the type of +the result of the function. Similarly, the body of the lambda in the RHS of +g is [Int], and the RHS of the case +alternative in h is a. + A result type signature never brings new type variables into scope. -The type variables bound in a result type signature scope over the right hand side -of the definition. However, consider this corner-case: +There are a couple of syntactic wrinkles. First, notice that all three +examples would parse quite differently with parentheses: - rev1 :: [a] -> [a] = \xs -> reverse xs + -- f assumes that 'a' is already in scope + f x (y :: [a]) = [x,y,x] - foo ys = rev (ys::[a]) + g = \ (x :: [Int]) -> [3,4] + + h :: forall a. [a] -> a + h xs = case xs of + ((y:ys) :: a) -> y -The signature on rev1 is considered a pattern type signature, not a result -type signature, and the type variables it binds have the same scope as rev1 -itself (i.e. the right-hand side of rev1 and the rest of the module too). -In particular, the expression (ys::[a]) is OK, because the type variable a -is in scope (otherwise it would mean (ys::forall a.[a]), which would be rejected). - - -As mentioned above, rev1 is made monomorphic by this scoping rule. -For example, the following program would be rejected, because it claims that rev1 -is polymorphic: +Now the signature is on the pattern; and +h would certainly be ill-typed (since the pattern +(y:ys) cannot have the type a. + +Second, to avoid ambiguity, the type after the “::” in a result +pattern signature on a lambda or case must be atomic (i.e. a single +token or a parenthesised type of some sort). To see why, +consider how one would parse this: - rev1 :: [b] -> [b] - rev1 :: [a] -> [a] = \xs -> reverse xs + \ x :: a -> b -> x + + +Class and instance declarations -Result type signatures are not yet implemented in Hugs. - +The type variables in the head of a class or instance declaration +scope over the methods defined in the where part. For example: + + + + class C a where + op :: [a] -> a + + op xs = let ys::[a] + ys = reverse xs + in + head ys + + @@ -4770,6 +4606,150 @@ Because the preprocessor targets Haskell (rather than Core), + + + +Bang patterns +<indexterm><primary>Bang patterns</primary></indexterm> + +GHC supports an extension of pattern matching called bang +patterns. Bang patterns are under consideration for Haskell Prime. +The Haskell +prime feature description contains more discussion and examples +than the material below. + + +Bang patterns are enabled by the flag . + + + +Informal description of bang patterns + + +The main idea is to add a single new production to the syntax of patterns: + + pat ::= !pat + +Matching an expression e against a pattern !p is done by first +evaluating e (to WHNF) and then matching the result against p. +Example: + +f1 !x = True + +This definition makes f1 is strict in x, +whereas without the bang it would be lazy. +Bang patterns can be nested of course: + +f2 (!x, y) = [x,y] + +Here, f2 is strict in x but not in +y. +A bang only really has an effect if it precedes a variable or wild-card pattern: + +f3 !(x,y) = [x,y] +f4 (x,y) = [x,y] + +Here, f3 and f4 are identical; putting a bang before a pattern that +forces evaluation anyway does nothing. + +Bang patterns work in case expressions too, of course: + +g5 x = let y = f x in body +g6 x = case f x of { y -> body } +g7 x = case f x of { !y -> body } + +The functions g5 and g6 mean exactly the same thing. +But g7 evalutes (f x), binds y to the +result, and then evaluates body. + +Bang patterns work in let and where +definitions too. For example: + +let ![x,y] = e in b + +is a strict pattern: operationally, it evaluates e, matches +it against the pattern [x,y], and then evaluates b +The "!" should not be regarded as part of the pattern; after all, +in a function argument ![x,y] means the +same as [x,y]. Rather, the "!" +is part of the syntax of let bindings. + + + + + +Syntax and semantics + + + +We add a single new production to the syntax of patterns: + + pat ::= !pat + +There is one problem with syntactic ambiguity. Consider: + +f !x = 3 + +Is this a definition of the infix function "(!)", +or of the "f" with a bang pattern? GHC resolves this +ambiguity inf favour of the latter. If you want to define +(!) with bang-patterns enabled, you have to do so using +prefix notation: + +(!) f x = 3 + +The semantics of Haskell pattern matching is described in +Section 3.17.2 of the Haskell Report. To this description add +one extra item 10, saying: +Matching +the pattern !pat against a value v behaves as follows: +if v is bottom, the match diverges + otherwise, pat is matched against + v + + +Similarly, in Figure 4 of +Section 3.17.3, add a new case (t): + +case v of { !pat -> e; _ -> e' } + = v `seq` case v of { pat -> e; _ -> e' } + + +That leaves let expressions, whose translation is given in +Section +3.12 +of the Haskell Report. +In the translation box, first apply +the following transformation: for each pattern pi that is of +form !qi = ei, transform it to (xi,!qi) = ((),ei), and and replace e0 +by (xi `seq` e0). Then, when none of the left-hand-side patterns +have a bang at the top, apply the rules in the existing box. + +The effect of the let rule is to force complete matching of the pattern +qi before evaluation of the body is begun. The bang is +retained in the translated form in case qi is a variable, +thus: + + let !y = f x in b + + + + +The let-binding can be recursive. However, it is much more common for +the let-binding to be non-recursive, in which case the following law holds: +(let !p = rhs in body) + is equivalent to +(case rhs of !p -> body) + + +A pattern with a bang at the outermost level is not allowed at the top level of +a module. + + + + @@ -6070,7 +6050,7 @@ shortcoming is something that could be fixed, with some kind of pragma.) - The <literal>inline</literal> function + The <literal>lazy</literal> function The lazy function restrains strictness analysis a little: @@ -6095,6 +6075,21 @@ look strict in y which would defeat the whole purpose of par. + + The <literal>unsafeCoerce#</literal> function + +The function unsafeCoerce# allows you to side-step the +typechecker entirely. It has type + + unsafeCoerce# :: a -> b + +That is, it allows you to coerce any type into any other type. If you use this +function, you had better get it right, otherwise segmentation faults await. +It is generally used when you want to write a program that you know is +well-typed, but where Haskell's type system is not expressive enough to prove +that it is well typed. + + @@ -6354,6 +6349,51 @@ Just to finish with, here's another example I rather like: + +Control over monomorphism + +GHC supports two flags that control the way in which generalisation is +carried out at let and where bindings. + + + +Switching off the dreaded Monomorphism Restriction + + +Haskell's monomorphism restriction (see +Section +4.5.5 +of the Haskell Report) +can be completely switched off by +. + + + + +Monomorphic pattern bindings + + + + As an experimental change, we are exploring the possibility of + making pattern bindings monomorphic; that is, not generalised at all. + A pattern binding is a binding whose LHS has no function arguments, + and is not a simple variable. For example: + + f x = x -- Not a pattern binding + f = \x -> x -- Not a pattern binding + f :: Int -> Int = \x -> x -- Not a pattern binding + + (g,h) = e -- A pattern binding + (f) = e -- A pattern binding + [x] = e -- A pattern binding + +Experimentally, GHC now makes pattern bindings monomorphic by +default. Use to recover the +standard behaviour. + + + +