X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fdocs%2Fusers_guide%2Fglasgow_exts.sgml;h=d4a39bef56ca1f188bd3d36657347524cc4f8855;hb=7b398a32ad0e56d07bbf1feb653e3eda123dc9b2;hp=5c1483c470ff646cf223aca87f0ad3257e44205f;hpb=eedbfe545e6e1e8a345c67ecc31844f71aabf12d;p=ghc-hetmet.git diff --git a/ghc/docs/users_guide/glasgow_exts.sgml b/ghc/docs/users_guide/glasgow_exts.sgml index 5c1483c..d4a39be 100644 --- a/ghc/docs/users_guide/glasgow_exts.sgml +++ b/ghc/docs/users_guide/glasgow_exts.sgml @@ -16,150 +16,15 @@ performance because of the implementation costs of Haskell's -Executive summary of our extensions: - - - - - - Unboxed types and primitive operations: - - You can get right down to the raw machine types and - operations; included in this are “primitive - arrays” (direct access to Big Wads of Bytes). Please - see and following. - - - - - Type system extensions: - - GHC supports a large number of extensions to Haskell's - type system. Specifically: - - - - Multi-parameter type classes: - - - - - - - Functional dependencies: - - - - - - - Implicit parameters: - - - - - - - Local universal quantification: - - - - - - - Extistentially quantification in data types: - - - - - - - Scoped type variables: - - Scoped type variables enable the programmer to - supply type signatures for some nested declarations, - where this would not be legal in Haskell 98. Details in - . - - - - - - - - Pattern guards - - Instead of being a boolean expression, a guard is a list - of qualifiers, exactly as in a list comprehension. See . - - - - - Data types with no constructors - - See . - - - - - Parallel list comprehensions - - An extension to the list comprehension syntax to support - zipWith-like functionality. See . - - - - - Foreign calling: - - Just what it sounds like. We provide - lots of rope that you can dangle around - your neck. Please see . - - - - - Pragmas - - Pragmas are special instructions to the compiler placed - in the source file. The pragmas GHC supports are described in - . - - - - - Rewrite rules: - - The programmer can specify rewrite rules as part of the - source program (in a pragma). GHC applies these rewrite rules - wherever it can. Details in . - - - - - Generic classes: - - Generic class declarations allow you to define a class - whose methods say how to work over an arbitrary data type. - Then it's really easy to make any new type into an instance of - the class. This generalises the rather ad-hoc "deriving" - feature of Haskell 98. Details in . - - - - - Before you get too carried away working at the lowest level (e.g., sloshing MutableByteArray#s around your program), you may wish to check if there are libraries that provide a -“Haskellised veneer” over the features you want. See -. +“Haskellised veneer” over the features you want. The +separate libraries documentation describes all the libraries that come +with GHC. + Language options @@ -188,6 +53,30 @@ program), you may wish to check if there are libraries that provide a + and : + + + + This option enables the language extension defined in the + Haskell 98 Foreign Function Interface Addendum plus deprecated + syntax of previous versions of the FFI for backwards + compatibility. + + + + + : + + + This option enables the deprecated with + keyword for implicit parameters; it is merely provided for backwards + compatibility. + It is independent of the + flag. + + + + : @@ -200,6 +89,7 @@ program), you may wish to check if there are libraries that provide a + @@ -241,7 +131,7 @@ program), you may wish to check if there are libraries that provide a module namespace is flat, and you must not conflict with any Prelude module.) - Even though you have not imported the Prelude, all + Even though you have not imported the Prelude, most of the built-in syntax still refers to the built-in Haskell Prelude types and values, as specified by the Haskell Report. For example, the type [Int] @@ -250,51 +140,9 @@ program), you may wish to check if there are libraries that provide a translation for list comprehensions continues to use Prelude.map etc. - With one group of exceptions! You may want to - define your own numeric class hierarchy. It completely - defeats that purpose if the literal "1" means - "Prelude.fromInteger 1", which is what - the Haskell Report specifies. So the - flag causes the - following pieces of built-in syntax to refer to whatever - is in scope, not the Prelude versions: - - - - Integer and fractional literals mean - "fromInteger 1" and - "fromRational 3.2", not the - Prelude-qualified versions; both in expressions and in - patterns. - - - - Negation (e.g. "- (f x)") - means "negate (f x)" (not - Prelude.negate). - - - - In an n+k pattern, the standard Prelude - Ord class is still used for comparison, - but the necessary subtraction uses whatever - "(-)" is in scope (not - "Prelude.(-)"). - - - - Note: Negative literals, such as -3, are - specified by (a careful reading of) the Haskell Report as - meaning Prelude.negate (Prelude.fromInteger 3). - However, GHC deviates from this slightly, and treats them as meaning - fromInteger (-3). One particular effect of this - slightly-non-standard reading is that there is no difficulty with - the literal -2147483648 at type Int; - it means fromInteger (-2147483648). The strict interpretation - would be negate (fromInteger 2147483648), - and the call to fromInteger would overflow - (at type Int, remember). - + However, does + change the handling of certain built-in syntax: see + . @@ -303,1397 +151,1819 @@ program), you may wish to check if there are libraries that provide a + &primitives; - -Primitive state-transformer monad - -state transformers (Glasgow extensions) -ST monad (Glasgow extension) - + + +Type system extensions - -This monad underlies our implementation of arrays, mutable and -immutable, and our implementation of I/O, including “C calls”. - + +Data types with no constructors - -The ST library, which provides access to the -ST monad, is described in . - +With the flag, GHC lets you declare +a data type with no constructors. For example: - + + data S -- S :: * + data T a -- T :: * -> * + - -Primitive arrays, mutable and otherwise - +Syntactically, the declaration lacks the "= constrs" part. The +type can be parameterised over types of any kind, but if the kind is +not * then an explicit kind annotation must be used +(see ). + +Such data types have only one value, namely bottom. +Nevertheless, they can be useful when defining "phantom types". + + + +Infix type constructors -primitive arrays (Glasgow extension) -arrays, primitive (Glasgow extension) +GHC allows type constructors to be operators, and to be written infix, very much +like expressions. More specifically: + + + A type constructor can be an operator, beginning with a colon; e.g. :*:. + The lexical syntax is the same as that for data constructors. + + + Types can be written infix. For example Int :*: Bool. + + + Back-quotes work + as for expressions, both for type constructors and type variables; e.g. Int `Either` Bool, or + Int `a` Bool. Similarly, parentheses work the same; e.g. (:*:) Int Bool. + + + Fixities may be declared for type constructors just as for data constructors. However, + one cannot distinguish between the two in a fixity declaration; a fixity declaration + sets the fixity for a data constructor and the corresponding type constructor. For example: + + infixl 7 T, :*: + + sets the fixity for both type constructor T and data constructor T, + and similarly for :*:. + Int `a` Bool. + + + Function arrow is infixr with fixity 0. (This might change; I'm not sure what it should be.) + + + Data type and type-synonym declarations can be written infix. E.g. + + data a :*: b = Foo a b + type a :+: b = Either a b + + + + The only thing that differs between operators in types and operators in expressions is that + ordinary non-constructor operators, such as + and * + are not allowed in types. Reason: the uniform thing to do would be to make them type + variables, but that's not very useful. A less uniform but more useful thing would be to + allow them to be type constructors. But that gives trouble in export + lists. So for now we just exclude them. + + + + + + +Explicitly-kinded quantification -GHC knows about quite a few flavours of Large Swathes of Bytes. +Haskell infers the kind of each type variable. Sometimes it is nice to be able +to give the kind explicitly as (machine-checked) documentation, +just as it is nice to give a type signature for a function. On some occasions, +it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999) +John Hughes had to define the data type: + + data Set cxt a = Set [a] + | Unused (cxt a -> ()) + +The only use for the Unused constructor was to force the correct +kind for the type variable cxt. - -First, GHC distinguishes between primitive arrays of (boxed) Haskell -objects (type Array# obj) and primitive arrays of bytes (type -ByteArray#). +GHC now instead allows you to specify the kind of a type variable directly, wherever +a type variable is explicitly bound. Namely: + +data declarations: + + data Set (cxt :: * -> *) a = Set [a] + +type declarations: + + type T (f :: * -> *) = f Int + +class declarations: + + class (Eq a) => C (f :: * -> *) a where ... + +forall's in type signatures: + + f :: forall (cxt :: * -> *). Set cxt Int + + -Second, it distinguishes between… - +The parentheses are required. Some of the spaces are required too, to +separate the lexemes. If you write (f::*->*) you +will get a parse error, because "::*->*" is a +single lexeme in Haskell. + - -Immutable: - -Arrays that do not change (as with “standard” Haskell arrays); you -can only read from them. Obviously, they do not need the care and -attention of the state-transformer monad. +As part of the same extension, you can put kind annotations in types +as well. Thus: + + f :: (Int :: *) -> Int + g :: forall a. a -> (a :: *) + +The syntax is + + atype ::= '(' ctype '::' kind ') + +The parentheses are required. - - - -Mutable: - + + + + +Class method types + -Arrays that may be changed or “mutated.” All the operations on them -live within the state-transformer monad and the updates happen -in-place. +Haskell 98 prohibits class method types to mention constraints on the +class type variable, thus: + + class Seq s a where + fromList :: [a] -> s a + elem :: Eq a => a -> s a -> Bool + +The type of elem is illegal in Haskell 98, because it +contains the constraint Eq a, constrains only the +class type variable (in this case a). - - - -“Static” (in C land): - -A C routine may pass an Addr# pointer back into Haskell land. There -are then primitive operations with which you may merrily grab values -over in C land, by indexing off the “static” pointer. +With the GHC lifts this restriction. - - - -“Stable” pointers: - + + + + +Multi-parameter type classes + + -If, for some reason, you wish to hand a Haskell pointer (i.e., -not an unboxed value) to a C routine, you first make the -pointer “stable,” so that the garbage collector won't forget that it -exists. That is, GHC provides a safe way to pass Haskell pointers to -C. +This section documents GHC's implementation of multi-parameter type +classes. There's lots of background in the paper Type +classes: exploring the design space (Simon Peyton Jones, Mark +Jones, Erik Meijer). -Please see for more details. +I'd like to thank people who reported shorcomings in the GHC 3.02 +implementation. Our default decisions were all conservative ones, and +the experience of these heroic pioneers has given useful concrete +examples to support several generalisations. (These appear below as +design choices not implemented in 3.02.) - - - -“Foreign objects”: - + -A “foreign object” is a safe way to pass an external object (a -C-allocated pointer, say) to Haskell and have Haskell do the Right -Thing when it no longer references the object. So, for example, C -could pass a large bitmap over to Haskell and say “please free this -memory when you're done with it.” +I've discussed these notes with Mark Jones, and I believe that Hugs +will migrate towards the same design choices as I outline here. +Thanks to him, and to many others who have offered very useful +feedback. + +Types + -Please see for more details. +There are the following restrictions on the form of a qualified +type: - - - + + + + + forall tv1..tvn (c1, ...,cn) => type + + -The libraries documentatation gives more details on all these -“primitive array” types and the operations on them. +(Here, I write the "foralls" explicitly, although the Haskell source +language omits them; in Haskell 1.4, all the free type variables of an +explicit source-language type signature are universally quantified, +except for the class type variables in a class declaration. However, +in GHC, you can give the foralls if you want. See ). - + + + + + + Each universally quantified type variable +tvi must be mentioned (i.e. appear free) in type. + +The reason for this is that a value with a type that does not obey +this restriction could not be used without introducing +ambiguity. Here, for example, is an illegal type: - -Data types with no constructors -With the flag, GHC lets you declare -a data type with no constructors. For example: - data S -- S :: * - data T a -- T :: * -> * + forall a. Eq a => Int -Syntactically, the declaration lacks the "= constrs" part. The -type can be parameterised, but only over ordinary types, of kind *; since -Haskell does not have kind signatures, you cannot parameterise over higher-kinded -types. -Such data types have only one value, namely bottom. -Nevertheless, they can be useful when defining "phantom types". - - -Pattern guards +When a value with this type was used, the constraint Eq tv +would be introduced where tv is a fresh type variable, and +(in the dictionary-translation implementation) the value would be +applied to a dictionary for Eq tv. The difficulty is that we +can never know which instance of Eq to use because we never +get any more information about tv. - -Pattern guards (Glasgow extension) -The discussion that follows is an abbreviated version of Simon Peyton Jones's original proposal. (Note that the proposal was written before pattern guards were implemented, so refers to them as unimplemented.) + + -Suppose we have an abstract data type of finite maps, with a -lookup operation: + Every constraint ci must mention at least one of the +universally quantified type variables tvi. + +For example, this type is OK because C a b mentions the +universally quantified type variable b: + -lookup :: FiniteMap -> Int -> Maybe Int + forall a. C a b => burble -The lookup returns Nothing if the supplied key is not in the domain of the mapping, and (Just v) otherwise, -where v is the value that the key maps to. Now consider the following definition: - + +The next type is illegal because the constraint Eq b does not +mention a: + -clunky env var1 var2 | ok1 && ok2 = val1 + val2 -| otherwise = var1 + var2 -where - m1 = lookup env var1 - m2 = lookup env var2 - ok1 = maybeToBool m1 - ok2 = maybeToBool m2 - val1 = expectJust m1 - val2 = expectJust m2 + forall a. Eq b => burble - -The auxiliary functions are + +The reason for this restriction is milder than the other one. The +excluded types are never useful or necessary (because the offending +context doesn't need to be witnessed at this point; it can be floated +out). Furthermore, floating them out increases sharing. Lastly, +excluding them is a conservative choice; it leaves a patch of +territory free in case we need it later. + + - -maybeToBool :: Maybe a -> Bool -maybeToBool (Just x) = True -maybeToBool Nothing = False + -expectJust :: Maybe a -> a -expectJust (Just x) = x -expectJust Nothing = error "Unexpected Nothing" - + -What is clunky doing? The guard ok1 && -ok2 checks that both lookups succeed, using -maybeToBool to convert the Maybe -types to booleans. The (lazily evaluated) expectJust -calls extract the values from the results of the lookups, and binds the -returned values to val1 and val2 -respectively. If either lookup fails, then clunky takes the -otherwise case and returns the sum of its arguments. +These restrictions apply to all types, whether declared in a type signature +or inferred. -This is certainly legal Haskell, but it is a tremendously verbose and -un-obvious way to achieve the desired effect. Arguably, a more direct way -to write clunky would be to use case expressions: +Unlike Haskell 1.4, constraints in types do not have to be of +the form (class type-variables). Thus, these type signatures +are perfectly OK + + -clunky env var1 var1 = case lookup env var1 of - Nothing -> fail - Just val1 -> case lookup env var2 of - Nothing -> fail - Just val2 -> val1 + val2 -where - fail = val1 + val2 + f :: Eq (m a) => [m a] -> [m a] + g :: Eq [a] => ... - -This is a bit shorter, but hardly better. Of course, we can rewrite any set -of pattern-matching, guarded equations as case expressions; that is -precisely what the compiler does when compiling equations! The reason that -Haskell provides guarded equations is because they allow us to write down -the cases we want to consider, one at a time, independently of each other. -This structure is hidden in the case version. Two of the right-hand sides -are really the same (fail), and the whole expression -tends to become more and more indented. -Here is how I would write clunky: +This choice recovers principal types, a property that Haskell 1.4 does not have. - -clunky env var1 var1 - | Just val1 <- lookup env var1 - , Just val2 <- lookup env var2 - = val1 + val2 -...other equations for clunky... - + + + +Class declarations -The semantics should be clear enough. The qualifers are matched in order. -For a <- qualifier, which I call a pattern guard, the -right hand side is evaluated and matched against the pattern on the left. -If the match fails then the whole guard fails and the next equation is -tried. If it succeeds, then the appropriate binding takes place, and the -next qualifier is matched, in the augmented environment. Unlike list -comprehensions, however, the type of the expression to the right of the -<- is the same as the type of the pattern to its -left. The bindings introduced by pattern guards scope over all the -remaining guard qualifiers, and over the right hand side of the equation. - + + + -Just as with list comprehensions, boolean expressions can be freely mixed -with among the pattern guards. For example: - + Multi-parameter type classes are permitted. For example: + -f x | [y] <- x - , y > 3 - , Just z <- h y - = ... + class Collection c a where + union :: c a -> c a -> c a + ...etc. - -Haskell's current guards therefore emerge as a special case, in which the -qualifier list has just one element, a boolean expression. - - - - Parallel List Comprehensions - list comprehensionsparallel - - parallel list comprehensions - - Parallel list comprehensions are a natural extension to list - comprehensions. List comprehensions can be thought of as a nice - syntax for writing maps and filters. Parallel comprehensions - extend this to include the zipWith family. + + + + + + The class hierarchy must be acyclic. However, the definition +of "acyclic" involves only the superclass relationships. For example, +this is OK: - A parallel list comprehension has multiple independent - branches of qualifier lists, each separated by a `|' symbol. For - example, the following zips together two lists: - [ (x, y) | x <- xs | y <- ys ] + class C a where { + op :: D b => a -> b -> b + } + + class C a => D a where { ... } - The behavior of parallel list comprehensions follows that of - zip, in that the resulting list will have the same length as the - shortest branch. - We can define parallel list comprehensions by translation to - regular comprehensions. Here's the basic idea: +Here, C is a superclass of D, but it's OK for a +class operation op of C to mention D. (It +would not be OK for D to be a superclass of C.) + + + + + + + There are no restrictions on the context in a class declaration +(which introduces superclasses), except that the class hierarchy must +be acyclic. So these class declarations are OK: - Given a parallel comprehension of the form: - [ e | p1 <- e11, p2 <- e12, ... - | q1 <- e21, q2 <- e22, ... - ... - ] + class Functor (m k) => FiniteMap m k where + ... + + class (Monad m, Monad (t m)) => Transform t m where + lift :: m a -> (t m) a - This will be translated to: + + + + + + + In the signature of a class operation, every constraint +must mention at least one type variable that is not a class type +variable. + +Thus: + - [ e | ((p1,p2), (q1,q2), ...) <- zipN [(p1,p2) | p1 <- e11, p2 <- e12, ...] - [(q1,q2) | q1 <- e21, q2 <- e22, ...] - ... - ] + class Collection c a where + mapC :: Collection c b => (a->b) -> c a -> c b - where `zipN' is the appropriate zip for the given number of - branches. - - - - The foreign interface +is OK because the constraint (Collection a b) mentions +b, even though it also mentions the class variable +a. On the other hand: - The foreign interface consists of the following components: - - - The Foreign Function Interface language specification - (included in this manual, in ). - You must use the command-line option - to make GHC understand the foreign declarations - defined by the FFI. - + + class C a where + op :: Eq a => (a,b) -> (a,b) + - - The Foreign module (see ) collects together several interfaces - which are useful in specifying foreign language - interfaces, including the following: - - - The ForeignObj module (see ), for managing pointers from - Haskell into the outside world. - - - - The StablePtr module (see ), for managing pointers - into Haskell from the outside world. - - - - The CTypes module (see ) gives Haskell equivalents for the - standard C datatypes, for use in making Haskell bindings - to existing C libraries. - - - - The CTypesISO module (see ) gives Haskell equivalents for C - types defined by the ISO C standard. - - - - The Storable library, for - primitive marshalling of data types between Haskell and - the foreign language. - - +is not OK because the constraint (Eq a) mentions on the class +type variable a, but not b. However, any such +example is easily fixed by moving the offending context up to the +superclass context: - - -The following sections also give some hints and tips on the use -of the foreign function interface in GHC. + + class Eq a => C a where + op ::(a,b) -> (a,b) + - -Using function headers - - -C calls, function headers - +A yet more relaxed rule would allow the context of a class-op signature +to mention only class type variables. However, that conflicts with +Rule 1(b) for types above. - -When generating C (using the directive), one can assist the -C compiler in detecting type errors by using the directive -() to provide .h files containing function headers. + + -For example, - + The type of each class operation must mention all of +the class type variables. For example: - -#include "HsFFI.h" + class Coll s a where + empty :: s + insert :: s -> a -> s + + + +is not OK, because the type of empty doesn't mention +a. This rule is a consequence of Rule 1(a), above, for +types, and has the same motivation. -void initialiseEFS (HsInt size); -HsInt terminateEFS (void); -HsForeignObj emptyEFS(void); -HsForeignObj updateEFS (HsForeignObj a, HsInt i, HsInt x); -HsInt lookupEFS (HsForeignObj a, HsInt i); +Sometimes, offending class declarations exhibit misunderstandings. For +example, Coll might be rewritten + + + + class Coll s a where + empty :: s a + insert :: s a -> a -> s a - - The types HsInt, - HsForeignObj etc. are described in . - Note that this approach is only - essential for returning - floats (or if sizeof(int) != - sizeof(int *) on your architecture) but is a Good - Thing for anyone who cares about writing solid code. You're - crazy not to do it. +which makes the connection between the type of a collection of +a's (namely (s a)) and the element type a. +Occasionally this really doesn't work, in which case you can split the +class like this: - - + + class CollE s where + empty :: s - -Multi-parameter type classes - + class CollE s => Coll s a where + insert :: s -> a -> s + - -This section documents GHC's implementation of multi-parameter type -classes. There's lots of background in the paper Type -classes: exploring the design space (Simon Peyton Jones, Mark -Jones, Erik Meijer). - - -I'd like to thank people who reported shorcomings in the GHC 3.02 -implementation. Our default decisions were all conservative ones, and -the experience of these heroic pioneers has given useful concrete -examples to support several generalisations. (These appear below as -design choices not implemented in 3.02.) + + + - -I've discussed these notes with Mark Jones, and I believe that Hugs -will migrate towards the same design choices as I outline here. -Thanks to him, and to many others who have offered very useful -feedback. - -Types + + + +Instance declarations -There are the following restrictions on the form of a qualified -type: - + + + + Instance declarations may not overlap. The two instance +declarations + - forall tv1..tvn (c1, ...,cn) => type + instance context1 => C type1 where ... + instance context2 => C type2 where ... - + +"overlap" if type1 and type2 unify + +However, if you give the command line option +-fallow-overlapping-instances +option then overlapping instance declarations are permitted. +However, GHC arranges never to commit to using an instance declaration +if another instance declaration also applies, either now or later. + + + -(Here, I write the "foralls" explicitly, although the Haskell source -language omits them; in Haskell 1.4, all the free type variables of an -explicit source-language type signature are universally quantified, -except for the class type variables in a class declaration. However, -in GHC, you can give the foralls if you want. See ). + EITHER type1 and type2 do not unify + + - - + OR type2 is a substitution instance of type1 +(but not identical to type1), or vice versa. + + + +Notice that these rules + - Each universally quantified type variable -tvi must be mentioned (i.e. appear free) in type. + make it clear which instance decl to use +(pick the most specific one that matches) -The reason for this is that a value with a type that does not obey -this restriction could not be used without introducing -ambiguity. Here, for example, is an illegal type: + + + + + do not mention the contexts context1, context2 +Reason: you can pick which instance decl +"matches" based on the type. + + + +However the rules are over-conservative. Two instance declarations can overlap, +but it can still be clear in particular situations which to use. For example: - forall a. Eq a => Int + instance C (Int,a) where ... + instance C (a,Bool) where ... - - -When a value with this type was used, the constraint Eq tv -would be introduced where tv is a fresh type variable, and -(in the dictionary-translation implementation) the value would be -applied to a dictionary for Eq tv. The difficulty is that we -can never know which instance of Eq to use because we never -get any more information about tv. +These are rejected by GHC's rules, but it is clear what to do when trying +to solve the constraint C (Int,Int) because the second instance +cannot apply. Yell if this restriction bites you. + + +GHC is also conservative about committing to an overlapping instance. For example: + + class C a where { op :: a -> a } + instance C [Int] where ... + instance C a => C [a] where ... + + f :: C b => [b] -> [b] + f x = op x + +From the RHS of f we get the constraint C [b]. But +GHC does not commit to the second instance declaration, because in a paricular +call of f, b might be instantiate to Int, so the first instance declaration +would be appropriate. So GHC rejects the program. If you add +GHC will instead silently pick the second instance, without complaining about +the problem of subsequent instantiations. + + +Regrettably, GHC doesn't guarantee to detect overlapping instance +declarations if they appear in different modules. GHC can "see" the +instance declarations in the transitive closure of all the modules +imported by the one being compiled, so it can "see" all instance decls +when it is compiling Main. However, it currently chooses not +to look at ones that can't possibly be of use in the module currently +being compiled, in the interests of efficiency. (Perhaps we should +change that decision, at least for Main.) - Every constraint ci must mention at least one of the -universally quantified type variables tvi. - -For example, this type is OK because C a b mentions the -universally quantified type variable b: + There are no restrictions on the type in an instance +head, except that at least one must not be a type variable. +The instance "head" is the bit after the "=>" in an instance decl. For +example, these are OK: - forall a. C a b => burble + instance C Int a where ... + + instance D (Int, Int) where ... + + instance E [[a]] where ... -The next type is illegal because the constraint Eq b does not -mention a: +Note that instance heads may contain repeated type variables. +For example, this is OK: - forall a. Eq b => burble + instance Stateful (ST s) (MutVar s) where ... -The reason for this restriction is milder than the other one. The -excluded types are never useful or necessary (because the offending -context doesn't need to be witnessed at this point; it can be floated -out). Furthermore, floating them out increases sharing. Lastly, -excluding them is a conservative choice; it leaves a patch of -territory free in case we need it later. - - - +The "at least one not a type variable" restriction is to ensure that +context reduction terminates: each reduction step removes one type +constructor. For example, the following would make the type checker +loop if it wasn't excluded: - - + + instance C a => C a where ... + - -These restrictions apply to all types, whether declared in a type signature -or inferred. - - -Unlike Haskell 1.4, constraints in types do not have to be of -the form (class type-variables). Thus, these type signatures -are perfectly OK - +There are two situations in which the rule is a bit of a pain. First, +if one allows overlapping instance declarations then it's quite +convenient to have a "default instance" declaration that applies if +something more specific does not: - - f :: Eq (m a) => [m a] -> [m a] - g :: Eq [a] => ... + instance C a where + op = ... -- Default - - -This choice recovers principal types, a property that Haskell 1.4 does not have. - +Second, sometimes you might want to use the following to get the +effect of a "class synonym": - - -Class declarations + + class (C1 a, C2 a, C3 a) => C a where { } - + instance (C1 a, C2 a, C3 a) => C a where { } + - - - - Multi-parameter type classes are permitted. For example: +This allows you to write shorter signatures: - class Collection c a where - union :: c a -> c a -> c a - ...etc. + f :: C a => ... + + + +instead of + + + + f :: (C1 a, C2 a, C3 a) => ... +I'm on the lookout for a simple rule that preserves decidability while +allowing these idioms. The experimental flag +-fallow-undecidable-instances +option lifts this restriction, allowing all the types in an +instance head to be type variables. - The class hierarchy must be acyclic. However, the definition -of "acyclic" involves only the superclass relationships. For example, -this is OK: + Unlike Haskell 1.4, instance heads may use type +synonyms. As always, using a type synonym is just shorthand for +writing the RHS of the type synonym definition. For example: - class C a where { - op :: D b => a -> b -> b - } - - class C a => D a where { ... } + type Point = (Int,Int) + instance C Point where ... + instance C [Point] where ... -Here, C is a superclass of D, but it's OK for a -class operation op of C to mention D. (It -would not be OK for D to be a superclass of C.) +is legal. However, if you added - - - - - There are no restrictions on the context in a class declaration -(which introduces superclasses), except that the class hierarchy must -be acyclic. So these class declarations are OK: + + instance C (Int,Int) where ... + - - class Functor (m k) => FiniteMap m k where - ... +as well, then the compiler will complain about the overlapping +(actually, identical) instance declarations. As always, type synonyms +must be fully applied. You cannot, for example, write: - class (Monad m, Monad (t m)) => Transform t m where - lift :: m a -> (t m) a + + + type P a = [[a]] + instance Monad P where ... +This design decision is independent of all the others, and easily +reversed, but it makes sense to me. + - In the signature of a class operation, every constraint -must mention at least one type variable that is not a class type -variable. - -Thus: +The types in an instance-declaration context must all +be type variables. Thus - class Collection c a where - mapC :: Collection c b => (a->b) -> c a -> c b +instance C a b => Eq (a,b) where ... -is OK because the constraint (Collection a b) mentions -b, even though it also mentions the class variable -a. On the other hand: +is OK, but - class C a where - op :: Eq a => (a,b) -> (a,b) +instance C Int b => Foo b where ... -is not OK because the constraint (Eq a) mentions on the class -type variable a, but not b. However, any such -example is easily fixed by moving the offending context up to the -superclass context: - +is not OK. Again, the intent here is to make sure that context +reduction terminates. - - class Eq a => C a where - op ::(a,b) -> (a,b) - +Voluminous correspondence on the Haskell mailing list has convinced me +that it's worth experimenting with a more liberal rule. If you use +the flag can use arbitrary +types in an instance context. 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. + + -A yet more relaxed rule would allow the context of a class-op signature -to mention only class type variables. However, that conflicts with -Rule 1(b) for types above. + - - - - The type of each class operation must mention all of -the class type variables. For example: + + + + +Implicit parameters + + Implicit paramters are implemented as described in +"Implicit parameters: dynamic scoping with static types", +J Lewis, MB Shields, E Meijer, J Launchbury, +27th ACM Symposium on Principles of Programming Languages (POPL'00), +Boston, Jan 2000. + +(Most of the following, stil rather incomplete, documentation is due to Jeff Lewis.) + +A variable is called dynamically bound when it is bound by the calling +context of a function and statically bound when bound by the callee's +context. In Haskell, all variables are statically bound. Dynamic +binding of variables is a notion that goes back to Lisp, but was later +discarded in more modern incarnations, such as Scheme. Dynamic binding +can be very confusing in an untyped language, and unfortunately, typed +languages, in particular Hindley-Milner typed languages like Haskell, +only support static scoping of variables. + + +However, by a simple extension to the type class system of Haskell, we +can support dynamic binding. Basically, we express the use of a +dynamically bound variable as a constraint on the type. These +constraints lead to types of the form (?x::t') => t, which says "this +function uses a dynamically-bound variable ?x +of type t'". For +example, the following expresses the type of a sort function, +implicitly parameterized by a comparison function named cmp. - class Coll s a where - empty :: s - insert :: s -> a -> s + sort :: (?cmp :: a -> a -> Bool) => [a] -> [a] +The dynamic binding constraints are just a new form of predicate in the type class system. + + +An implicit parameter is introduced by the special form ?x, +where x is +any valid identifier. Use if this construct also introduces new +dynamic binding constraints. For example, the following definition +shows how we can define an implicitly parameterized sort function in +terms of an explicitly parameterized sortBy function: + + sortBy :: (a -> a -> Bool) -> [a] -> [a] + sort :: (?cmp :: a -> a -> Bool) => [a] -> [a] + sort = sortBy ?cmp + +Dynamic binding constraints behave just like other type class +constraints in that they are automatically propagated. Thus, when a +function is used, its implicit parameters are inherited by the +function that called it. For example, our sort function might be used +to pick out the least value in a list: + + least :: (?cmp :: a -> a -> Bool) => [a] -> a + least xs = fst (sort xs) + +Without lifting a finger, the ?cmp parameter is +propagated to become a parameter of least as well. With explicit +parameters, the default is that parameters must always be explicit +propagated. With implicit parameters, the default is to always +propagate them. + + +An implicit parameter differs from other type class constraints in the +following way: All uses of a particular implicit parameter must have +the same type. This means that the type of (?x, ?x) +is (?x::a) => (a,a), and not +(?x::a, ?x::b) => (a, b), as would be the case for type +class constraints. + + +An implicit parameter is bound using the standard +let binding form, where the bindings must be a +collection of simple bindings to implicit-style variables (no +function-style bindings, and no type signatures); these bindings are +neither polymorphic or recursive. This form binds the implicit +parameters arising in the body, not the free variables as a +let or where would do. For +example, we define the min function by binding +cmp. + + min :: [a] -> a + min = let ?cmp = (<=) in least + + +Note the following points: + + +You may not mix implicit-parameter bindings with ordinary bindings in a +single let +expression; use two nested lets instead. + -is not OK, because the type of empty doesn't mention -a. This rule is a consequence of Rule 1(a), above, for -types, and has the same motivation. - -Sometimes, offending class declarations exhibit misunderstandings. For -example, Coll might be rewritten + +You may put multiple implicit-parameter bindings in a +single let expression; they are not treated +as a mutually recursive group (as ordinary let bindings are). +Instead they are treated as a non-recursive group, each scoping over the bindings that +follow. For example, consider: + + f y = let { ?x = y; ?x = ?x+1 } in ?x + +This function adds one to its argument. + + +You may not have an implicit-parameter binding in a where clause, +only in a let binding. + + + You can't have an implicit parameter in the context of a class or instance +declaration. For example, both these declarations are illegal: - class Coll s a where - empty :: s a - insert :: s a -> a -> s a + class (?x::Int) => C a where ... + instance (?x::a) => Foo [a] where ... +Reason: exactly which implicit parameter you pick up depends on exactly where +you invoke a function. But the ``invocation'' of instance declarations is done +behind the scenes by the compiler, so it's hard to figure out exactly where it is done. +Easiest thing is to outlaw the offending types. + + + + + + + +Linear implicit parameters + + +Linear implicit parameters are an idea developed by Koen Claessen, +Mark Shields, and Simon PJ. They address the long-standing +problem that monads seem over-kill for certain sorts of problem, notably: + + + distributing a supply of unique names + distributing a suppply of random numbers + distributing an oracle (as in QuickCheck) + + + +Linear implicit parameters are just like ordinary implicit parameters, +except that they are "linear" -- that is, they cannot be copied, and +must be explicitly "split" instead. Linear implicit parameters are +written '%x' instead of '?x'. +(The '/' in the '%' suggests the split!) + + +For example: + + import GHC.Exts( Splittable ) + data NameSupply = ... + + splitNS :: NameSupply -> (NameSupply, NameSupply) + newName :: NameSupply -> Name -which makes the connection between the type of a collection of -a's (namely (s a)) and the element type a. -Occasionally this really doesn't work, in which case you can split the -class like this: + instance Splittable NameSupply where + split = splitNS + f :: (%ns :: NameSupply) => Env -> Expr -> Expr + f env (Lam x e) = Lam x' (f env e) + where + x' = newName %ns + env' = extend env x x' + ...more equations for f... + +Notice that the implicit parameter %ns is consumed + + once by the call to newName + once by the recursive call to f + + + +So the translation done by the type checker makes +the parameter explicit: - class CollE s where - empty :: s - - class CollE s => Coll s a where - insert :: s -> a -> s + f :: NameSupply -> Env -> Expr -> Expr + f ns env (Lam x e) = Lam x' (f ns1 env e) + where + (ns1,ns2) = splitNS ns + x' = newName ns2 + env = extend env x x' - - +Notice the call to 'split' introduced by the type checker. +How did it know to use 'splitNS'? Because what it really did +was to introduce a call to the overloaded function 'split', +defined by the class Splittable: + + class Splittable a where + split :: a -> (a,a) + +The instance for Splittable NameSupply tells GHC how to implement +split for name supplies. But we can simply write + + g x = (x, %ns, %ns) + +and GHC will infer + + g :: (Splittable a, %ns :: a) => b -> (b,a,a) + +The Splittable class is built into GHC. It's exported by module +GHC.Exts. + +Other points: + + '?x' and '%x' +are entirely distinct implicit parameters: you + can use them together and they won't intefere with each other. - + You can bind linear implicit parameters in 'with' clauses. + You cannot have implicit parameters (whether linear or not) + in the context of a class or instance declaration. + - - - -Instance declarations +Warnings - - - - +The monomorphism restriction is even more important than usual. +Consider the example above: + + f :: (%ns :: NameSupply) => Env -> Expr -> Expr + f env (Lam x e) = Lam x' (f env e) + where + x' = newName %ns + env' = extend env x x' + +If we replaced the two occurrences of x' by (newName %ns), which is +usually a harmless thing to do, we get: + + f :: (%ns :: NameSupply) => Env -> Expr -> Expr + f env (Lam x e) = Lam (newName %ns) (f env e) + where + env' = extend env x (newName %ns) + +But now the name supply is consumed in three places +(the two calls to newName,and the recursive call to f), so +the result is utterly different. Urk! We don't even have +the beta rule. + - Instance declarations may not overlap. The two instance -declarations +Well, this is an experimental change. With implicit +parameters we have already lost beta reduction anyway, and +(as John Launchbury puts it) we can't sensibly reason about +Haskell programs without knowing their typing. + + +Recursive functions +Linear implicit parameters can be particularly tricky when you have a recursive function +Consider - instance context1 => C type1 where ... - instance context2 => C type2 where ... + foo :: %x::T => Int -> [Int] + foo 0 = [] + foo n = %x : foo (n-1) +where T is some type in class Splittable. + +Do you get a list of all the same T's or all different T's +(assuming that split gives two distinct T's back)? + +If you supply the type signature, taking advantage of polymorphic +recursion, you get what you'd probably expect. Here's the +translated term, where the implicit param is made explicit: + + foo x 0 = [] + foo x n = let (x1,x2) = split x + in x1 : foo x2 (n-1) + +But if you don't supply a type signature, GHC uses the Hindley +Milner trick of using a single monomorphic instance of the function +for the recursive calls. That is what makes Hindley Milner type inference +work. So the translation becomes + + foo x = let + foom 0 = [] + foom n = x : foom (n-1) + in + foom + +Result: 'x' is not split, and you get a list of identical T's. So the +semantics of the program depends on whether or not foo has a type signature. +Yikes! + +You may say that this is a good reason to dislike linear implicit parameters +and you'd be right. That is why they are an experimental feature. + + + -"overlap" if type1 and type2 unify - -However, if you give the command line option --fallow-overlapping-instances -option then two overlapping instance declarations are permitted -iff - + +Functional dependencies + - - + Functional dependencies are implemented as described by Mark Jones +in “Type Classes with Functional Dependencies”, Mark P. Jones, +In Proceedings of the 9th European Symposium on Programming, +ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782, +. + - EITHER type1 and type2 do not unify +There should be more documentation, but there isn't (yet). Yell if you need it. - - + + + + +Arbitrary-rank polymorphism + - OR type2 is a substitution instance of type1 -(but not identical to type1) +Haskell type signatures are implicitly quantified. The new keyword forall +allows us to say exactly what this means. For example: - - - - OR vice versa + + g :: b -> b + +means this: + + g :: forall b. (b -> b) + +The two are treated identically. - - - - - -Notice that these rules + +However, GHC's type system supports arbitrary-rank +explicit universal quantification in +types. +For example, all the following types are legal: + + f1 :: forall a b. a -> b -> a + g1 :: forall a b. (Ord a, Eq b) => a -> b -> a - - + f2 :: (forall a. a->a) -> Int -> Int + g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int + f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool + +Here, f1 and g1 are rank-1 types, and +can be written in standard Haskell (e.g. f1 :: a->b->a). +The forall makes explicit the universal quantification that +is implicitly added by Haskell. + - make it clear which instance decl to use -(pick the most specific one that matches) - +The functions f2 and g2 have rank-2 types; +the forall is on the left of a function arrrow. As g2 +shows, the polymorphic type on the left of the function arrow can be overloaded. - - - - do not mention the contexts context1, context2 -Reason: you can pick which instance decl -"matches" based on the type. +The functions f3 and g3 have rank-3 types; +they have rank-2 types on the left of a function arrow. - - + +GHC allows types of arbitrary rank; you can nest foralls +arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but +that restriction has now been lifted.) +In particular, a forall-type (also called a "type scheme"), +including an operational type class context, is legal: + + On the left of a function arrow + On the right of a function arrow (see ) + As the argument of a constructor, or type of a field, in a data type declaration. For +example, any of the f1,f2,f3,g1,g2,g3 above would be valid +field type signatures. + As the type of an implicit parameter + In a pattern type signature (see ) +There is one place you cannot put a forall: +you cannot instantiate a type variable with a forall-type. So you cannot +make a forall-type the argument of a type constructor. So these types are illegal: + + x1 :: [forall a. a->a] + x2 :: (forall a. a->a, Int) + x3 :: Maybe (forall a. a->a) + +Of course forall becomes a keyword; you can't use forall as +a type variable any more! + -Regrettably, GHC doesn't guarantee to detect overlapping instance -declarations if they appear in different modules. GHC can "see" the -instance declarations in the transitive closure of all the modules -imported by the one being compiled, so it can "see" all instance decls -when it is compiling Main. However, it currently chooses not -to look at ones that can't possibly be of use in the module currently -being compiled, in the interests of efficiency. (Perhaps we should -change that decision, at least for Main.) + +Examples + + +In a data or newtype declaration one can quantify +the types of the constructor arguments. Here are several examples: - - - There are no restrictions on the type in an instance -head, except that at least one must not be a type variable. -The instance "head" is the bit after the "=>" in an instance decl. For -example, these are OK: - - instance C Int a where ... +data T a = T1 (forall b. b -> b -> b) a - instance D (Int, Int) where ... +data MonadT m = MkMonad { return :: forall a. a -> m a, + bind :: forall a b. m a -> (a -> m b) -> m b + } - instance E [[a]] where ... +newtype Swizzle = MkSwizzle (Ord a => [a] -> [a]) + -Note that instance heads may contain repeated type variables. -For example, this is OK: + +The constructors have rank-2 types: + + - instance Stateful (ST s) (MutVar s) where ... +T1 :: forall a. (forall b. b -> b -> b) -> a -> T a +MkMonad :: forall m. (forall a. a -> m a) + -> (forall a b. m a -> (a -> m b) -> m b) + -> MonadT m +MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle + -The "at least one not a type variable" restriction is to ensure that -context reduction terminates: each reduction step removes one type -constructor. For example, the following would make the type checker -loop if it wasn't excluded: + +Notice that you don't need to use a forall if there's an +explicit context. For example in the first argument of the +constructor MkSwizzle, an implicit "forall a." is +prefixed to the argument type. The implicit forall +quantifies all type variables that are not already in scope, and are +mentioned in the type quantified over. + + +As for type signatures, implicit quantification happens for non-overloaded +types too. So if you write this: - instance C a => C a where ... + data T a = MkT (Either a b) (b -> b) - -There are two situations in which the rule is a bit of a pain. First, -if one allows overlapping instance declarations then it's quite -convenient to have a "default instance" declaration that applies if -something more specific does not: - +it's just as if you had written this: - instance C a where - op = ... -- Default + data T a = MkT (forall b. Either a b) (forall b. b -> b) +That is, since the type variable b isn't in scope, it's +implicitly universally quantified. (Arguably, it would be better +to require explicit quantification on constructor arguments +where that is what is wanted. Feedback welcomed.) + -Second, sometimes you might want to use the following to get the -effect of a "class synonym": + +You construct values of types T1, MonadT, Swizzle by applying +the constructor to suitable values, just as usual. For example, + + - class (C1 a, C2 a, C3 a) => C a where { } + a1 :: T Int + a1 = T1 (\xy->x) 3 + + a2, a3 :: Swizzle + a2 = MkSwizzle sort + a3 = MkSwizzle reverse + + a4 :: MonadT Maybe + a4 = let r x = Just x + b m k = case m of + Just y -> k y + Nothing -> Nothing + in + MkMonad r b - instance (C1 a, C2 a, C3 a) => C a where { } + mkTs :: (forall b. b -> b -> b) -> a -> [T a] + mkTs f x y = [T1 f x, T1 f y] + -This allows you to write shorter signatures: - - - - f :: C a => ... - - + +The type of the argument can, as usual, be more general than the type +required, as (MkSwizzle reverse) shows. (reverse +does not need the Ord constraint.) + -instead of + +When you use pattern matching, the bound variables may now have +polymorphic types. For example: + + - f :: (C1 a, C2 a, C3 a) => ... - + f :: T a -> a -> (a, Char) + f (T1 w k) x = (w k x, w 'c' 'd') + g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b] + g (MkSwizzle s) xs f = s (map f (s xs)) -I'm on the lookout for a simple rule that preserves decidability while -allowing these idioms. The experimental flag --fallow-undecidable-instances -option lifts this restriction, allowing all the types in an -instance head to be type variables. + h :: MonadT m -> [m a] -> m [a] + h m [] = return m [] + h m (x:xs) = bind m x $ \y -> + bind m (h m xs) $ \ys -> + return m (y:ys) + - - - Unlike Haskell 1.4, instance heads may use type -synonyms. As always, using a type synonym is just shorthand for -writing the RHS of the type synonym definition. For example: +In the function h we use the record selectors return +and bind to extract the polymorphic bind and return functions +from the MonadT data structure, rather than using pattern +matching. + + + +Type inference + +In general, type inference for arbitrary-rank types is undecideable. +GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96) +to get a decidable algorithm by requiring some help from the programmer. +We do not yet have a formal specification of "some help" but the rule is this: + + +For a lambda-bound or case-bound variable, x, either the programmer +provides an explicit polymorphic type for x, or GHC's type inference will assume +that x's type has no foralls in it. + + +What does it mean to "provide" an explicit type for x? You can do that by +giving a type signature for x directly, using a pattern type signature +(), thus: - type Point = (Int,Int) - instance C Point where ... - instance C [Point] where ... + \ f :: (forall a. a->a) -> (f True, f 'c') - - -is legal. However, if you added - - +Alternatively, you can give a type signature to the enclosing +context, which GHC can "push down" to find the type for the variable: - instance C (Int,Int) where ... + (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char) - - -as well, then the compiler will complain about the overlapping -(actually, identical) instance declarations. As always, type synonyms -must be fully applied. You cannot, for example, write: - - +Here the type signature on the expression can be pushed inwards +to give a type signature for f. Similarly, and more commonly, +one can give a type signature for the function itself: + + h :: (forall a. a->a) -> (Bool,Char) + h f = (f True, f 'c') + +You don't need to give a type signature if the lambda bound variable +is a constructor argument. Here is an example we saw earlier: - type P a = [[a]] - instance Monad P where ... + f :: T a -> a -> (a, Char) + f (T1 w k) x = (w k x, w 'c' 'd') +Here we do not need to give a type signature to w, because +it is an argument of constructor T1 and that tells GHC all +it needs to know. + + -This design decision is independent of all the others, and easily -reversed, but it makes sense to me. - - - + +Implicit quantification -The types in an instance-declaration context must all -be type variables. Thus - - +GHC performs implicit quantification as follows. At the top level (only) of +user-written types, if and only if there is no explicit forall, +GHC finds all the type variables mentioned in the type that are not already +in scope, and universally quantifies them. For example, the following pairs are +equivalent: -instance C a b => Eq (a,b) where ... - - + f :: a -> a + f :: forall a. a -> a -is OK, but + g (x::a) = let + h :: a -> b -> b + h x y = y + in ... + g (x::a) = let + h :: forall b. a -> b -> b + h x y = y + in ... + + + +Notice that GHC does not find the innermost possible quantification +point. For example: + + f :: (a -> a) -> Int + -- MEANS + f :: forall a. (a -> a) -> Int + -- NOT + f :: (forall a. a -> a) -> Int - -instance C Int b => Foo b where ... + g :: (Ord a => a -> a) -> Int + -- MEANS the illegal type + g :: forall a. (Ord a => a -> a) -> Int + -- NOT + g :: (forall a. Ord a => a -> a) -> Int +The latter produces an illegal type, which you might think is silly, +but at least the rule is simple. If you want the latter type, you +can write your for-alls explicitly. Indeed, doing so is strongly advised +for rank-2 types. + + + + +Liberalised type synonyms + -is not OK. Again, the intent here is to make sure that context -reduction terminates. + +Type synonmys are like macros at the type level, and +GHC does validity checking on types only after expanding type synonyms. +That means that GHC can be very much more liberal about type synonyms than Haskell 98: + + You can write a forall (including overloading) +in a type synonym, thus: + + type Discard a = forall b. Show b => a -> b -> (a, String) -Voluminous correspondence on the Haskell mailing list has convinced me -that it's worth experimenting with a more liberal rule. If you use -the flag can use arbitrary -types in an instance context. 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. + f :: Discard a + f x y = (x, show y) + g :: Discard Int -> (Int,Bool) -- A rank-2 type + g f = f Int True + - - - + +You can write an unboxed tuple in a type synonym: + + type Pr = (# Int, Int #) - + h :: Int -> Pr + h x = (# x, x #) + + - + +You can apply a type synonym to a forall type: + + type Foo a = a -> a -> Bool + + f :: Foo (forall b. b->b) + +After expanding the synonym, f has the legal (in GHC) type: + + f :: (forall b. b->b) -> (forall b. b->b) -> Bool + + - -Implicit parameters - + +You can apply a type synonym to a partially applied type synonym: + + type Generic i o = forall x. i x -> o x + type Id x = x + + foo :: Generic Id [] + +After epxanding the synonym, foo has the legal (in GHC) type: + + foo :: forall x. x -> [x] + + - Implicit paramters are implemented as described in -"Implicit parameters: dynamic scoping with static types", -J Lewis, MB Shields, E Meijer, J Launchbury, -27th ACM Symposium on Principles of Programming Languages (POPL'00), -Boston, Jan 2000. + -There should be more documentation, but there isn't (yet). Yell if you need it. +GHC currently does kind checking before expanding synonyms (though even that +could be changed.) + +After expanding type synonyms, GHC does validity checking on types, looking for +the following mal-formedness which isn't detected simply by kind checking: - - You can't have an implicit parameter in the context of a class or instance -declaration. For example, both these declarations are illegal: - - class (?x::Int) => C a where ... - instance (?x::a) => Foo [a] where ... - -Reason: exactly which implicit parameter you pick up depends on exactly where -you invoke a function. But the ``invocation'' of instance declarations is done -behind the scenes by the compiler, so it's hard to figure out exactly where it is done. -Easiest thing is to outlaw the offending types. - - + +Type constructor applied to a type involving for-alls. + + +Unboxed tuple on left of an arrow. + + +Partially-applied type synonym. + +So, for example, +this will be rejected: + + type Pr = (# Int, Int #) - - + h :: Pr -> Int + h x = ... + +because GHC does not allow unboxed tuples on the left of a function arrow. + + - -Functional dependencies - + +For-all hoisting + +It is often convenient to use generalised type synonyms at the right hand +end of an arrow, thus: + + type Discard a = forall b. a -> b -> a - Functional dependencies are implemented as described by Mark Jones -in "Type Classes with Functional Dependencies", Mark P. Jones, -In Proceedings of the 9th European Symposium on Programming, -ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782. + g :: Int -> Discard Int + g x y z = x+y + +Simply expanding the type synonym would give + + g :: Int -> (forall b. Int -> b -> Int) + +but GHC "hoists" the forall to give the isomorphic type + + g :: forall b. Int -> Int -> b -> Int + +In general, the rule is this: to determine the type specified by any explicit +user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly +performs the transformation: + + type1 -> forall a1..an. context2 => type2 +==> + forall a1..an. context2 => type1 -> type2 + +(In fact, GHC tries to retain as much synonym information as possible for use in +error messages, but that is a usability issue.) This rule applies, of course, whether +or not the forall comes from a synonym. For example, here is another +valid way to write g's type signature: + + g :: Int -> Int -> forall b. b -> Int + - -There should be more documentation, but there isn't (yet). Yell if you need it. +When doing this hoisting operation, GHC eliminates duplicate constraints. For +example: + + type Foo a = (?x::Int) => Bool -> a + g :: Foo (Foo Int) + +means + + g :: (?x::Int) => Bool -> Bool -> Int + - + - -Explicit universal quantification +<sect2 id="existential-quantification"> +<title>Existentially quantified data constructors -GHC's type system supports explicit universal quantification in -constructor fields and function arguments. This is useful for things -like defining runST from the state-thread world. -GHC's syntax for this now agrees with Hugs's, namely: +The idea of using existential quantification in data type declarations +was suggested by Laufer (I believe, thought doubtless someone will +correct me), and implemented in Hope+. It's been in Lennart +Augustsson's hbc Haskell compiler for several years, and +proved very useful. Here's the idea. Consider the declaration: - forall a b. (Ord a, Eq b) => a -> b -> a + data Foo = forall a. MkFoo a (a -> Bool) + | Nil -The context is, of course, optional. You can't use forall as -a type variable any more! - - - -Haskell type signatures are implicitly quantified. The forall -allows us to say exactly what this means. For example: +The data type Foo has two constructors with types: - g :: b -> b + MkFoo :: forall a. a -> (a -> Bool) -> Foo + Nil :: Foo -means this: +Notice that the type variable a in the type of MkFoo +does not appear in the data type itself, which is plain Foo. +For example, the following expression is fine: - g :: forall b. (b -> b) + [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] -The two are treated identically. +Here, (MkFoo 3 even) packages an integer with a function +even that maps an integer to Bool; and MkFoo 'c' +isUpper packages a character with a compatible function. These +two things are each of type Foo and can be put in a list. - -Universally-quantified data type fields - - -In a data or newtype declaration one can quantify -the types of the constructor arguments. Here are several examples: +What can we do with a value of type Foo?. In particular, +what happens when we pattern-match on MkFoo? -data T a = T1 (forall b. b -> b -> b) a - -data MonadT m = MkMonad { return :: forall a. a -> m a, - bind :: forall a b. m a -> (a -> m b) -> m b - } - -newtype Swizzle = MkSwizzle (Ord a => [a] -> [a]) + f (MkFoo val fn) = ??? -The constructors now have so-called rank 2 polymorphic -types, in which there is a for-all in the argument types.: +Since all we know about val and fn is that they +are compatible, the only (useful) thing we can do with them is to +apply fn to val to get a boolean. For example: -T1 :: forall a. (forall b. b -> b -> b) -> a -> T a -MkMonad :: forall m. (forall a. a -> m a) - -> (forall a b. m a -> (a -> m b) -> m b) - -> MonadT m -MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle + f :: Foo -> Bool + f (MkFoo val fn) = fn val -Notice that you don't need to use a forall if there's an -explicit context. For example in the first argument of the -constructor MkSwizzle, an implicit "forall a." is -prefixed to the argument type. The implicit forall -quantifies all type variables that are not already in scope, and are -mentioned in the type quantified over. +What this allows us to do is to package heterogenous values +together with a bunch of functions that manipulate them, and then treat +that collection of packages in a uniform manner. You can express +quite a bit of object-oriented-like programming this way. - -As for type signatures, implicit quantification happens for non-overloaded -types too. So if you write this: + +Why existential? + - - data T a = MkT (Either a b) (b -> b) - + +What has this to do with existential quantification? +Simply that MkFoo has the (nearly) isomorphic type + -it's just as if you had written this: + - data T a = MkT (forall b. Either a b) (forall b. b -> b) + MkFoo :: (exists a . (a, a -> Bool)) -> Foo -That is, since the type variable b isn't in scope, it's -implicitly universally quantified. (Arguably, it would be better -to require explicit quantification on constructor arguments -where that is what is wanted. Feedback welcomed.) - + +But Haskell programmers can safely think of the ordinary +universally quantified type given above, thereby avoiding +adding a new existential quantification construct. + - -Construction + + + +Type classes -You construct values of types T1, MonadT, Swizzle by applying -the constructor to suitable values, just as usual. For example, +An easy extension (implemented in hbc) is to allow +arbitrary contexts before the constructor. For example: -(T1 (\xy->x) 3) :: T Int - -(MkSwizzle sort) :: Swizzle -(MkSwizzle reverse) :: Swizzle - -(let r x = Just x - b m k = case m of - Just y -> k y - Nothing -> Nothing - in - MkMonad r b) :: MonadT Maybe +data Baz = forall a. Eq a => Baz1 a a + | forall b. Show b => Baz2 b (b -> b) -The type of the argument can, as usual, be more general than the type -required, as (MkSwizzle reverse) shows. (reverse -does not need the Ord constraint.) - - - - - -Pattern matching - - -When you use pattern matching, the bound variables may now have -polymorphic types. For example: +The two constructors have the types you'd expect: - f :: T a -> a -> (a, Char) - f (T1 f k) x = (f k x, f 'c' 'd') - - g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b] - g (MkSwizzle s) xs f = s (map f (s xs)) - - h :: MonadT m -> [m a] -> m [a] - h m [] = return m [] - h m (x:xs) = bind m x $ \y -> - bind m (h m xs) $ \ys -> - return m (y:ys) +Baz1 :: forall a. Eq a => a -> a -> Baz +Baz2 :: forall b. Show b => b -> (b -> b) -> Baz -In the function h we use the record selectors return -and bind to extract the polymorphic bind and return functions -from the MonadT data structure, rather than using pattern -matching. +But when pattern matching on Baz1 the matched values can be compared +for equality, and when pattern matching on Baz2 the first matched +value can be converted to a string (as well as applying the function to it). +So this program is legal: -You cannot pattern-match against an argument that is polymorphic. -For example: - newtype TIM s a = TIM (ST s (Maybe a)) - - runTIM :: (forall s. TIM s a) -> Maybe a - runTIM (TIM m) = runST m + f :: Baz -> String + f (Baz1 p q) | p == q = "Yes" + | otherwise = "No" + f (Baz2 v fn) = show (fn v) -Here the pattern-match fails, because you can't pattern-match against -an argument of type (forall s. TIM s a). Instead you -must bind the variable and pattern match in the right hand side: - - - runTIM :: (forall s. TIM s a) -> Maybe a - runTIM tm = case tm of { TIM m -> runST m } - +Operationally, in a dictionary-passing implementation, the +constructors Baz1 and Baz2 must store the +dictionaries for Eq and Show respectively, and +extract it on pattern matching. + -The tm on the right hand side is (invisibly) instantiated, like -any polymorphic value at its occurrence site, and now you can pattern-match -against it. + +Notice the way that the syntax fits smoothly with that used for +universal quantification earlier. - + - -The partial-application restriction + +Restrictions -There is really only one way in which data structures with polymorphic -components might surprise you: you must not partially apply them. -For example, this is illegal: +There are several restrictions on the ways in which existentially-quantified +constructors can be use. + + + + + When pattern matching, each pattern match introduces a new, +distinct, type for each existential type variable. These types cannot +be unified with any other type, nor can they escape from the scope of +the pattern match. For example, these fragments are incorrect: + + - map MkSwizzle [sort, reverse] +f1 (MkFoo a f) = a - - - -The restriction is this: every subexpression of the program must -have a type that has no for-alls, except that in a function -application (f e1…en) the partial applications are not subject to -this rule. The restriction makes type inference feasible. - - -In the illegal example, the sub-expression MkSwizzle has the -polymorphic type (Ord b => [b] -> [b]) -> Swizzle and is not -a sub-expression of an enclosing application. On the other hand, this -expression is OK: - +Here, the type bound by MkFoo "escapes", because a +is the result of f1. One way to see why this is wrong is to +ask what type f1 has: - - map (T1 (\a b -> a)) [1,2,3] + f1 :: Foo -> a -- Weird! - - -even though it involves a partial application of T1, because -the sub-expression T1 (\a b -> a) has type Int -> T -Int. - +What is this "a" in the result type? Clearly we don't mean +this: - - -Type signatures - + + f1 :: forall a. Foo -> a -- Wrong! + - -Once you have data constructors with universally-quantified fields, or -constants such as runST that have rank-2 types, it isn't long -before you discover that you need more! Consider: - - +The original program is just plain wrong. Here's another sort of error + - mkTs f x y = [T1 f x, T1 f y] + f2 (Baz1 a b) (Baz1 p q) = a==q - - -mkTs is a fuction that constructs some values of type -T, using some pieces passed to it. The trouble is that since -f is a function argument, Haskell assumes that it is -monomorphic, so we'll get a type error when applying T1 to -it. This is a rather silly example, but the problem really bites in -practice. Lots of people trip over the fact that you can't make -"wrappers functions" for runST for exactly the same reason. -In short, it is impossible to build abstractions around functions with -rank-2 types. - +It's ok to say a==b or p==q, but +a==q is wrong because it equates the two distinct types arising +from the two Baz1 constructors. + - -The solution is fairly clear. We provide the ability to give a rank-2 -type signature for ordinary functions (not only data -constructors), thus: + + +You can't pattern-match on an existentially quantified +constructor in a let or where group of +bindings. So this is illegal: + - mkTs :: (forall b. b -> b -> b) -> a -> [T a] - mkTs f x y = [T1 f x, T1 f y] + f3 x = a==b where { Baz1 a b = x } - - - -This type signature tells the compiler to attribute f with -the polymorphic type (forall b. b -> b -> b) when type -checking the body of mkTs, so now the application of -T1 is fine. - - -There are two restrictions: - +You can only pattern-match +on an existentially-quantified constructor in a case expression or +in the patterns of a function definition. - +The reason for this restriction is really an implementation one. +Type-checking binding groups is already a nightmare without +existentials complicating the picture. Also an existential pattern +binding at the top level of a module doesn't make sense, because it's +not clear how to prevent the existentially-quantified type "escaping". +So for now, there's a simple-to-state restriction. We'll see how +annoying it is. - + + - You can only define a rank 2 type, specified by the following -grammar: +You can't use existential quantification for newtype +declarations. So this is illegal: -rank2type ::= [forall tyvars .] [context =>] funty -funty ::= ([forall tyvars .] [context =>] ty) -> funty - | ty -ty ::= ...current Haskell monotype syntax... + newtype T = forall a. Ord a => MkT a -Informally, the universal quantification must all be right at the beginning, -or at the top level of a function argument. +Reason: a value of type T must be represented as a pair +of a dictionary for Ord t and a value of type t. +That contradicts the idea that newtype should have no +concrete representation. You can get just the same efficiency and effect +by using data instead of newtype. If there is no +overloading involved, then there is more of a case for allowing +an existentially-quantified newtype, because the data +because the data version does carry an implementation cost, +but single-field existentially quantified constructors aren't much +use. So the simple restriction (no existential stuff on newtype) +stands, unless there are convincing reasons to change it. + - There is a restriction on the definition of a function whose -type signature is a rank-2 type: the polymorphic arguments must be -matched on the left hand side of the "=" sign. You can't -define mkTs like this: + You can't use deriving to define instances of a +data type with existentially quantified data constructors. +Reason: in most cases it would not make sense. For example:# -mkTs :: (forall b. b -> b -> b) -> a -> [T a] -mkTs = \ f x y -> [T1 f x, T1 f y] +data T = forall a. MkT [a] deriving( Eq ) +To derive Eq in the standard way we would need to have equality +between the single component of two MkT constructors: + +instance Eq T where + (MkT a) == (MkT b) = ??? + -The same partial-application rule applies to ordinary functions with -rank-2 types as applied to data constructors. - +But a and b have distinct types, and so can't be compared. +It's just about possible to imagine examples in which the derived instance +would make sense, but it seems altogether simpler simply to prohibit such +declarations. Define your own instances! @@ -1701,381 +1971,399 @@ rank-2 types as applied to data constructors. - + + - -Type synonyms and hoisting +<sect2 id="scoped-type-variables"> +<title>Scoped type variables -GHC also allows you to write a forall in a type synonym, thus: - - type Discard a = forall b. a -> b -> a +A pattern type signature can introduce a scoped type +variable. For example + - f :: Discard a - f x y = x - -However, it is often convenient to use these sort of synonyms at the right hand -end of an arrow, thus: - - type Discard a = forall b. a -> b -> a + - g :: Int -> Discard Int - g x y z = x+y - -Simply expanding the type synonym would give - - g :: Int -> (forall b. Int -> b -> Int) - -but GHC "hoists" the forall to give the isomorphic type - g :: forall b. Int -> Int -> b -> Int +f (xs::[a]) = ys ++ ys + where + ys :: [a] + ys = reverse xs -In general, the rule is this: to determine the type specified by any explicit -user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly -performs the transformation: + + + + +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. + + + + Pattern type signatures are completely orthogonal to ordinary, separate +type signatures. The two can be used independently or together. +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 +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. + + + +What a pattern type signature means + +A type variable brought into scope by a pattern type signature is simply +the name for a type. The restriction they express is that all occurrences +of the same name mean the same type. For example: - type1 -> forall a. type2 -==> - forall a. type1 -> type2 + f :: [Int] -> Int -> Int + f (xs::[a]) (y::a) = (head xs + y) :: a -(In fact, GHC tries to retain as much synonym information as possible for use in -error messages, but that is a usability issue.) This rule applies, of course, whether -or not the forall comes from a synonym. For example, here is another -valid way to write g's type signature: +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: + - g :: Int -> Int -> forall b. b -> Int + 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] - - - + - -Existentially quantified data constructors - + +Scope and implicit quantification -The idea of using existential quantification in data type declarations -was suggested by Laufer (I believe, thought doubtless someone will -correct me), and implemented in Hope+. It's been in Lennart -Augustsson's hbc Haskell compiler for several years, and -proved very useful. Here's the idea. Consider the declaration: + + + + + +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: - data Foo = forall a. MkFoo a (a -> Bool) - | Nil + 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 data type Foo has two constructors with types: - + - - - MkFoo :: forall a. a -> (a -> Bool) -> Foo - Nil :: Foo - +The type variables bound by the pattern may be +mentioned in ordinary type signatures or pattern +type signatures anywhere within their scope. + + -Notice that the type variable a in the type of MkFoo -does not appear in the data type itself, which is plain Foo. -For example, the following expression is fine: + 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: - [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] + 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. - -Here, (MkFoo 3 even) packages an integer with a function -even that maps an integer to Bool; and MkFoo 'c' -isUpper packages a character with a compatible function. These -two things are each of type Foo and can be put in a list. + + -What can we do with a value of type Foo?. In particular, -what happens when we pattern-match on MkFoo? +The pattern type signature is a monotype: - + + +A pattern type signature cannot contain any explicit forall quantification. + - - f (MkFoo val fn) = ??? - + +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). + - -Since all we know about val and fn is that they -are compatible, the only (useful) thing we can do with them is to -apply fn to val to get a boolean. For example: - + + + + +The type variables in the head of a class or instance declaration +scope over the methods defined in the where part. For example: + + - f :: Foo -> Bool - f (MkFoo val fn) = fn val + class C a where + op :: [a] -> a + + op xs = let ys::[a] + ys = reverse xs + in + head ys - - -What this allows us to do is to package heterogenous values -together with a bunch of functions that manipulate them, and then treat -that collection of packages in a uniform manner. You can express -quite a bit of object-oriented-like programming this way. +(Not implemented in Hugs yet, Dec 98). + - -Why existential? - + - -What has this to do with existential quantification? -Simply that MkFoo has the (nearly) isomorphic type - - - - MkFoo :: (exists a . (a, a -> Bool)) -> Foo - + - + +Result type signatures -But Haskell programmers can safely think of the ordinary -universally quantified type given above, thereby avoiding -adding a new existential quantification construct. - - - - -Type classes + + -An easy extension (implemented in hbc) is to allow -arbitrary contexts before the constructor. For example: - + The result type of a function can be given a signature, +thus: - -data Baz = forall a. Eq a => Baz1 a a - | forall b. Show b => Baz2 b (b -> b) + f (x::a) :: [a] = [x,x,x] - - -The two constructors have the types you'd expect: - +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: - -Baz1 :: forall a. Eq a => a -> a -> Baz -Baz2 :: forall b. Show b => b -> (b -> b) -> Baz + f :: Int -> [a] -> [a] + f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x) + in \xs -> map g (reverse xs `zip` xs) - - -But when pattern matching on Baz1 the matched values can be compared -for equality, and when pattern matching on Baz2 the first matched -value can be converted to a string (as well as applying the function to it). -So this program is legal: + - - - - f :: Baz -> String - f (Baz1 p q) | p == q = "Yes" - | otherwise = "No" - f (Baz1 v fn) = show (fn v) - - - + - -Operationally, in a dictionary-passing implementation, the -constructors Baz1 and Baz2 must store the -dictionaries for Eq and Show respectively, and -extract it on pattern matching. -Notice the way that the syntax fits smoothly with that used for -universal quantification earlier. +Result type signatures are not yet implemented in Hugs. - - - -Restrictions + - -There are several restrictions on the ways in which existentially-quantified -constructors can be use. - + +Where a pattern type signature can occur - +A pattern type signature can occur in any pattern. For example: - + - When pattern matching, each pattern match introduces a new, -distinct, type for each existential type variable. These types cannot -be unified with any other type, nor can they escape from the scope of -the pattern match. For example, these fragments are incorrect: - - - -f1 (MkFoo a f) = a - - - -Here, the type bound by MkFoo "escapes", because a -is the result of f1. One way to see why this is wrong is to -ask what type f1 has: +A pattern type signature can be on an arbitrary sub-pattern, not +ust on a variable: - f1 :: Foo -> a -- Weird! + f ((x,y)::(a,b)) = (y,x) :: (b,a) -What is this "a" in the result type? Clearly we don't mean -this: + + + + + Pattern type signatures, including the result part, can be used +in lambda abstractions: - f1 :: forall a. Foo -> a -- Wrong! + (\ (x::a, y) :: a -> x) + + + - -The original program is just plain wrong. Here's another sort of error + + Pattern type signatures, including the result part, can be used +in case expressions: - f2 (Baz1 a b) (Baz1 p q) = a==q + case e of { (x::a, y) :: a -> x } - -It's ok to say a==b or p==q, but -a==q is wrong because it equates the two distinct types arising -from the two Baz1 constructors. - - - + -You can't pattern-match on an existentially quantified -constructor in a let or where group of -bindings. So this is illegal: +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: - f3 x = a==b where { Baz1 a b = x } + \ x :: a -> b -> x -You can only pattern-match -on an existentially-quantified constructor in a case expression or -in the patterns of a function definition. - -The reason for this restriction is really an implementation one. -Type-checking binding groups is already a nightmare without -existentials complicating the picture. Also an existential pattern -binding at the top level of a module doesn't make sense, because it's -not clear how to prevent the existentially-quantified type "escaping". -So for now, there's a simple-to-state restriction. We'll see how -annoying it is. - + -You can't use existential quantification for newtype -declarations. So this is illegal: + Pattern type signatures can bind existential type variables. +For example: - newtype T = forall a. Ord a => MkT a - - + data T = forall a. MkT [a] -Reason: a value of type T must be represented as a pair -of a dictionary for Ord t and a value of type t. -That contradicts the idea that newtype should have no -concrete representation. You can get just the same efficiency and effect -by using data instead of newtype. If there is no -overloading involved, then there is more of a case for allowing -an existentially-quantified newtype, because the data -because the data version does carry an implementation cost, -but single-field existentially quantified constructors aren't much -use. So the simple restriction (no existential stuff on newtype) -stands, unless there are convincing reasons to change it. + f :: T -> T + f (MkT [t::a]) = MkT t3 + where + t3::[a] = [t,t,t] + + + - You can't use deriving to define instances of a -data type with existentially quantified data constructors. - -Reason: in most cases it would not make sense. For example:# +Pattern type signatures +can be used in pattern bindings: -data T = forall a. MkT [a] deriving( Eq ) + 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 -To derive Eq in the standard way we would need to have equality -between the single component of two MkT constructors: - +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 -instance Eq T where - (MkT a) == (MkT b) = ??? + f4 :: b->b + f4 = \x -> x +makes a polymorphic function, but b is not in scope anywhere +in f4's scope. -But a and b have distinct types, and so can't be compared. -It's just about possible to imagine examples in which the derived instance -would make sense, but it seems altogether simpler simply to prohibit such -declarations. Define your own instances! - - + + + + + + Assertions @@ -2138,410 +2426,442 @@ assert pred val ==> assertError "Main.hs|15" pred val <para> The rewrite is only performed by the compiler when it spots -applications of <function>Exception.assert</function>, so you can still define and -use your own versions of <function>assert</function>, should you so wish. If not, -import <literal>Exception</literal> to make use <function>assert</function> in your code. +applications of <function>Control.Exception.assert</function>, so you +can still define and use your own versions of +<function>assert</function>, should you so wish. If not, import +<literal>Control.Exception</literal> to make use +<function>assert</function> in your code. </para> <para> To have the compiler ignore uses of assert, use the compiler option -<option>-fignore-asserts</option>. <indexterm><primary>-fignore-asserts option</primary></indexterm> That is, -expressions of the form <literal>assert pred e</literal> will be rewritten to <literal>e</literal>. +<option>-fignore-asserts</option>. <indexterm><primary>-fignore-asserts +option</primary></indexterm> That is, expressions of the form +<literal>assert pred e</literal> will be rewritten to +<literal>e</literal>. </para> <para> Assertion failures can be caught, see the documentation for the -<literal>Exception</literal> library (<xref linkend="sec-Exception">) -for the details. +<literal>Control.Exception</literal> library for the details. </para> </sect1> -<sect1 id="scoped-type-variables"> -<title>Scoped Type Variables - - - -A pattern type signature can introduce a scoped type -variable. For example - - + +Syntactic extensions - -f (xs::[a]) = ys ++ ys - where - ys :: [a] - ys = reverse xs - + - + + Hierarchical Modules - -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. - + GHC supports a small extension to the syntax of module + names: a module name is allowed to contain a dot + ‘.’. This is also known as the + “hierarchical module namespace” extension, because + it extends the normally flat Haskell module namespace into a + more flexible hierarchy of modules. - - Pattern type signatures are completely orthogonal to ordinary, separate -type signatures. The two can be used independently or together. -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 -a type for ys; a major benefit of scoped type variables is that -it becomes possible to do so. - + This extension has very little impact on the language + itself; modules names are always fully + qualified, so you can just think of the fully qualified module + name as the module name. In particular, this + means that the full module name must be given after the + module keyword at the beginning of the + module; for example, the module A.B.C must + begin - -Scoped type variables are implemented in both GHC and Hugs. Where the -implementations differ from the specification below, those differences -are noted. - +module A.B.C - -So much for the basic idea. Here are the details. - - -What a pattern type signature means - -A type variable brought into scope by a pattern type signature is simply -the name for a type. The restriction they express 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: + It is a common strategy to use the as + keyword to save some typing when using qualified names with + hierarchical modules. For example: - 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] +import qualified Control.Monad.ST.Strict as ST - - - -Scope and implicit quantification - - + Hierarchical modules have an impact on the way that GHC + searches for files. For a description, see . - - + GHC comes with a large collection of libraries arranged + hierarchically; see the accompanying library documentation. + There is an ongoing project to create and maintain a stable set + of core libraries used by several Haskell + compilers, and the libraries that GHC comes with represent the + current status of that project. For more details, see Haskell + Libraries. - -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 variables thus brought into scope may be mentioned -in ordinary type signatures or pattern type signatures anywhere within -their scope. + - - + +Pattern guards - - In ordinary type signatures, any type variable mentioned in the -signature that is in scope is not universally quantified. - +Pattern guards (Glasgow extension) +The discussion that follows is an abbreviated version of Simon Peyton Jones's original proposal. (Note that the proposal was written before pattern guards were implemented, so refers to them as unimplemented.) - - - - Ordinary type signatures do not bring any new type variables -into scope (except in the type signature itself!). So this is illegal: +Suppose we have an abstract data type of finite maps, with a +lookup operation: - f :: a -> a - f x = x::a +lookup :: FiniteMap -> Int -> Maybe Int -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. - - - - - - - There is no implicit universal quantification on pattern type -signatures, nor may one write an explicit forall type in a pattern -type signature. The pattern type signature is a monotype. - +The lookup returns Nothing if the supplied key is not in the domain of the mapping, and (Just v) otherwise, +where v is the value that the key maps to. Now consider the following definition: - - - - - -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 +clunky env var1 var2 | ok1 && ok2 = val1 + val2 +| otherwise = var1 + var2 +where + m1 = lookup env var1 + m2 = lookup env var2 + ok1 = maybeToBool m1 + ok2 = maybeToBool m2 + val1 = expectJust m1 + val2 = expectJust m2 - -(Not implemented in Hugs yet, Dec 98). - - - - - - - - - - -Result type signatures - - - - - - - The result type of a function can be given a signature, -thus: - +The auxiliary functions are + - f (x::a) :: [a] = [x,x,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: - +maybeToBool :: Maybe a -> Bool +maybeToBool (Just x) = True +maybeToBool Nothing = False - - f :: Int -> [a] -> [a] - f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x) - in \xs -> map g (reverse xs `zip` xs) +expectJust :: Maybe a -> a +expectJust (Just x) = x +expectJust Nothing = error "Unexpected Nothing" - - - - - - + +What is clunky doing? The guard ok1 && +ok2 checks that both lookups succeed, using +maybeToBool to convert the Maybe +types to booleans. The (lazily evaluated) expectJust +calls extract the values from the results of the lookups, and binds the +returned values to val1 and val2 +respectively. If either lookup fails, then clunky takes the +otherwise case and returns the sum of its arguments. -Result type signatures are not yet implemented in Hugs. +This is certainly legal Haskell, but it is a tremendously verbose and +un-obvious way to achieve the desired effect. Arguably, a more direct way +to write clunky would be to use case expressions: - - - -Where a pattern type signature can occur + +clunky env var1 var1 = case lookup env var1 of + Nothing -> fail + Just val1 -> case lookup env var2 of + Nothing -> fail + Just val2 -> val1 + val2 +where + fail = val1 + val2 + -A pattern type signature can occur in any pattern, but there -are restrictions on pattern bindings: - +This is a bit shorter, but hardly better. Of course, we can rewrite any set +of pattern-matching, guarded equations as case expressions; that is +precisely what the compiler does when compiling equations! The reason that +Haskell provides guarded equations is because they allow us to write down +the cases we want to consider, one at a time, independently of each other. +This structure is hidden in the case version. Two of the right-hand sides +are really the same (fail), and the whole expression +tends to become more and more indented. + - -A pattern type signature can be on an arbitrary sub-pattern, not -ust on a variable: - +Here is how I would write clunky: + - f ((x,y)::(a,b)) = (y,x) :: (b,a) +clunky env var1 var1 + | Just val1 <- lookup env var1 + , Just val2 <- lookup env var2 + = val1 + val2 +...other equations for clunky... - + +The semantics should be clear enough. The qualifers are matched in order. +For a <- qualifier, which I call a pattern guard, the +right hand side is evaluated and matched against the pattern on the left. +If the match fails then the whole guard fails and the next equation is +tried. If it succeeds, then the appropriate binding takes place, and the +next qualifier is matched, in the augmented environment. Unlike list +comprehensions, however, the type of the expression to the right of the +<- is the same as the type of the pattern to its +left. The bindings introduced by pattern guards scope over all the +remaining guard qualifiers, and over the right hand side of the equation. - - - Pattern type signatures, including the result part, can be used -in lambda abstractions: +Just as with list comprehensions, boolean expressions can be freely mixed +with among the pattern guards. For example: + - (\ (x::a, y) :: a -> x) +f x | [y] <- x + , y > 3 + , Just z <- h y + = ... - - - - Pattern type signatures, including the result part, can be used -in case expressions: +Haskell's current guards therefore emerge as a special case, in which the +qualifier list has just one element, a boolean expression. + + + + + +The recursive do-notation + + The recursive do-notation (also known as mdo-notation) is implemented as described in +"A recursive do for Haskell", +Levent Erkok, John Launchbury", +Haskell Workshop 2002, pages: 29-37. Pittsburgh, Pennsylvania. + + +The do-notation of Haskell does not allow recursive bindings, +that is, the variables bound in a do-expression are visible only in the textually following +code block. Compare this to a let-expression, where bound variables are visible in the entire binding +group. It turns out that several applications can benefit from recursive bindings in +the do-notation, and this extension provides the necessary syntactic support. + + +Here is a simple (yet contrived) example: + - case e of { (x::a, y) :: a -> x } +justOnes = mdo xs <- Just (1:xs) + return xs - + +As you can guess justOnes will evaluate to Just [1,1,1,.... - - -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: - - +The MonadFix library introduces the MonadFix class. It's definition is: + - \ x :: a -> b -> x +class Monad m => MonadFix m where + mfix :: (a -> m a) -> m a + +The function mfix +dictates how the required recursion operation should be performed. If recursive bindings are required for a monad, +then that monad must be declared an instance of the MonadFix class. +For details, see the above mentioned reference. + + +The MonadFix library automatically declares List, Maybe, IO, and +state monads (both lazy and strict) as instances of the MonadFix class. + + +There are three important points in using the recursive-do notation: + + +The recursive version of the do-notation uses the keyword mdo (rather +than do). + + +If you want to declare an instance of the MonadFix class for one of +your own monads, or you need to refer to the class name MonadFix in any other way (for instance in +writing a type constraint), then your program should import Control.Monad.MonadFix. +Otherwise, you don't need to import any special libraries to use the mdo-notation. That is, +as long as you only use the predefined instances mentioned above, the mdo-notation will +be automatically available. (Note: This differs from the Hugs implementation, where +MonadFix should always be imported.) + + +As with other extensions, ghc should be given the flag -fglasgow-exts + + - - + +Historical note: The originial implementation of the mdo-notation, and most +of the existing documents, use the names +MonadRec for the class, and +Control.Monad.MonadRec for the library. These names +are no longer supported. + - Pattern type signatures can bind existential type variables. -For example: +The web page: http://www.cse.ogi.edu/PacSoft/projects/rmb +contains up to date information on recursive monadic bindings. + + - - data T = forall a. MkT [a] + - f :: T -> T - f (MkT [t::a]) = MkT t3 - where - t3::[a] = [t,t,t] - + + Parallel List Comprehensions + list comprehensionsparallel + + parallel list comprehensions + + Parallel list comprehensions are a natural extension to list + comprehensions. List comprehensions can be thought of as a nice + syntax for writing maps and filters. Parallel comprehensions + extend this to include the zipWith family. - - + A parallel list comprehension has multiple independent + branches of qualifier lists, each separated by a `|' symbol. For + example, the following zips together two lists: + + [ (x, y) | x <- xs | y <- ys ] + - + The behavior of parallel list comprehensions follows that of + zip, in that the resulting list will have the same length as the + shortest branch. - -Pattern type signatures that bind new type variables -may not be used in pattern bindings at all. -So this is illegal: + We can define parallel list comprehensions by translation to + regular comprehensions. Here's the basic idea: + Given a parallel comprehension of the form: - f x = let (y, z::a) = x in ... + [ e | p1 <- e11, p2 <- e12, ... + | q1 <- e21, q2 <- e22, ... + ... + ] - -But these are OK, because they do not bind fresh type variables: - + This will be translated to: - f1 x = let (y, z::Int) = x in ... - f2 (x::(Int,a)) = let (y, z::a) = x in ... + [ e | ((p1,p2), (q1,q2), ...) <- zipN [(p1,p2) | p1 <- e11, p2 <- e12, ...] + [(q1,q2) | q1 <- e21, q2 <- e22, ...] + ... + ] + where `zipN' is the appropriate zip for the given number of + branches. -However a single variable is considered a degenerate function binding, -rather than a degerate pattern binding, so this is permitted, even -though it binds a type variable: - + - - f :: (b->b) = \(x::b) -> x - + +Rebindable syntax - - + GHC allows most kinds of built-in syntax to be rebound by + the user, to facilitate replacing the Prelude + with a home-grown version, for example. - + You may want to define your own numeric class + hierarchy. It completely defeats that purpose if the + literal "1" means "Prelude.fromInteger + 1", which is what the Haskell Report specifies. + So the flag causes + the following pieces of built-in syntax to refer to + whatever is in scope, not the Prelude + versions: -Such degnerate function bindings do not fall under the monomorphism -restriction. Thus: - + + + Integer and fractional literals mean + "fromInteger 1" and + "fromRational 3.2", not the + Prelude-qualified versions; both in expressions and in + patterns. + However, the standard Prelude Eq class + is still used for the equality test necessary for literal patterns. + - + + Negation (e.g. "- (f x)") + means "negate (f x)" (not + Prelude.negate). + - - g :: a -> a -> Bool = \x y. x==y - + + In an n+k pattern, the standard Prelude + Ord class is still used for comparison, + but the necessary subtraction uses whatever + "(-)" is in scope (not + "Prelude.(-)"). + - + + "Do" notation is translated using whatever + functions (>>=), + (>>), fail, and + return, are in scope (not the Prelude + versions). List comprehensions, and parallel array + comprehensions, are unaffected. + - -Here g has type forall a. Eq a => a -> a -> Bool, just as if -g had a separate type signature. Lacking a type signature, g -would get a monomorphic type. - + Be warned: this is an experimental facility, with fewer checks than + usual. In particular, it is essential that the functions GHC finds in scope + must have the appropriate types, namely: + + fromInteger :: forall a. (...) => Integer -> a + fromRational :: forall a. (...) => Rational -> a + negate :: forall a. (...) => a -> a + (-) :: forall a. (...) => a -> a -> a + (>>=) :: forall m a. (...) => m a -> (a -> m b) -> m b + (>>) :: forall m a. (...) => m a -> m b -> m b + return :: forall m a. (...) => a -> m a + fail :: forall m a. (...) => String -> m a + + (The (...) part can be any context including the empty context; that part + is up to you.) + If the functions don't have the right type, very peculiar things may + happen. Use -dcore-lint to + typecheck the desugared program. If Core Lint is happy you should be all right. + + - + + Pragmas - -Pragmas - + pragma - -GHC supports several pragmas, or instructions to the compiler placed -in the source code. Pragmas don't affect the meaning of the program, -but they might affect the efficiency of the generated code. - + GHC supports several pragmas, or instructions to the + compiler placed in the source code. Pragmas don't normally affect + the meaning of the program, but they might affect the efficiency + of the generated code. + + Pragmas all take the form + +{-# word ... #-} + + where word indicates the type of + pragma, and is followed optionally by information specific to that + type of pragma. Case is ignored in + word. The various values for + word that GHC understands are described + in the following sections; any pragma encountered with an + unrecognised word is (silently) + ignored. INLINE pragma @@ -2613,17 +2933,23 @@ For example, in GHC's own <literal>UniqueSupply</literal> monad code, we have: <title>NOINLINE pragma - NOINLINE pragma -pragma, NOINLINE - +pragmaNOINLINE +NOTINLINE pragma +pragmaNOTINLINE -The NOINLINE pragma does exactly what you'd expect: it stops the -named function from being inlined by the compiler. You shouldn't ever -need to do this, unless you're very cautious about code size. +The NOINLINE pragma does exactly what you'd expect: +it stops the named function from being inlined by the compiler. You +shouldn't ever need to do this, unless you're very cautious about code +size. +NOTINLINE is a synonym for +NOINLINE (NOTINLINE is specified +by Haskell 98 as the standard way to disable inlining, so it should be +used if you want your code to be portable). + @@ -2701,12 +3027,17 @@ i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly Same idea, except for instance declarations. For example: -instance (Eq a) => Eq (Foo a) where { ... usual stuff ... } - -{-# SPECIALIZE instance Eq (Foo [(Int, Bar)] #-} +instance (Eq a) => Eq (Foo a) where { + {-# SPECIALIZE instance Eq (Foo [(Int, Bar)]) #-} + ... usual stuff ... + } - -Compatible with HBC, by the way. +The pragma must occur inside the where part +of the instance declaration. + + +Compatible with HBC, by the way, except perhaps in the placement +of the pragma. @@ -2791,6 +3122,8 @@ GHC will print the specified message. + + Rewrite rules @@ -3094,14 +3427,14 @@ The following are good producers: <function>++</function> </para> </listitem> -<listitem> +<listitem> <para> <function>map</function> </para> </listitem> -<listitem> +<listitem> <para> <function>filter</function> </para> @@ -3151,8 +3484,14 @@ The following are good consumers: <function>++</function> (on its first argument) </para> </listitem> + <listitem> +<para> + <function>foldr</function> +</para> +</listitem> +<listitem> <para> <function>map</function> </para> @@ -3346,6 +3685,9 @@ program even if fusion doesn't happen. More rules in <filename>PrelList.lhs</fi <sect1 id="generic-classes"> <title>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. @@ -3501,10 +3843,10 @@ So this too is illegal: class Foo a where op1 :: a -> Bool - op {| a :*: b |} (Inl x) = True + op1 {| a :*: b |} (x :*: y) = True op2 :: a -> Bool - op {| p :*: q |} (Inr y) = False + op2 {| p :*: q |} (x :*: y) = False (The reason for this restriction is that we gather all the equations for a particular type consructor into a single generic instance declaration.) @@ -3596,6 +3938,182 @@ Just to finish with, here's another example I rather like: + +Generalised derived instances for newtypes + + +When you define an abstract type using newtype, you may want +the new type to inherit some instances from its representation. In +Haskell 98, you can inherit instances of Eq, Ord, +Enum and Bounded by deriving them, but for any +other classes you have to write an explicit instance declaration. For +example, if you define + + + newtype Dollars = Dollars Int + + +and you want to use arithmetic on Dollars, you have to +explicitly define an instance of Num: + + + instance Num Dollars where + Dollars a + Dollars b = Dollars (a+b) + ... + +All the instance does is apply and remove the newtype +constructor. It is particularly galling that, since the constructor +doesn't appear at run-time, this instance declaration defines a +dictionary which is wholly equivalent to the Int +dictionary, only slower! + + + Generalising the deriving clause + +GHC now permits such instances to be derived instead, so one can write + + newtype Dollars = Dollars Int deriving (Eq,Show,Num) + + +and the implementation uses the same Num dictionary +for Dollars as for Int. Notionally, the compiler +derives an instance declaration of the form + + + instance Num Int => Num Dollars + + +which just adds or removes the newtype constructor according to the type. + + + +We can also derive instances of constructor classes in a similar +way. For example, suppose we have implemented state and failure monad +transformers, such that + + + instance Monad m => Monad (State s m) + instance Monad m => Monad (Failure m) + +In Haskell 98, we can define a parsing monad by + + type Parser tok m a = State [tok] (Failure m) a + + +which is automatically a monad thanks to the instance declarations +above. With the extension, we can make the parser type abstract, +without needing to write an instance of class Monad, via + + + newtype Parser tok m a = Parser (State [tok] (Failure m) a) + deriving Monad + +In this case the derived instance declaration is of the form + + instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) + + +Notice that, since Monad is a constructor class, the +instance is a partial application of the new type, not the +entire left hand side. We can imagine that the type declaration is +``eta-converted'' to generate the context of the instance +declaration. + + + +We can even derive instances of multi-parameter classes, provided the +newtype is the last class parameter. In this case, a ``partial +application'' of the class appears in the deriving +clause. For example, given the class + + + class StateMonad s m | m -> s where ... + instance Monad m => StateMonad s (State s m) where ... + +then we can derive an instance of StateMonad for Parsers by + + newtype Parser tok m a = Parser (State [tok] (Failure m) a) + deriving (Monad, StateMonad [tok]) + + +The derived instance is obtained by completing the application of the +class to the new type: + + + instance StateMonad [tok] (State [tok] (Failure m)) => + StateMonad [tok] (Parser tok m) + + + + +As a result of this extension, all derived instances in newtype +declarations are treated uniformly (and implemented just by reusing +the dictionary for the representation type), except +Show and Read, which really behave differently for +the newtype and its representation. + + + + A more precise specification + +Derived instance declarations are constructed as follows. Consider the +declaration (after expansion of any type synonyms) + + + newtype T v1...vn = T' (S t1...tk vk+1...vn) deriving (c1...cm) + + +where S is a type constructor, t1...tk are +types, +vk+1...vn are type variables which do not occur in any of +the ti, and the ci are partial applications of +classes of the form C t1'...tj'. The derived instance +declarations are, for each ci, + + + instance ci (S t1...tk vk+1...v) => ci (T v1...vp) + +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 + +Here we cannot derive the instance + + instance Monad (State s m) => Monad (NonMonad m) + + +because the type variable s occurs in State s m, +and so cannot be "eta-converted" away. It is a good thing that this +deriving clause is rejected, because NonMonad m is +not, in fact, a monad --- for the same reason. Try defining +>>= with the correct type: you won't be able to. + + + +Notice also that the order of class parameters becomes +important, since we can only derive instances for the last one. If the +StateMonad class above were instead defined as + + + class StateMonad m s | m -> s where ... + + +then we would not have been able to derive an instance for the +Parser type above. We hypothesise that multi-parameter +classes usually have one "main" parameter for which deriving new +instances is most interesting. + + + + + + +