X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=f8ad5c1b0ac8a79f9ee96c6a4227e6abafcaa6e7;hp=6b41b39057bbdd4cc4f3b81ebfbc72af919610d6;hb=9da4639011348fb6c318e3cba4b08622f811d9c4;hpb=3eeeb57d95c6a218ce457f85e1f5b3511057101f diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 6b41b39..f8ad5c1 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. - : - + ,: - Switch off the Haskell 98 monomorphism restriction. + These two flags control how generalisation is done. + See . + + + + + + + : + + + + 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 @@ -894,6 +905,38 @@ fromInteger :: Integer -> Bool -> Bool you should be all right. + + +Postfix operators + + +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 + + (e !) + +is equivalent (from the point of view of both type checking and execution) to the expression + + ((!) e) + +(for any expression e and operator (!). +The strict Haskell 98 interpretation is that the section is equivalent to + + (\y -> (!) e y) + +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. + +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.) + +The extension does not extend to the left-hand side of function +definitions; you must define such a function in prefix form. + + + @@ -2022,6 +2065,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 +2138,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. @@ -2178,8 +2226,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. @@ -2466,7 +2526,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 @@ -2626,6 +2686,11 @@ inner binding of ?x, so (f 9) will return + + Explicitly-kinded quantification @@ -3163,228 +3230,103 @@ for rank-2 types. - + +Impredicative polymorphism + +GHC supports impredicative polymorphism. This means +that you can call a polymorphic function at a polymorphic type, and +parameterise data structures over polymorphic types. For example: + + f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) + f (Just g) = Just (g [3], g "hello") + f Nothing = Nothing + +Notice here that the Maybe type is parameterised by the +polymorphic type (forall a. [a] -> +[a]). + +The technical details of this extension are described in the paper +Boxy types: +type inference for higher-rank types and impredicativity, +which appeared at ICFP 2006. + + -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 ys. +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 () +An expression type signature () +A pattern type signature () +Class and instance declarations () - - - - + - -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 @@ -3411,180 +3353,145 @@ 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, including the result part, can be used -in case expressions: + +Expression type signatures +An expression type signature that has explicit +quantification (using forall) brings into scope the +explicitly-quantified +type variables, in the annotated expression. For example: - case e of { ((x::a, y) :: (a,b)) -> x } + f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool ) - -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. - +Here, the type signature forall a. ST s Bool brings the +type variable s into scope, in the annotated expression +(op >>= \(x :: STRef s Int) -> g x). - + - + +Pattern type signatures -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::a) -> 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. + + + + +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 + + @@ -3751,16 +3658,19 @@ declaration (after expansion of any type synonyms) where - The type t is an arbitrary type + The ci are partial applications of + classes of the form C t1'...tj', where the arity of C + is exactly j+1. That is, C lacks exactly one type argument. - The vk+1...vn are type variables which do not occur in - t, and + The k is chosen so that ci (T v1...vk) is well-kinded. - The ci are partial applications of - classes of the form C t1'...tj', where the arity of C - is exactly j+1. That is, C lacks exactly one type argument. + The type t is an arbitrary type. + + + The type variables vk+1...vn do not occur in t, + nor in the ci, and None of the ci is Read, Show, @@ -3773,13 +3683,8 @@ where Then, for each ci, the derived instance declaration is: - instance ci (t vk+1...v) => ci (T v1...vp) + instance ci t => ci (T v1...vk) -where p is chosen so that T v1...vp is of the -right kind for the last parameter of class Ci. - - - As an example which does not work, consider newtype NonMonad m s = NonMonad (State s m s) deriving Monad @@ -3891,9 +3796,9 @@ pattern binding must have the same context. For example, this is fine: -Generalised Algebraic Data Types +Generalised Algebraic Data Types (GADTs) -Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you +Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you to give the type signatures of constructors explicitly. For example: data Term a where @@ -3914,9 +3819,20 @@ for these Terms: eval (If b e1 e2) = if eval b then eval e1 else eval e2 eval (Pair e1 e2) = (eval e1, eval e2) -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 +on the wiki, +and Ralf Hinze's +Fun with phantom types also has a number of examples. Note that papers +may use different notation to that implemented in GHC. - The extensions to GHC are these: + +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 Simple +unification-based type inference for GADTs, +which appeared in ICFP 2006. Data type declarations have a 'where' form, as exemplified above. The type signature of @@ -4008,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 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 @@ -4059,19 +3975,26 @@ the result type of the case expression. Hence the addition < Template Haskell -Template Haskell allows you to do compile-time meta-programming in Haskell. There is a "home page" for -Template Haskell at -http://www.haskell.org/th/, while -the background to +Template Haskell allows you to do compile-time meta-programming in +Haskell. +The background to the main technical innovations is discussed in " Template Meta-programming for Haskell" (Proc Haskell Workshop 2002). -The details of the Template Haskell design are still in flux. Make sure you -consult the online library reference material + + +There is a Wiki page about +Template Haskell at +http://www.haskell.org/th/, and that is the best place to look for +further details. +You may also +consult the online +Haskell library reference material (search for the type ExpQ). [Temporary: many changes to the original design are described in "http://research.microsoft.com/~simonpj/tmp/notes2.ps". -Not all of these changes are in GHC 6.2.] +Not all of these changes are in GHC 6.6.] The first example from that paper is set out below as a worked example to help get you started. @@ -4772,6 +4695,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. + + + + @@ -6016,7 +6083,7 @@ r) GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha r) -> tpl2}) - (%note "foo" + (%note "bar" eta); @@ -6072,7 +6139,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: @@ -6097,15 +6164,27 @@ 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. + + Generic classes - (Note: support for generic classes is currently broken in - GHC 5.02). - 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. @@ -6356,6 +6435,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. + + + +