X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fdocs%2Fusers_guide%2Fglasgow_exts.sgml;h=025a92387e1e38ef3b2b409def984e1a02f9689c;hb=9a9feb62db17daf7f2566395f719c2aecec5feb0;hp=4d1ee1736a5aebd5353e6aea3bf2429f1c8df481;hpb=2c5ca121806c7ee3d81b728397e6e74ff2909d9d;p=ghc-hetmet.git diff --git a/ghc/docs/users_guide/glasgow_exts.sgml b/ghc/docs/users_guide/glasgow_exts.sgml index 4d1ee17..025a923 100644 --- a/ghc/docs/users_guide/glasgow_exts.sgml +++ b/ghc/docs/users_guide/glasgow_exts.sgml @@ -65,18 +65,6 @@ with GHC. - : - - - This option enables the deprecated with - keyword for implicit parameters; it is merely provided for backwards - compatibility. - It is independent of the - flag. - - - - : @@ -110,6 +98,15 @@ with GHC. + + + + See . Independent of + . + + + + @@ -118,34 +115,51 @@ with GHC. - - - - -fno-implicit-prelude - option GHC normally imports - Prelude.hi files for you. If you'd - rather it didn't, then give it a - option. The idea - is that you can then import a Prelude of your own. (But - don't call it Prelude; the Haskell - module namespace is flat, and you must not conflict with - any Prelude module.) - - 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] - still means Prelude.[] Int; tuples - continue to refer to the standard Prelude tuples; the - translation for list comprehensions continues to use - Prelude.map etc. - - However, does - change the handling of certain built-in syntax: see - . + + + + -fno-implicit-prelude + option GHC normally imports + Prelude.hi files for you. If you'd + rather it didn't, then give it a + option. The idea is + that you can then import a Prelude of your own. (But don't + call it Prelude; the Haskell module + namespace is flat, and you must not conflict with any + Prelude module.) + + 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] + still means Prelude.[] Int; tuples + continue to refer to the standard Prelude tuples; the + translation for list comprehensions continues to use + Prelude.map etc. + + However, does + change the handling of certain built-in syntax: see . + + - - + + + + Enables Template Haskell (see ). Currently also implied by + . + + + + + + + Enables implicit parameters (see ). Currently also implied by + . + + @@ -406,9 +420,9 @@ tuples to avoid unnecessary allocation during sequences of operations. import qualified Control.Monad.ST.Strict as ST - Hierarchical modules have an impact on the way that GHC - searches for files. For a description, see . + For details on how GHC searches for source and interface + files in the presence of hierarchical modules, see . GHC comes with a large collection of libraries arranged hierarchically; see the accompanying library documentation. @@ -635,32 +649,6 @@ This name is not supported by GHC. - Infix type constructors - -GHC supports infix type constructors, much as it supports infix data constructors. For example: - - infixl 5 :+: - - data a :+: b = Inl a | Inr b - - f :: a `Either` b -> a :+: b - f (Left x) = Inl x - - -The lexical -syntax of an infix type constructor is just like that of an infix data constructor: either -it's an operator beginning with ":", or it is an ordinary (alphabetic) type constructor enclosed in -back-quotes. - - -When you give a fixity declaration, the fixity applies to both the data constructor and the -type constructor with the specified name. You cannot give different fixities to the type constructor T -and the data constructor T. - - - - - @@ -791,7 +779,11 @@ and the data constructor T. Type system extensions - + + +Data types and type synonyms + + Data types with no constructors With the flag, GHC lets you declare @@ -809,9 +801,9 @@ not * then an explicit kind annotation must be used Such data types have only one value, namely bottom. Nevertheless, they can be useful when defining "phantom types". - + - + Infix type constructors @@ -862,651 +854,673 @@ like expressions. More specifically: - + - -Explicitly-kinded quantification + +Liberalised type synonyms -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. - - -GHC now instead allows you to specify the kind of a type variable directly, wherever -a type variable is explicitly bound. Namely: +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: -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 - - - + You can write a forall (including overloading) +in a type synonym, thus: + + type Discard a = forall b. Show b => a -> b -> (a, String) - -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. - + f :: Discard a + f x y = (x, show y) - -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. + 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 #) - -Class method types - - -Haskell 98 prohibits class method types to mention constraints on the -class type variable, thus: + h :: Int -> Pr + h x = (# x, x #) + + + + +You can apply a type synonym to a forall type: - class Seq s a where - fromList :: [a] -> s a - elem :: Eq a => a -> s a -> Bool + type Foo a = a -> a -> Bool + + f :: Foo (forall b. b->b) -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). +After expanding the synonym, f has the legal (in GHC) type: + + f :: (forall b. b->b) -> (forall b. b->b) -> Bool + + + + +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] + + + + + -With the GHC lifts this restriction. +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: + + +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. + - - -Multi-parameter type classes +<sect3 id="existential-quantification"> +<title>Existentially quantified data constructors -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). +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: -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. - + + data Foo = forall a. MkFoo a (a -> Bool) + | Nil + - -Types + -There are the following restrictions on the form of a qualified -type: +The data type Foo has two constructors with types: - forall tv1..tvn (c1, ...,cn) => type + MkFoo :: forall a. a -> (a -> Bool) -> Foo + Nil :: Foo -(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 ). +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: - - + + [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] + + + - Each universally quantified type variable -tvi must be mentioned (i.e. appear free) in type. +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. + -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: + +What can we do with a value of type Foo?. In particular, +what happens when we pattern-match on MkFoo? + + - forall a. Eq a => Int + f (MkFoo val fn) = ??? - -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. - - - - 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: +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: + + - forall a. C a b => burble + f :: Foo -> Bool + f (MkFoo val fn) = fn val + -The next type is illegal because the constraint Eq b does not -mention a: - - - - forall a. Eq b => burble - - + +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. + -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. + +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 + -These restrictions apply to all types, whether declared in a type signature -or inferred. +But Haskell programmers can safely think of the ordinary +universally quantified type given above, thereby avoiding +adding a new existential quantification construct. + + + +Type classes + -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 +An easy extension (implemented in hbc) is to allow +arbitrary contexts before the constructor. For example: - f :: Eq (m a) => [m a] -> [m a] - g :: Eq [a] => ... +data Baz = forall a. Eq a => Baz1 a a + | forall b. Show b => Baz2 b (b -> b) -This choice recovers principal types, a property that Haskell 1.4 does not have. +The two constructors have the types you'd expect: - - - -Class declarations - - - + +Baz1 :: forall a. Eq a => a -> a -> Baz +Baz2 :: forall b. Show b => b -> (b -> b) -> Baz + + + - Multi-parameter type classes are permitted. For example: +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: + + - class Collection c a where - union :: c a -> c a -> c a - ...etc. + f :: Baz -> String + f (Baz1 p q) | p == q = "Yes" + | otherwise = "No" + f (Baz2 v fn) = show (fn v) - - - - - The class hierarchy must be acyclic. However, the definition -of "acyclic" involves only the superclass relationships. For example, -this is OK: +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. + - - class C a where { - op :: D b => a -> b -> b - } + - class C a => D a where { ... } - + +Restrictions + +There are several restrictions on the ways in which existentially-quantified +constructors can be use. + -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: + 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: - class Functor (m k) => FiniteMap m k where - ... - - class (Monad m, Monad (t m)) => Transform t m where - lift :: m a -> (t m) a +f1 (MkFoo a f) = a - - - - - - In the signature of a class operation, every constraint -must mention at least one type variable that is not a class type -variable. - -Thus: +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: - class Collection c a where - mapC :: Collection c b => (a->b) -> c a -> c b + f1 :: Foo -> a -- Weird! -is OK because the constraint (Collection a b) mentions -b, even though it also mentions the class variable -a. On the other hand: +What is this "a" in the result type? Clearly we don't mean +this: - class C a where - op :: Eq a => (a,b) -> (a,b) + f1 :: forall a. Foo -> a -- Wrong! -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 original program is just plain wrong. Here's another sort of error - class Eq a => C a where - op ::(a,b) -> (a,b) + f2 (Baz1 a b) (Baz1 p q) = a==q -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. +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 type of each class operation must mention all of -the class type variables. For example: +You can't pattern-match on an existentially quantified +constructor in a let or where group of +bindings. So this is illegal: - class Coll s a where - empty :: s - insert :: s -> a -> s + f3 x = a==b where { Baz1 a b = x } +Instead, use a case expression: -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. + + f3 x = case x of Baz1 a b -> a==b + -Sometimes, offending class declarations exhibit misunderstandings. For -example, Coll might be rewritten +In general, 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: - class Coll s a where - empty :: s a - insert :: s a -> a -> s a + newtype T = forall a. Ord a => MkT a -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: +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 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. - - class CollE s where - empty :: s + + + - class CollE s => Coll s a where - insert :: s -> a -> s + + 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:# + + +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) = ??? + +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! - + + - -Instance declarations + - + + +Class declarations + + +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). + + +There are the following constraints on class declarations: - Instance declarations may not overlap. The two instance -declarations + Multi-parameter type classes are permitted. For example: - instance context1 => C type1 where ... - instance context2 => C type2 where ... + class Collection c a where + union :: c a -> c a -> c a + ...etc. -"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. - - - - - 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 - - - - - make it clear which instance decl to use -(pick the most specific one that matches) - - - - + The class hierarchy must be acyclic. However, the definition +of "acyclic" involves only the superclass relationships. For example, +this is OK: - - 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: - - instance C (Int,a) where ... - instance C (a,Bool) where ... - -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 + class C a where { + op :: D b => a -> b -> b + } + + class C a => D a where { ... } -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.) + + +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 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: + 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 a where ... - - instance D (Int, Int) where ... + class Functor (m k) => FiniteMap m k where + ... - instance E [[a]] where ... + class (Monad m, Monad (t m)) => Transform t m where + lift :: m a -> (t m) a -Note that instance heads may contain repeated type variables. -For example, this is OK: - - - - instance Stateful (ST s) (MutVar s) where ... - + + + -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: + + All of the class type variables must be reachable (in the sense +mentioned in ) +from the free varibles of each method type +. For example: - instance C a => C a where ... + class Coll s a where + empty :: s + insert :: s -> a -> s -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: +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 - instance C a where - op = ... -- Default + class Coll s a where + empty :: s a + insert :: s a -> a -> s a -Second, sometimes you might want to use the following to get the -effect of a "class synonym": +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 (C1 a, C2 a, C3 a) => C a where { } + class CollE s where + empty :: s - instance (C1 a, C2 a, C3 a) => C a where { } + class CollE s => Coll s a where + insert :: s -> a -> s -This allows you to write shorter signatures: + + + + + +Class method types + +Haskell 98 prohibits class method types to mention constraints on the +class type variable, thus: - f :: C a => ... + 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). + + +With the GHC lifts this restriction. + + -instead of + + +Type signatures +The context of a type signature + +Unlike Haskell 98, constraints in types do not have to be of +the form (class type-variable) or +(class (type-variable type-variable ...)). Thus, +these type signatures are perfectly OK - f :: (C1 a, C2 a, C3 a) => ... + g :: Eq [a] => ... + g :: Ord (T 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. - - - - - 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: - +GHC imposes the following restrictions on the constraints in a type signature. +Consider the type: - type Point = (Int,Int) - instance C Point where ... - instance C [Point] where ... + forall tv1..tvn (c1, ...,cn) => type +(Here, we write the "foralls" explicitly, although the Haskell source +language omits them; in Haskell 98, 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 ). + -is legal. However, if you added - + - - instance C (Int,Int) where ... - + + + + Each universally quantified type variable +tvi must be reachable from type. -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: +A type variable is "reachable" if it it is functionally dependent +(see ) +on the type variables 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: - type P a = [[a]] - instance Monad P where ... + forall a. Eq a => Int -This design decision is independent of all the others, and easily -reversed, but it makes sense to me. +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. -The types in an instance-declaration context must all -be type variables. Thus + 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: -instance C a b => Eq (a,b) where ... + forall a. C a b => burble -is OK, but +The next type is illegal because the constraint Eq b does not +mention a: -instance C Int b => Foo b where ... + forall a. Eq b => burble -is not OK. Again, the intent here is to make sure that context -reduction terminates. - -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. +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. @@ -1514,1136 +1528,1037 @@ with N. - - - - -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. - + +For-all hoisting -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. +It is often convenient to use generalised type synonyms (see ) at the right hand +end of an arrow, thus: - sort :: (?cmp :: a -> a -> Bool) => [a] -> [a] + type Discard a = forall b. a -> b -> a + + g :: Int -> Discard Int + g x y z = x+y -The dynamic binding constraints are just a new form of predicate in the type class system. - - -An implicit parameter occurs in an expression using the special form ?x, -where x is -any valid identifier (e.g. ord ?x is a valid expression). -Use of this construct also introduces a new -dynamic-binding constraint in the type of the expression. -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 - - - - -Implicit-parameter type constraints - -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: +Simply expanding the type synonym would give - least :: (?cmp :: a -> a -> Bool) => [a] -> a - least xs = fst (sort xs) + g :: Int -> (forall b. Int -> b -> Int) -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 type constraint 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. - - - You can't have an implicit parameter in the context of a class or instance -declaration. For example, both these declarations are illegal: +but GHC "hoists" the forall to give the isomorphic type - class (?x::Int) => C a where ... - instance (?x::a) => Foo [a] where ... + g :: forall b. Int -> Int -> b -> Int -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. - -Implicit-parameter constraints do not cause ambiguity. For example, consider: +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: - f :: (?x :: [a]) => Int -> Int - f n = n + length ?x - - g :: (Read a, Show a) => String -> String - g s = show (read s) + type1 -> forall a1..an. context2 => type2 +==> + forall a1..an. context2 => type1 -> type2 -Here, g has an ambiguous type, and is rejected, but f -is fine. The binding for ?x at f's call site is -quite unambiguous, and fixes the type a. - - - - -Implicit-parameter bindings - - -An implicit parameter is bound using the standard -let or where binding forms. -For example, we define the min function by binding -cmp. +(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: - min :: [a] -> a - min = let ?cmp = (<=) in least + g :: Int -> Int -> forall b. b -> Int -A group of implicit-parameter bindings may occur anywhere a normal group of Haskell -bindings can occur, except at top level. That is, they can occur in a let -(including in a list comprehension, or do-notation, or pattern guards), -or a where clause. -Note the following points: - - -An implicit-parameter binding group 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. - - -You may not mix implicit-parameter bindings with ordinary bindings in a -single let -expression; use two nested lets instead. -(In the case of where you are stuck, since you can't nest where clauses.) - - - -You may put multiple implicit-parameter bindings in a -single binding group; but they are not treated -as a mutually recursive group (as ordinary let bindings are). -Instead they are treated as a non-recursive group, simultaneously binding all the implicit -parameter. The bindings are not nested, and may be re-ordered without changing -the meaning of the program. -For example, consider: +When doing this hoisting operation, GHC eliminates duplicate constraints. For +example: - f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y + type Foo a = (?x::Int) => Bool -> a + g :: Foo (Foo Int) -The use of ?x in the binding for ?y does not "see" -the binding for ?x, so the type of f is +means - f :: (?x::Int) => Int -> Int + g :: (?x::Int) => Bool -> Bool -> Int - - - + + - -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) - + +Instance declarations + +Overlapping instances -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 ) +In general, instance declarations may not overlap. The two instance +declarations - data NameSupply = ... - - splitNS :: NameSupply -> (NameSupply, NameSupply) - newName :: NameSupply -> Name - instance Splittable NameSupply where - split = splitNS + + 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. - 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: - - 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. + EITHER type1 and type2 do not unify - -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. - + + OR type2 is a substitution instance of type1 +(but not identical to type1), or vice versa. - -Warnings + + +Notice that these rules + + -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. + make it clear which instance decl to use +(pick the most specific one that matches) + + + + -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. + do not mention the contexts context1, context2 +Reason: you can pick which instance decl +"matches" based on the type. + - - -Recursive functions -Linear implicit parameters can be particularly tricky when you have a recursive function -Consider + +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: - foo :: %x::T => Int -> [Int] - foo 0 = [] - foo n = %x : foo (n-1) + instance C (Int,a) where ... + instance C (a,Bool) where ... -where T is some type in class Splittable. +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. + -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 +GHC is also conservative about committing to an overlapping instance. For example: - foo x = let - foom 0 = [] - foom n = x : foom (n-1) - in - foom + 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 -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. +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.) - - - -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, -. - + +Type synonyms in the instance head -There should be more documentation, but there isn't (yet). Yell if you need it. - - +Unlike Haskell 98, instance heads may use type +synonyms. (The instance "head" is the bit after the "=>" in an instance decl.) +As always, using a type synonym is just shorthand for +writing the RHS of the type synonym definition. For example: - -Arbitrary-rank polymorphism - - - -Haskell type signatures are implicitly quantified. The new keyword forall -allows us to say exactly what this means. For example: - - - g :: b -> b - -means this: - - g :: forall b. (b -> b) + type Point = (Int,Int) + instance C Point where ... + instance C [Point] where ... -The two are treated identically. - - -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 +is legal. However, if you added + - 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. - - -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. - - -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) + instance C (Int,Int) where ... -Of course forall becomes a keyword; you can't use forall as -a type variable any more! - - -Examples - - - -In a data or newtype declaration one can quantify -the types of the constructor arguments. Here are several examples: - +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: - -data T a = T1 (forall b. b -> b -> b) a + type P a = [[a]] + instance Monad P where ... + -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]) - +This design decision is independent of all the others, and easily +reversed, but it makes sense to me. + - -The constructors have rank-2 types: - + +Undecidable instances - +An instance declaration must normally obey the following rules: + +At least one of the types in the head of +an instance declaration must not be a type variable. +For example, these are OK: -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 - + instance C Int a where ... - + instance D (Int, Int) where ... - -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. + instance E [[a]] where ... + +but this is not: + + instance F a where ... + +Note that instance heads may contain repeated type variables. +For example, this is OK: + + instance Stateful (ST s) (MutVar s) where ... + + - -As for type signatures, implicit quantification happens for non-overloaded -types too. So if you write this: + +All of the types in the context of +an instance declaration must be type variables. +Thus - data T a = MkT (Either a b) (b -> b) +instance C a b => Eq (a,b) where ... + +is OK, but + +instance C Int b => Foo b where ... + +is not OK. + + + +These restrictions 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 ... +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: - data T a = MkT (forall b. Either a b) (forall b. b -> b) + instance C a where + op = ... -- Default -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.) - - -You construct values of types T1, MonadT, Swizzle by applying -the constructor to suitable values, just as usual. For example, - +Second, sometimes you might want to use the following to get the +effect of a "class synonym": - - 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 + class (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] + instance (C1 a, C2 a, C3 a) => C a where { } - - - -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.) - - -When you use pattern matching, the bound variables may now have -polymorphic types. For example: - +This allows you to write shorter signatures: - - f :: T a -> a -> (a, Char) - f (T1 w k) x = (w k x, w 'c' 'd') + f :: C a => ... + - 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) +instead of + + + + f :: (C1 a, C2 a, C3 a) => ... - +Voluminous correspondence on the Haskell mailing list has convinced me +that it's worth experimenting with more liberal rules. If you use +the experimental flag +-fallow-undecidable-instances +option, you can use arbitrary +types in both an instance context and instance head. Termination is ensured by having a +fixed-depth recursion stack. If you exceed the stack depth you get a +sort of backtrace, and the opportunity to increase the stack depth +with N. + -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. +I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while +allowing these idioms interesting idioms. - -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: + + + +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.) + +Implicit parameter support is enabled with the option +. + -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. +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. -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: - - \ f :: (forall a. a->a) -> (f True, f 'c') - -Alternatively, you can give a type signature to the enclosing -context, which GHC can "push down" to find the type for the variable: - - (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char) - -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: +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. - f :: T a -> a -> (a, Char) - f (T1 w k) x = (w k x, w 'c' 'd') + sort :: (?cmp :: a -> a -> Bool) => [a] -> [a] -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. +The dynamic binding constraints are just a new form of predicate in the type class system. - - - - - -Implicit quantification - -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: +An implicit parameter occurs in an expression using the special form ?x, +where x is +any valid identifier (e.g. ord ?x is a valid expression). +Use of this construct also introduces a new +dynamic-binding constraint in the type of the expression. +For example, the following definition +shows how we can define an implicitly parameterized sort function in +terms of an explicitly parameterized sortBy function: - f :: a -> a - f :: forall a. a -> a + sortBy :: (a -> a -> Bool) -> [a] -> [a] - 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 ... + sort :: (?cmp :: a -> a -> Bool) => [a] -> [a] + sort = sortBy ?cmp + + +Implicit-parameter type constraints -Notice that GHC does not find the innermost possible quantification -point. For example: +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: - f :: (a -> a) -> Int - -- MEANS - f :: forall a. (a -> a) -> Int - -- NOT - f :: (forall a. a -> a) -> Int - - - 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 + least :: (?cmp :: a -> a -> Bool) => [a] -> a + least xs = fst (sort xs) -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. +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 type constraint 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. - - - - -Liberalised type synonyms - + 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 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: +Implicit-parameter constraints do not cause ambiguity. For example, consider: - type Discard a = forall b. Show b => a -> b -> (a, String) - - f :: Discard a - f x y = (x, show y) + f :: (?x :: [a]) => Int -> Int + f n = n + length ?x - g :: Discard Int -> (Int,Bool) -- A rank-2 type - g f = f Int True + g :: (Read a, Show a) => String -> String + g s = show (read s) +Here, g has an ambiguous type, and is rejected, but f +is fine. The binding for ?x at f's call site is +quite unambiguous, and fixes the type a. - + + + +Implicit-parameter bindings - -You can write an unboxed tuple in a type synonym: + +An implicit parameter is bound using the standard +let or where binding forms. +For example, we define the min function by binding +cmp. - type Pr = (# Int, Int #) - - h :: Int -> Pr - h x = (# x, x #) + min :: [a] -> a + min = let ?cmp = (<=) in least + + +A group of implicit-parameter bindings may occur anywhere a normal group of Haskell +bindings can occur, except at top level. That is, they can occur in a let +(including in a list comprehension, or do-notation, or pattern guards), +or a where clause. +Note the following points: + + +An implicit-parameter binding group 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. - -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 - +You may not mix implicit-parameter bindings with ordinary bindings in a +single let +expression; use two nested lets instead. +(In the case of where you are stuck, since you can't nest where clauses.) -You can apply a type synonym to a partially applied type synonym: +You may put multiple implicit-parameter bindings in a +single binding group; but they are not treated +as a mutually recursive group (as ordinary let bindings are). +Instead they are treated as a non-recursive group, simultaneously binding all the implicit +parameter. The bindings are not nested, and may be re-ordered without changing +the meaning of the program. +For example, consider: - type Generic i o = forall x. i x -> o x - type Id x = x - - foo :: Generic Id [] + f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y -After epxanding the synonym, foo has the legal (in GHC) type: +The use of ?x in the binding for ?y does not "see" +the binding for ?x, so the type of f is - foo :: forall x. x -> [x] + f :: (?x::Int) => Int -> Int - + + + + +Linear implicit parameters -GHC currently does kind checking before expanding synonyms (though even that -could be changed.) +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: - -After expanding type synonyms, GHC does validity checking on types, looking for -the following mal-formedness which isn't detected simply by kind checking: - -Type constructor applied to a type involving for-alls. - - -Unboxed tuple on left of an arrow. - - -Partially-applied type synonym. - + distributing a supply of unique names + distributing a suppply of random numbers + distributing an oracle (as in QuickCheck) -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. + +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-all hoisting -It is often convenient to use generalised type synonyms at the right hand -end of an arrow, thus: +For example: - type Discard a = forall b. a -> b -> a + import GHC.Exts( Splittable ) - g :: Int -> Discard Int - g x y z = x+y + data NameSupply = ... + + splitNS :: NameSupply -> (NameSupply, NameSupply) + newName :: NameSupply -> Name + + 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... -Simply expanding the type synonym would give +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: - g :: Int -> (forall b. Int -> b -> Int) + 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' -but GHC "hoists" the forall to give the isomorphic type +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: - g :: forall b. Int -> Int -> b -> Int + class Splittable a where + split :: a -> (a,a) -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 instance for Splittable NameSupply tells GHC how to implement +split for name supplies. But we can simply write - type1 -> forall a1..an. context2 => type2 -==> - forall a1..an. context2 => type1 -> type2 + g x = (x, %ns, %ns) -(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: +and GHC will infer - g :: Int -> Int -> forall b. b -> Int + g :: (Splittable a, %ns :: a) => b -> (b,a,a) +The Splittable class is built into GHC. It's exported by module +GHC.Exts. -When doing this hoisting operation, GHC eliminates duplicate constraints. For -example: +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. + + + +Warnings + + +The monomorphism restriction is even more important than usual. +Consider the example above: - type Foo a = (?x::Int) => Bool -> a - g :: Foo (Foo Int) + 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' -means +If we replaced the two occurrences of x' by (newName %ns), which is +usually a harmless thing to do, we get: - g :: (?x::Int) => Bool -> Bool -> Int + 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. + + +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. - - - -Existentially quantified data constructors - + +Recursive functions +Linear implicit parameters can be particularly tricky when you have a recursive function +Consider + + foo :: %x::T => Int -> [Int] + foo 0 = [] + foo n = %x : foo (n-1) + +where T is some type in class Splittable. -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: +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. + - - - - data Foo = forall a. MkFoo a (a -> Bool) - | Nil - + - + +Functional dependencies + - -The data type Foo has two constructors with types: + 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, +. - - +Functional dependencies are introduced by a vertical bar in the syntax of a +class declaration; e.g. - MkFoo :: forall a. a -> (a -> Bool) -> Foo - Nil :: Foo - - - + class (Monad m) => MonadState s m | m -> s where ... - -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: + class Foo a b c | a b -> c where ... + +There should be more documentation, but there isn't (yet). Yell if you need it. + - - - - [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] - - - -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. - + +Explicitly-kinded quantification -What can we do with a value of type Foo?. In particular, -what happens when we pattern-match on MkFoo? +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. - - - - f (MkFoo val fn) = ??? - - +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 + + -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 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. - - - f :: Foo -> Bool - f (MkFoo val fn) = fn val - - +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. + - -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. - - -Why existential? +<sect2 id="universal-quantification"> +<title>Arbitrary-rank polymorphism -What has this to do with existential quantification? -Simply that MkFoo has the (nearly) isomorphic type +Haskell type signatures are implicitly quantified. The new keyword forall +allows us to say exactly what this means. For example: - - - MkFoo :: (exists a . (a, a -> Bool)) -> Foo + g :: b -> b - - - - -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: - - - - +means this: -data Baz = forall a. Eq a => Baz1 a a - | forall b. Show b => Baz2 b (b -> b) + g :: forall b. (b -> b) - - - - -The two constructors have the types you'd expect: +The two are treated identically. - +However, GHC's type system supports arbitrary-rank +explicit universal quantification in +types. +For example, all the following types are legal: -Baz1 :: forall a. Eq a => a -> a -> Baz -Baz2 :: forall b. Show b => b -> (b -> b) -> Baz - + 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 - -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: + 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. - - - - f :: Baz -> String - f (Baz1 p q) | p == q = "Yes" - | otherwise = "No" - f (Baz2 v fn) = show (fn v) - - +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. - -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 function f3 has a rank-3 type; +it has rank-2 types on the left of a function arrow. - -Notice the way that the syntax fits smoothly with that used for -universal quantification earlier. +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 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! - - -Restrictions + +Examples + -There are several restrictions on the ways in which existentially-quantified -constructors can be use. +In a data or newtype declaration one can quantify +the types of the constructor arguments. Here are several examples: - - - - - 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: +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 + } - - f1 :: Foo -> a -- Weird! +newtype Swizzle = MkSwizzle (Ord a => [a] -> [a]) + -What is this "a" in the result type? Clearly we don't mean -this: + +The constructors have rank-2 types: + + - f1 :: forall a. Foo -> a -- Wrong! +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 original program is just plain wrong. Here's another sort of error + +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: - f2 (Baz1 a b) (Baz1 p q) = a==q + data T a = MkT (Either a b) (b -> b) +it's just as if you had written this: -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. - + + 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.) - - -You can't pattern-match on an existentially quantified -constructor in a let or where group of -bindings. So this is illegal: +You construct values of types T1, MonadT, Swizzle by applying +the constructor to suitable values, just as usual. For example, + + - f3 x = a==b where { Baz1 a b = x } - - -Instead, use a case expression: + 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 - - f3 x = case x of Baz1 a b -> a==b + mkTs :: (forall b. b -> b -> b) -> a -> [T a] + mkTs f x y = [T1 f x, T1 f y] -In general, 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. + + +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.) - - -You can't use existential quantification for newtype -declarations. So this is illegal: +When you use pattern matching, the bound variables may now have +polymorphic types. For example: + + - newtype T = forall a. Ord a => MkT a - - + f :: T a -> a -> (a, Char) + f (T1 w k) x = (w k x, w 'c' 'd') -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. + 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) + - - - You can't use deriving to define instances of a -data type with existentially quantified data constructors. +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. + + -Reason: in most cases it would not make sense. For example:# + +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: -data T = forall a. MkT [a] deriving( Eq ) + \ f :: (forall a. a->a) -> (f True, f 'c') + +Alternatively, you can give a type signature to the enclosing +context, which GHC can "push down" to find the type for the variable: + + (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char) + +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: + + 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. + -To derive Eq in the standard way we would need to have equality -between the single component of two MkT constructors: + + + + +Implicit quantification + +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 Eq T where - (MkT a) == (MkT b) = ??? - + f :: a -> a + f :: forall a. a -> a -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! + 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 - + 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. - - + + + Scoped type variables @@ -2839,66 +2754,27 @@ ordinary type signatures). - - - - - -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 - - - -(Not implemented in Hugs yet, Dec 98). - - - - - - - - - - -Result type signatures - - + - - - The result type of a function can be given a signature, -thus: - - - - 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: +The type variables in the head of a class or instance declaration +scope over the methods defined in the where part. For example: - f :: Int -> [a] -> [a] - f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x) - in \xs -> map g (reverse xs `zip` xs) + class C a where + op :: [a] -> a + + op xs = let ys::[a] + ys = reverse xs + in + head ys +(Not implemented in Hugs yet, Dec 98). @@ -2906,10 +2782,6 @@ you want: - -Result type signatures are not yet implemented in Hugs. - - @@ -3025,6 +2897,80 @@ in f4's scope. + + +Result type signatures + + +The result type of a function can be given a signature, thus: + + + + 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: + + + + f :: Int -> [a] -> [a] + f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x) + in \xs -> map g (reverse xs `zip` xs) + + + + +The type variables bound in a result type signature scope over the right hand side +of the definition. However, consider this corner-case: + + rev1 :: [a] -> [a] = \xs -> reverse xs + + foo ys = rev (ys::[a]) + +The signature on rev1 is considered a pattern type signature, not a result +type signature, and the type variables it binds have the same scope as rev1 +itself (i.e. the right-hand side of rev1 and the rest of the module too). +In particular, the expression (ys::[a]) is OK, because the type variable a +is in scope (otherwise it would mean (ys::forall a.[a]), which would be rejected). + + +As mentioned above, rev1 is made monomorphic by this scoping rule. +For example, the following program would be rejected, because it claims that rev1 +is polymorphic: + + rev1 :: [b] -> [b] + rev1 :: [a] -> [a] = \xs -> reverse xs + + + + +Result type signatures are not yet implemented in Hugs. + + + + + + + +Deriving clause for classes <literal>Typeable</literal> and <literal>Data</literal> + + +Haskell 98 allows the programmer to add "deriving( Eq, Ord )" to a data type +declaration, to generate a standard instance declaration for classes specified in the deriving clause. +In Haskell 98, the only classes that may appear in the deriving clause are the standard +classes Eq, Ord, +Enum, Ix, Bounded, Read, and Show. + + +GHC extends this list with two more classes that may be automatically derived +(provided the flag is specified): +Typeable, and Data. These classes are defined in the library +modules Data.Dynamic and Data.Generics respectively, and the +appropriate class must be in scope before it can be mentioned in the deriving clause. + @@ -3153,13 +3099,33 @@ 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, - +where + + + S is a type constructor, + + + The t1...tk are types, + + + The 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', where the arity of C + is exactly j+1. That is, C lacks exactly one type argument. + + + None of the ci is Read, Show, + Typeable, or Data. These classes + should not "look through" the type or its constructor. You can still + derive these classes for a newtype, but it happens in the usual way, not + via this new mechanism. + + +Then, for each ci, the derived instance +declaration is: instance ci (S t1...tk vk+1...v) => ci (T v1...vp) @@ -3211,11 +3177,13 @@ instances is most interesting. Template Haskell -Template Haskell allows you to do compile-time meta-programming in Haskell. The background -the main technical innovations are discussed in "Template Haskell allows you to do compile-time meta-programming in Haskell. There is a "home page" for +Template Haskell at +http://www.haskell.org/th/, while +the background to +the main technical innovations is discussed in " -Template Meta-programming for Haskell", in -Proc Haskell Workshop 2002. +Template Meta-programming for Haskell" (Proc Haskell Workshop 2002). The first example from that paper is set out below as a worked example to help get you started. @@ -3226,10 +3194,16 @@ The documentation here describes the realisation in GHC. (It's rather sketchy j Tim Sheard is going to expand it.) - Syntax - - Template Haskell has the following new syntactic constructions. You need to use the flag - -fglasgow-exts to switch these syntactic extensions on. + + Syntax + + Template Haskell has the following new syntactic + constructions. You need to use the flag + + to switch these syntactic extensions on + ( is currently implied by + , but you are encouraged to + specify it explicitly). @@ -3276,7 +3250,6 @@ Tim Sheard is going to expand it.) - Using Template Haskell @@ -3296,6 +3269,13 @@ Tim Sheard is going to expand it.) The flag -ddump-splices shows the expansion of all top-level splices as they happen. + + If you are building GHC from source, you need at least a stage-2 bootstrap compiler to + run Template Haskell. A stage-1 compiler will reject the TH constructs. Reason: TH + compiles and runs a program, and then looks at the result. So it's important that + the program it compiles produces results whose representations are identical to + those of the compiler itself. + Template Haskell works in any mode (--make, --interactive, @@ -3309,68 +3289,540 @@ Tim Sheard is going to expand it.) First cut and paste the two modules below into "Main.hs" and "Printf.hs": -{- Main.hs -} -module Main where - --- Import our template "pr" -import Printf ( pr ) +{- Main.hs -} +module Main where + +-- Import our template "pr" +import Printf ( pr ) + +-- The splice operator $ takes the Haskell source code +-- generated at compile time by "pr" and splices it into +-- the argument of "putStrLn". +main = putStrLn ( $(pr "Hello") ) + + + +{- Printf.hs -} +module Printf where + +-- Skeletal printf from the paper. +-- It needs to be in a separate module to the one where +-- you intend to use it. + +-- Import some Template Haskell syntax +import Language.Haskell.THSyntax + +-- Describe a format string +data Format = D | S | L String + +-- Parse a format string. This is left largely to you +-- as we are here interested in building our first ever +-- Template Haskell program and not in building printf. +parse :: String -> [Format] +parse s = [ L s ] + +-- Generate Haskell source code from a parsed representation +-- of the format string. This code will be spliced into +-- the module which calls "pr", at compile time. +gen :: [Format] -> Expr +gen [D] = [| \n -> show n |] +gen [S] = [| \s -> s |] +gen [L s] = string s + +-- Here we generate the Haskell code for the splice +-- from an input format string. +pr :: String -> Expr +pr s = gen (parse s) + + +Now run the compiler (here we are a Cygwin prompt on Windows): + + +$ ghc --make -fth main.hs -o main.exe + + +Run "main.exe" and here is your output: + + +$ ./main +Hello + + + + + + + + + +Arrow notation + + +Arrows are a generalization of monads introduced by John Hughes. +For more details, see + + + + +“Generalising Monads to Arrows”, +John Hughes, in Science of Computer Programming 37, +pp67–111, May 2000. + + + + + +“A New Notation for Arrows”, +Ross Paterson, in ICFP, Sep 2001. + + + + + +“Arrows and Computation”, +Ross Paterson, in The Fun of Programming, +Palgrave, 2003. + + + + +and the arrows web page at +http://www.haskell.org/arrows/. +With the flag, GHC supports the arrow +notation described in the second of these papers. +What follows is a brief introduction to the notation; +it won't make much sense unless you've read Hughes's paper. +This notation is translated to ordinary Haskell, +using combinators from the +Control.Arrow +module. + + +The extension adds a new kind of expression for defining arrows, +of the form proc pat -> cmd, +where proc is a new keyword. +The variables of the pattern are bound in the body of the +proc-expression, +which is a new sort of thing called a command. +The syntax of commands is as follows: + +cmd ::= exp1 -< exp2 + | exp1 -<< exp2 + | do { cstmt1 .. cstmtn ; cmd } + | let decls in cmd + | if exp then cmd1 else cmd2 + | case exp of { calts } + | cmd1 qop cmd2 + | (| aexp cmd1 .. cmdn |) + | \ pat1 .. patn -> cmd + | cmd aexp + | ( cmd ) + +cstmt ::= let decls + | pat <- cmd + | rec { cstmt1 .. cstmtn } + | cmd + +Commands produce values, but (like monadic computations) +may yield more than one value, +or none, and may do other things as well. +For the most part, familiarity with monadic notation is a good guide to +using commands. +However the values of expressions, even monadic ones, +are determined by the values of the variables they contain; +this is not necessarily the case for commands. + + + +A simple example of the new notation is the expression + +proc x -> f -< x+1 + +We call this a procedure or +arrow abstraction. +As with a lambda expression, the variable x +is a new variable bound within the proc-expression. +It refers to the input to the arrow. +In the above example, -< is not an identifier but an +new reserved symbol used for building commands from an expression of arrow +type and an expression to be fed as input to that arrow. +(The weird look will make more sense later.) +It may be read as analogue of application for arrows. +The above example is equivalent to the Haskell expression + +arr (\ x -> x+1) >>> f + +That would make no sense if the expression to the left of +-< involves the bound variable x. +More generally, the expression to the left of -< +may not involve any local variable, +i.e. a variable bound in the current arrow abstraction. +For such a situation there is a variant -<<, as in + +proc x -> f x -<< x+1 + +which is equivalent to + +arr (\ x -> (f, x+1)) >>> app + +so in this case the arrow must belong to the ArrowApply +class. +Such an arrow is equivalent to a monad, so if you're using this form +you may find a monadic formulation more convenient. + + + +do-notation for commands + + +Another form of command is a form of do-notation. +For example, you can write + +proc x -> do + y <- f -< x+1 + g -< 2*y + let z = x+y + t <- h -< x*z + returnA -< t+z + +You can read this much like ordinary do-notation, +but with commands in place of monadic expressions. +The first line sends the value of x+1 as an input to +the arrow f, and matches its output against +y. +In the next line, the output is discarded. +The arrow returnA is defined in the +Control.Arrow +module as arr id. +The above example is treated as an abbreviation for + +arr (\ x -> (x, x)) >>> + first (arr (\ x -> x+1) >>> f) >>> + arr (\ (y, x) -> (y, (x, y))) >>> + first (arr (\ y -> 2*y) >>> g) >>> + arr snd >>> + arr (\ (x, y) -> let z = x+y in ((x, z), z)) >>> + first (arr (\ (x, z) -> x*z) >>> h) >>> + arr (\ (t, z) -> t+z) >>> + returnA + +Note that variables not used later in the composition are projected out. +After simplification using rewrite rules (see ) +defined in the +Control.Arrow +module, this reduces to + +arr (\ x -> (x+1, x)) >>> + first f >>> + arr (\ (y, x) -> (2*y, (x, y))) >>> + first g >>> + arr (\ (_, (x, y)) -> let z = x+y in (x*z, z)) >>> + first h >>> + arr (\ (t, z) -> t+z) + +which is what you might have written by hand. +With arrow notation, GHC keeps track of all those tuples of variables for you. + + + +Note that although the above translation suggests that +let-bound variables like z must be +monomorphic, the actual translation produces Core, +so polymorphic variables are allowed. + + + +It's also possible to have mutually recursive bindings, +using the new rec keyword, as in the following example: + +counter :: ArrowCircuit a => a Bool Int +counter = proc reset -> do + rec output <- returnA -< if reset then 0 else next + next <- delay 0 -< output+1 + returnA -< output + +The translation of such forms uses the loop combinator, +so the arrow concerned must belong to the ArrowLoop class. + + + + + +Conditional commands + + +In the previous example, we used a conditional expression to construct the +input for an arrow. +Sometimes we want to conditionally execute different commands, as in + +proc (x,y) -> + if f x y + then g -< x+1 + else h -< y+2 + +which is translated to + +arr (\ (x,y) -> if f x y then Left x else Right y) >>> + (arr (\x -> x+1) >>> f) ||| (arr (\y -> y+2) >>> g) + +Since the translation uses |||, +the arrow concerned must belong to the ArrowChoice class. + + + +There are also case commands, like + +case input of + [] -> f -< () + [x] -> g -< x+1 + x1:x2:xs -> do + y <- h -< (x1, x2) + ys <- k -< xs + returnA -< y:ys + +The syntax is the same as for case expressions, +except that the bodies of the alternatives are commands rather than expressions. +The translation is similar to that of if commands. + + + + + +Defining your own control structures + + +As we're seen, arrow notation provides constructs, +modelled on those for expressions, +for sequencing, value recursion and conditionals. +But suitable combinators, +which you can define in ordinary Haskell, +may also be used to build new commands out of existing ones. +The basic idea is that a command defines an arrow from environments to values. +These environments assign values to the free local variables of the command. +Thus combinators that produce arrows from arrows +may also be used to build commands from commands. +For example, the ArrowChoice class includes a combinator + +ArrowChoice a => (<+>) :: a e c -> a e c -> a e c + +so we can use it to build commands: + +expr' = proc x -> + returnA -< x + <+> do + symbol Plus -< () + y <- term -< () + expr' -< x + y + <+> do + symbol Minus -< () + y <- term -< () + expr' -< x - y + +This is equivalent to + +expr' = (proc x -> returnA -< x) + <+> (proc x -> do + symbol Plus -< () + y <- term -< () + expr' -< x + y) + <+> (proc x -> do + symbol Minus -< () + y <- term -< () + expr' -< x - y) + +It is essential that this operator be polymorphic in e +(representing the environment input to the command +and thence to its subcommands) +and satisfy the corresponding naturality property + +arr k >>> (f <+> g) = (arr k >>> f) <+> (arr k >>> g) + +at least for strict k. +(This should be automatic if you're not using seq.) +This ensures that environments seen by the subcommands are environments +of the whole command, +and also allows the translation to safely trim these environments. +The operator must also not use any variable defined within the current +arrow abstraction. + + + +We could define our own operator + +untilA :: ArrowChoice a => a e () -> a e Bool -> a e () +untilA body cond = proc x -> + if cond x then returnA -< () + else do + body -< x + untilA body cond -< x + +and use it in the same way. +Of course this infix syntax only makes sense for binary operators; +there is also a more general syntax involving special brackets: + +proc x -> do + y <- f -< x+1 + (|untilA (increment -< x+y) (within 0.5 -< x)|) + + + + + + +Primitive constructs + + +Some operators will need to pass additional inputs to their subcommands. +For example, in an arrow type supporting exceptions, +the operator that attaches an exception handler will wish to pass the +exception that occurred to the handler. +Such an operator might have a type + +handleA :: ... => a e c -> a (e,Ex) c -> a e c + +where Ex is the type of exceptions handled. +You could then use this with arrow notation by writing a command + +body `handleA` \ ex -> handler + +so that if an exception is raised in the command body, +the variable ex is bound to the value of the exception +and the command handler, +which typically refers to ex, is entered. +Though the syntax here looks like a functional lambda, +we are talking about commands, and something different is going on. +The input to the arrow represented by a command consists of values for +the free local variables in the command, plus a stack of anonymous values. +In all the prior examples, this stack was empty. +In the second argument to handleA, +this stack consists of one value, the value of the exception. +The command form of lambda merely gives this value a name. + + + +More concretely, +the values on the stack are paired to the right of the environment. +So when designing operators like handleA that pass +extra inputs to their subcommands, +More precisely, the type of each argument of the operator (and its result) +should have the form + +a (...(e,t1), ... tn) t + +where e is a polymorphic variable +(representing the environment) +and ti are the types of the values on the stack, +with t1 being the top. +The polymorphic variable e must not occur in +a, ti or +t. +However the arrows involved need not be the same. +Here are some more examples of suitable operators: + +bracketA :: ... => a e b -> a (e,b) c -> a (e,c) d -> a e d +runReader :: ... => a e c -> a' (e,State) c +runState :: ... => a e c -> a' (e,State) (c,State) + +We can supply the extra input required by commands built with the last two +by applying them to ordinary expressions, as in + +proc x -> do + s <- ... + (|runReader (do { ... })|) s + +which adds s to the stack of inputs to the command +built using runReader. + + + +The command versions of lambda abstraction and application are analogous to +the expression versions. +In particular, the beta and eta rules describe equivalences of commands. +These three features (operators, lambda abstraction and application) +are the core of the notation; everything else can be built using them, +though the results would be somewhat clumsy. +For example, we could simulate do-notation by defining + +bind :: Arrow a => a e b -> a (e,b) c -> a e c +u `bind` f = returnA &&& u >>> f --- The splice operator $ takes the Haskell source code --- generated at compile time by "pr" and splices it into --- the argument of "putStrLn". -main = putStrLn ( $(pr "Hello") ) +bind_ :: Arrow a => a e b -> a e c -> a e c +u `bind_` f = u `bind` (arr fst >>> f) - +We could simulate do by defining -{- Printf.hs -} -module Printf where +cond :: ArrowChoice a => a e b -> a e b -> a (e,Bool) b +cond f g = arr (\ (e,b) -> if b then Left e else Right e) >>> f ||| g + + --- Skeletal printf from the paper. --- It needs to be in a separate module to the one where --- you intend to use it. + --- Import some Template Haskell syntax -import Language.Haskell.THSyntax + +Differences with the paper --- Describe a format string -data Format = D | S | L String + --- Parse a format string. This is left largely to you --- as we are here interested in building our first ever --- Template Haskell program and not in building printf. -parse :: String -> [Format] -parse s = [ L s ] + +Instead of a single form of arrow application (arrow tail) with two +translations, the implementation provides two forms +-< (first-order) +and -<< (higher-order). + + --- Generate Haskell source code from a parsed representation --- of the format string. This code will be spliced into --- the module which calls "pr", at compile time. -gen :: [Format] -> Expr -gen [D] = [| \n -> show n |] -gen [S] = [| \s -> s |] -gen [L s] = string s + +User-defined operators are flagged with banana brackets instead of +a new form keyword. + + --- Here we generate the Haskell code for the splice --- from an input format string. -pr :: String -> Expr -pr s = gen (parse s) - + + + + + +Portability + + +Although only GHC implements arrow notation directly, +there is also a preprocessor +(available from the +arrows web page) +that translates arrow notation into Haskell 98 +for use with other Haskell systems. +You would still want to check arrow programs with GHC; +tracing type errors in the preprocessor output is not easy. +Modules intended for both GHC and the preprocessor must observe some +additional restrictions: + -Now run the compiler (here we are using a "stage three" build of GHC, at a Cygwin prompt on Windows): + + +The module must import +Control.Arrow. - -stage3/ghc/compiler/ghc-inplace --make -fglasgow-exts -package haskell-src main.hs -o main.exe - + + + + +The preprocessor cannot cope with other Haskell extensions. +These would have to go in separate modules. + + -Run "main.exe" and here is your output: + + +Because the preprocessor targets Haskell (rather than Core), +let-bound variables are monomorphic. + - -$ ./main -Hello - + + - + @@ -3484,32 +3936,72 @@ Assertion failures can be caught, see the documentation for the unrecognised word is (silently) ignored. - -INLINE pragma + <sect2 id="deprecated-pragma"> + <title>DEPRECATED pragma + DEPRECATED + -INLINE pragma -pragma, INLINE + The DEPRECATED pragma lets you specify that a particular + function, class, or type, is deprecated. There are two + forms. - -GHC (with , as always) tries to inline (or “unfold”) -functions/values that are “small enough,” thus avoiding the call -overhead and possibly exposing other more-wonderful optimisations. - + + + You can deprecate an entire module thus: + + module Wibble {-# DEPRECATED "Use Wobble instead" #-} where + ... + + When you compile any module that import + Wibble, GHC will print the specified + message. + - -You will probably see these unfoldings (in Core syntax) in your -interface files. - + + You can deprecate a function, class, or type, with the + following top-level declaration: + + {-# DEPRECATED f, C, T "Don't use these" #-} + + When you compile any module that imports and uses any + of the specifed entities, GHC will print the specified + message. + + + Any use of the deprecated item, or of anything from a deprecated + module, will be flagged with an appropriate message. However, + deprecations are not reported for + (a) uses of a deprecated function within its defining module, and + (b) uses of a deprecated function in an export list. + The latter reduces spurious complaints within a library + in which one module gathers together and re-exports + the exports of several others. + + You can suppress the warnings with the flag + . + - -Normally, if GHC decides a function is “too expensive” to inline, it -will not do so, nor will it export that unfolding for other modules to -use. - + + INLINE and NOINLINE pragmas - -The sledgehammer you can bring to bear is the -INLINEINLINE pragma pragma, used thusly: + These pragmas control the inlining of function + definitions. + + + INLINE pragma + INLINE + + GHC (with , as always) tries to + inline (or “unfold”) functions/values that are + “small enough,” thus avoiding the call overhead + and possibly exposing other more-wonderful optimisations. + Normally, if GHC decides a function is “too + expensive” to inline, it will not do so, nor will it + export that unfolding for other modules to use. + + The sledgehammer you can bring to bear is the + INLINEINLINE + pragma pragma, used thusly: key_function :: Int -> String -> (Bool, Double) @@ -3519,25 +4011,25 @@ key_function :: Int -> String -> (Bool, Double) #endif -(You don't need to do the C pre-processor carry-on unless you're going -to stick the code through HBC—it doesn't like INLINE pragmas.) - + (You don't need to do the C pre-processor carry-on + unless you're going to stick the code through HBC—it + doesn't like INLINE pragmas.) - -The major effect of an INLINE pragma is to declare a function's -“cost” to be very low. The normal unfolding machinery will then be -very keen to inline it. - + The major effect of an INLINE pragma + is to declare a function's “cost” to be very low. + The normal unfolding machinery will then be very keen to + inline it. - -An INLINE pragma for a function can be put anywhere its type -signature could be put. - + Syntactially, an INLINE pragma for a + function can be put anywhere its type signature could be + put. - -INLINE pragmas are a particularly good idea for the -then/return (or bind/unit) functions in a monad. -For example, in GHC's own UniqueSupply monad code, we have: + INLINE pragmas are a particularly + good idea for the + then/return (or + bind/unit) functions in + a monad. For example, in GHC's own + UniqueSupply monad code, we have: #ifdef __GLASGOW_HASKELL__ @@ -3546,32 +4038,140 @@ For example, in GHC's own UniqueSupply monad code, we have: #endif - + See also the NOINLINE pragma (). + + + + NOINLINE pragma + + NOINLINE + NOTINLINE + + 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). + + + + Phase control + + Sometimes you want to control exactly when in GHC's + pipeline the INLINE pragma is switched on. Inlining happens + only during runs of the simplifier. Each + run of the simplifier has a different phase + number; the phase number decreases towards zero. + If you use you'll see the + sequence of phase numbers for successive runs of the + simpifier. In an INLINE pragma you can optionally specify a + phase number, thus: - + + + You can say "inline f in Phase 2 + and all subsequent phases": + + {-# INLINE [2] f #-} + + + - -NOINLINE pragma - + + You can say "inline g in all + phases up to, but not including, Phase 3": + + {-# INLINE [~3] g #-} + + + + + + If you omit the phase indicator, you mean "inline in + all phases". + + -NOINLINE pragma -pragmaNOINLINE -NOTINLINE pragma -pragmaNOTINLINE + You can use a phase number on a NOINLINE pragma too: - -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. - + + + You can say "do not inline f + until Phase 2; in Phase 2 and subsequently behave as if + there was no pragma at all": + + {-# NOINLINE [2] f #-} + + + -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). + + You can say "do not inline g in + Phase 3 or any subsequent phase; before that, behave as if + there was no pragma": + + {-# NOINLINE [~3] g #-} + + + - + + If you omit the phase indicator, you mean "never + inline this function". + + + + The same phase-numbering control is available for RULES + (). + + + + + LINE pragma + + LINEpragma + pragmaLINE + This pragma is similar to C's #line + pragma, and is mainly for use in automatically generated Haskell + code. It lets you specify the line number and filename of the + original code; for example + + +{-# LINE 42 "Foo.vhs" #-} + + + if you'd generated the current file from something called + Foo.vhs and this line corresponds to line + 42 in the original. GHC will adjust its error messages to refer + to the line/file named in the LINE + pragma. + + + + OPTIONS pragma + OPTIONS + + pragmaOPTIONS + + + The OPTIONS pragma is used to specify + additional options that are given to the compiler when compiling + this source file. See for + details. + + + + RULES pragma + + The RULES pragma lets you specify rewrite rules. It is + described in . + SPECIALIZE pragma @@ -3597,35 +4197,37 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value {-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-} - To get very fancy, you can also specify a named function - to use for the specialised value, as in: + A SPECIALIZE pragma for a function can + be put anywhere its type signature could be put. +A SPECIALIZE has the effect of generating (a) a specialised +version of the function and (b) a rewrite rule (see ) that +rewrites a call to the un-specialised function into a call to the specialised +one. You can, instead, provide your own specialised function and your own rewrite rule. +For example, suppose that: -{-# RULES hammeredLookup = blah #-} + genericLookup :: Ord a => Table a b -> a -> b + intLookup :: Table Int b -> Int -> b - - where blah is an implementation of - hammerdLookup written specialy for - Widget lookups. It's Your +where intLookup is an implementation of genericLookup +that works very fast for keys of type Int. Then you can write the rule + + {-# RULES "intLookup" genericLookup = intLookup #-} + +(see ). It is Your Responsibility to make sure that - blah really behaves as a specialised - version of hammeredLookup!!! - - Note we use the RULE pragma here to - indicate that hammeredLookup applied at a - certain type should be replaced by blah. See - for more information on - RULES. + intLookup really behaves as a specialised + version of genericLookup!!! An example in which using RULES for specialisation will Win Big: -toDouble :: Real a => a -> Double -toDouble = fromRational . toRational + toDouble :: Real a => a -> Double + toDouble = fromRational . toRational -{-# SPECIALIZE toDouble :: Int -> Double = i2d #-} -i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly + {-# RULES "toDouble/Int" toDouble = i2d #-} + i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly The i2d function is virtually one machine @@ -3633,9 +4235,6 @@ i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly Rational—is obscenely expensive by comparison. - A SPECIALIZE pragma for a function can - be put anywhere its type signature could be put. - @@ -3663,83 +4262,71 @@ of the pragma. - -LINE pragma - - - -LINE pragma -pragma, LINE - - - -This pragma is similar to C's #line pragma, and is mainly for use in -automatically generated Haskell code. It lets you specify the line -number and filename of the original code; for example - - - - - -{-# LINE 42 "Foo.vhs" #-} - - - - - -if you'd generated the current file from something called Foo.vhs -and this line corresponds to line 42 in the original. GHC will adjust -its error messages to refer to the line/file named in the LINE -pragma. - - - - - -RULES pragma - - -The RULES pragma lets you specify rewrite rules. It is described in -. - - - - - -DEPRECATED pragma - - -The DEPRECATED pragma lets you specify that a particular function, class, or type, is deprecated. -There are two forms. - - - -You can deprecate an entire module thus: - - module Wibble {-# DEPRECATED "Use Wobble instead" #-} where - ... - - -When you compile any module that import Wibble, GHC will print -the specified message. - - - - -You can deprecate a function, class, or type, with the following top-level declaration: - - - {-# DEPRECATED f, C, T "Don't use these" #-} - - -When you compile any module that imports and uses any of the specifed entities, -GHC will print the specified message. - - - -You can suppress the warnings with the flag . - - + + UNPACK pragma + + UNPACK + + The UNPACK indicates to the compiler + that it should unpack the contents of a constructor field into + the constructor itself, removing a level of indirection. For + example: + + +data T = T {-# UNPACK #-} !Float + {-# UNPACK #-} !Float + + + will create a constructor T containing + two unboxed floats. This may not always be an optimisation: if + the T constructor is scrutinised and the + floats passed to a non-strict function for example, they will + have to be reboxed (this is done automatically by the + compiler). + + Unpacking constructor fields should only be used in + conjunction with , in order to expose + unfoldings to the compiler so the reboxing can be removed as + often as possible. For example: + + +f :: T -> Float +f (T f1 f2) = f1 + f2 + + + The compiler will avoid reboxing f1 + and f2 by inlining + + on floats, but only when is on. + + Any single-constructor data is eligible for unpacking; for + example + + +data T = T {-# UNPACK #-} !(Int,Int) + + + will store the two Ints directly in the + T constructor, by flattening the pair. + Multi-level unpacking is also supported: + + +data T = T {-# UNPACK #-} !S +data S = S {-# UNPACK #-} !Int {-# UNPACK #-} !Int + + + will store two unboxed Int#s + directly in the T constructor. The + unpacker can see through newtypes, too. + + If a field cannot be unpacked, you will not get a warning, + so it might be an idea to check the generated code with + . + + See also the flag, + which essentially has the effect of adding + {-# UNPACK #-} to every strict + constructor field. + @@ -3754,7 +4341,10 @@ GHC will print the specified message. The programmer can specify rewrite rules as part of the source program -(in a pragma). GHC applies these rewrite rules wherever it can. +(in a pragma). GHC applies these rewrite rules wherever it can, provided (a) +the flag () is on, +and (b) the flag +() is not specified. @@ -3778,16 +4368,34 @@ From a syntactic point of view: + There may be zero or more rules in a RULES pragma. + + + + + + Each rule has a name, enclosed in double quotes. The name itself has no significance at all. It is only used when reporting how many times the rule fired. - + - There may be zero or more rules in a RULES pragma. +A rule may optionally have a phase-control number (see ), +immediately after the name of the rule. Thus: + + {-# RULES + "map/map" [2] forall f g xs. map f (map g xs) = map (f.g) xs + #-} + +The "[2]" means that the rule is active in Phase 2 and subsequent phases. The inverse +notation "[~2]" is also accepted, meaning that the rule is active up to, but not including, +Phase 2. + + @@ -3796,6 +4404,7 @@ is set, so you must lay out your rules starting in the same column as the enclosing definitions. + @@ -4183,7 +4792,7 @@ will fuse with one but not the other) - + So, for example, the following should generate no intermediate lists: @@ -4271,7 +4880,7 @@ If you add you get a more detailed listing. - The defintion of (say) build in PrelBase.lhs looks llike this: + The defintion of (say) build in GHC/Base.lhs looks llike this: build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a] @@ -4289,9 +4898,9 @@ in the RHS of the INLINE thing. I regret the delicacy of thi - In ghc/lib/std/PrelBase.lhs look at the rules for map to + In libraries/base/GHC/Base.lhs look at the rules for map to see how to write rules that will do fusion and yet give an efficient -program even if fusion doesn't happen. More rules in PrelList.lhs. +program even if fusion doesn't happen. More rules in GHC/List.lhs. @@ -4301,6 +4910,69 @@ program even if fusion doesn't happen. More rules in PrelList.lhs + + CORE pragma + + CORE pragma + pragma, CORE + core, annotation + + + The external core format supports Note annotations; + the CORE pragma gives a way to specify what these + should be in your Haskell source code. Syntactically, core + annotations are attached to expressions and take a Haskell string + literal as an argument. The following function definition shows an + example: + + +f x = ({-# CORE "foo" #-} show) ({-# CORE "bar" #-} x) + + + Sematically, this is equivalent to: + + +g x = show x + + + + + However, when external for is generated (via + ), there will be Notes attached to the + expressions show and x. + The core function declaration for f is: + + + + f :: %forall a . GHCziShow.ZCTShow a -> + a -> GHCziBase.ZMZN GHCziBase.Char = + \ @ a (zddShow::GHCziShow.ZCTShow a) (eta::a) -> + (%note "foo" + %case zddShow %of (tpl::GHCziShow.ZCTShow a) + {GHCziShow.ZCDShow + (tpl1::GHCziBase.Int -> + a -> + GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha +r) + (tpl2::a -> GHCziBase.ZMZN GHCziBase.Char) + (tpl3::GHCziBase.ZMZN a -> + GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha +r) -> + tpl2}) + (%note "foo" + eta); + + + + Here, we can see that the function show (which + has been expanded out to a case expression over the Show dictionary) + has a %note attached to it, as does the + expression eta (which used to be called + x). + + + + @@ -4349,7 +5021,7 @@ Now you can make a data type into an instance of Bin like this: instance (Bin a, Bin b) => Bin (a,b) instance Bin a => Bin [a] -That is, just leave off the "where" clasuse. Of course, you can put in the +That is, just leave off the "where" clause. Of course, you can put in the where clause and over-ride whichever methods you please. @@ -4567,3 +5239,4 @@ Just to finish with, here's another example I rather like: ;;; sgml-parent-document: ("users_guide.sgml" "book" "chapter" "sect1") *** ;;; End: *** --> +