X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=ac10e2128ba42a26160e183af04831ba3b296599;hb=25ebbb764146f4c4634720bb285c3611e95cc951;hp=b2daa16709225747cb102764c71ff752a145977b;hpb=f3575e7955e410f519c9ef436a5407fe235ef704;p=ghc-hetmet.git diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index b2daa16..ac10e21 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -241,6 +241,14 @@ documentation describes all the libraries that come with GHC. + + + Enables overloaded string literals (see ). + + + + Enables lexically-scoped type variables (see describes all the libraries that come with GHC. - - Unboxed types and primitive operations @@ -375,6 +381,13 @@ worse, the unboxed value might be larger than a pointer (Double# for instance). + You cannot define a newtype whose representation type +(the argument type of the data constructor) is an unboxed type. Thus, +this is illegal: + + newtype A = MkA Int# + + You cannot bind a variable with an unboxed type in a top-level binding. @@ -544,14 +557,11 @@ import qualified Control.Monad.ST.Strict as ST linkend="search-path"/>. GHC comes with a large collection of libraries arranged - hierarchically; see the accompanying library documentation. - There is an ongoing project to create and maintain a stable set - of core libraries used by several Haskell - compilers, and the libraries that GHC comes with represent the - current status of that project. For more details, see Haskell - Libraries. - + hierarchically; see the accompanying library + documentation. More libraries to install are available + from HackageDB. @@ -620,7 +630,7 @@ to write clunky would be to use case expressions: -clunky env var1 var1 = case lookup env var1 of +clunky env var1 var2 = case lookup env var1 of Nothing -> fail Just val1 -> case lookup env var2 of Nothing -> fail @@ -645,7 +655,7 @@ Here is how I would write clunky: -clunky env var1 var1 +clunky env var1 var2 | Just val1 <- lookup env var1 , Just val2 <- lookup env var2 = val1 + val2 @@ -939,14 +949,10 @@ definitions; you must define such a function in prefix form. - -Type system extensions - - - -Data types and type synonyms + +Extensions to data types and type synonyms - + Data types with no constructors With the flag, GHC lets you declare @@ -960,13 +966,13 @@ a data type with no constructors. For example: Syntactically, the declaration lacks the "= constrs" part. The type can be parameterised over types of any kind, but if the kind is not * then an explicit kind annotation must be used -(see ). +(see ). Such data types have only one value, namely bottom. Nevertheless, they can be useful when defining "phantom types". - + - + Infix type constructors, classes, and type variables @@ -1033,9 +1039,9 @@ to be written infix, very much like expressions. More specifically: - + - + Liberalised type synonyms @@ -1125,10 +1131,10 @@ this will be rejected: because GHC does not allow unboxed tuples on the left of a function arrow. - + - + Existentially quantified data constructors @@ -1222,7 +1228,7 @@ that collection of packages in a uniform manner. You can express quite a bit of object-oriented-like programming this way. - + Why existential? @@ -1245,9 +1251,9 @@ But Haskell programmers can safely think of the ordinary adding a new existential quantification construct. - + - + Type classes @@ -1307,9 +1313,9 @@ Notice the way that the syntax fits smoothly with that used for universal quantification earlier. - + - + Record Constructors @@ -1326,7 +1332,7 @@ data Counter a = forall self. NewCounter Here tag is a public field, with a well-typed selector function tag :: Counter a -> a. The self type is hidden from the outside; any attempt to apply _this, -_inc or _output as functions will raise a +_inc or _display as functions will raise a compile-time error. In other words, GHC defines a record selector function only for fields whose type does not mention the existentially-quantified variables. (This example used an underscore in the fields for which record selectors @@ -1361,20 +1367,6 @@ main = do display (inc (inc counterB)) -- prints "##" -In GADT declarations (see ), the explicit -forall may be omitted. For example, we can express -the same Counter a using GADT: - - -data Counter a where - NewCounter { _this :: self - , _inc :: self -> self - , _display :: self -> IO () - , tag :: a - } - :: Counter a - - At the moment, record update syntax is only supported for Haskell 98 data types, so the following function does not work: @@ -1386,10 +1378,10 @@ setTag obj t = obj{ tag = t } - + - + Restrictions @@ -1515,7 +1507,7 @@ are convincing reasons to change it. 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:# +Reason: in most cases it would not make sense. For example:; data T = forall a. MkT [a] deriving( Eq ) @@ -1540,206 +1532,775 @@ declarations. Define your own instances! - - + + +Declaring data types with explicit constructor signatures - -Class declarations - - -This section, and the next one, documents GHC's type-class extensions. -There's lots of background in the paper Type -classes: exploring the design space (Simon Peyton Jones, Mark -Jones, Erik Meijer). - - -All the extensions are enabled by the flag. - - - -Multi-parameter type classes - -Multi-parameter type classes are permitted. For example: - - +GHC allows you to declare an algebraic data type by +giving the type signatures of constructors explicitly. For example: - class Collection c a where - union :: c a -> c a -> c a - ...etc. + data Maybe a where + Nothing :: Maybe a + Just :: a -> Maybe a - - - - - -The superclasses of a class declaration - - -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: - - +The form is called a "GADT-style declaration" +because Generalised Algebraic Data Types, described in , +can only be declared using this form. +Notice that GADT-style syntax generalises existential types (). +For example, these two declarations are equivalent: - class Functor (m k) => FiniteMap m k where - ... - - class (Monad m, Monad (t m)) => Transform t m where - lift :: m a -> (t m) a + data Foo = forall a. MkFoo a (a -> Bool) + data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' } - - - -As in Haskell 98, The class hierarchy must be acyclic. However, the definition -of "acyclic" involves only the superclass relationships. For example, -this is OK: - - +Any data type that can be declared in standard Haskell-98 syntax +can also be declared using GADT-style syntax. +The choice is largely stylistic, but GADT-style declarations differ in one important respect: +they treat class constraints on the data constructors differently. +Specifically, if the constructor is given a type-class context, that +context is made available by pattern matching. For example: - class C a where { - op :: D b => a -> b -> b - } - - class C a => D a where { ... } - + data Set a where + MkSet :: Eq a => [a] -> Set a + makeSet :: Eq a => [a] -> Set a + makeSet xs = MkSet (nub xs) -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.) + insert :: a -> Set a -> Set a + insert a (MkSet as) | a `elem` as = MkSet as + | otherwise = MkSet (a:as) + +A use of MkSet as a constructor (e.g. in the definition of makeSet) +gives rise to a (Eq a) +constraint, as you would expect. The new feature is that pattern-matching on MkSet +(as in the definition of insert) makes available an (Eq a) +context. In implementation terms, the MkSet constructor has a hidden field that stores +the (Eq a) dictionary that is passed to MkSet; so +when pattern-matching that dictionary becomes available for the right-hand side of the match. +In the example, the equality dictionary is used to satisfy the equality constraint +generated by the call to elem, so that the type of +insert itself has no Eq constraint. - - - - - - -Class method types - - -Haskell 98 prohibits class method types to mention constraints on the -class type variable, thus: +This behaviour contrasts with Haskell 98's peculiar treament of +contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report). +In Haskell 98 the defintion - class Seq s a where - fromList :: [a] -> s a - elem :: Eq a => a -> s a -> Bool + data Eq a => Set' a = MkSet' [a] -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). -GHC lifts this restriction. - - - - - - - -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, -. - +gives MkSet' the same type as MkSet above. But instead of +making available an (Eq a) constraint, pattern-matching +on MkSet' requires an (Eq a) constraint! +GHC faithfully implements this behaviour, odd though it is. But for GADT-style declarations, +GHC's behaviour is much more useful, as well as much more intuitive. -Functional dependencies are introduced by a vertical bar in the syntax of a -class declaration; e.g. +For example, a possible application of GHC's behaviour is to reify dictionaries: - class (Monad m) => MonadState s m | m -> s where ... + data NumInst a where + MkNumInst :: Num a => NumInst a - class Foo a b c | a b -> c where ... + intInst :: NumInst Int + intInst = MkNumInst + + plus :: NumInst a -> a -> a -> a + plus MkNumInst p q = p + q -There should be more documentation, but there isn't (yet). Yell if you need it. +Here, a value of type NumInst a is equivalent +to an explicit (Num a) dictionary. -Rules for functional dependencies -In a class declaration, all of the class type variables must be reachable (in the sense -mentioned in ) -from the free variables of each method type. -For example: +The rest of this section gives further details about GADT-style data +type declarations. + + + +The result type of each data constructor must begin with the type constructor being defined. +If the result type of all constructors +has the form T a1 ... an, where a1 ... an +are distinct type variables, then the data type is ordinary; +otherwise is a generalised data type (). + + +The type signature of +each constructor is independent, and is implicitly universally quantified as usual. +Different constructors may have different universally-quantified type variables +and different type-class constraints. +For example, this is fine: - class Coll s a where - empty :: s - insert :: s -> a -> s + data T a where + T1 :: Eq b => b -> T b + T2 :: (Show c, Ix c) => c -> [c] -> T c + -is not OK, because the type of empty doesn't mention -a. Functional dependencies can make the type variable -reachable: + +Unlike a Haskell-98-style +data type declaration, the type variable(s) in the "data Set a where" header +have no scope. Indeed, one can write a kind signature instead: - class Coll s a | s -> a where - empty :: s - insert :: s -> a -> s + data Set :: * -> * where ... + +or even a mixture of the two: + + data Foo a :: (* -> *) -> * where ... + +The type variables (if given) may be explicitly kinded, so we could also write the header for Foo +like this: + + data Foo a (b :: * -> *) where ... + -Alternatively Coll might be rewritten + +You can use strictness annotations, in the obvious places +in the constructor type: - class Coll s a where - empty :: s a - insert :: s a -> a -> s a + data Term a where + Lit :: !Int -> Term Int + If :: Term Bool -> !(Term a) -> !(Term a) -> Term a + Pair :: Term a -> Term b -> Term (a,b) + + +You can use a deriving clause on a GADT-style data type +declaration. For example, these two declarations are equivalent + + data Maybe1 a where { + Nothing1 :: Maybe1 a ; + Just1 :: a -> Maybe1 a + } deriving( Eq, Ord ) -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: + data Maybe2 a = Nothing2 | Just2 a + deriving( Eq, Ord ) + + + +You can use record syntax on a GADT-style data type declaration: - class CollE s where - empty :: s - - class CollE s => Coll s a where - insert :: s -> a -> s + data Person where + Adult { name :: String, children :: [Person] } :: Person + Child { name :: String } :: Person +As usual, for every constructor that has a field f, the type of +field f must be the same (modulo alpha conversion). - - + +At the moment, record updates are not yet possible with GADT-style declarations, +so support is limited to record construction, selection and pattern matching. +For exmaple + + aPerson = Adult { name = "Fred", children = [] } - -Background on functional dependencies + shortName :: Person -> Bool + hasChildren (Adult { children = kids }) = not (null kids) + hasChildren (Child {}) = False + + -The following description of the motivation and use of functional dependencies is taken -from the Hugs user manual, reproduced here (with minor changes) by kind -permission of Mark Jones. - - -Consider the following class, intended as part of a -library for collection types: + +As in the case of existentials declared using the Haskell-98-like record syntax +(), +record-selector functions are generated only for those fields that have well-typed +selectors. +Here is the example of that section, in GADT-style syntax: - class Collects e ce where - empty :: ce - insert :: e -> ce -> ce - member :: e -> ce -> Bool +data Counter a where + NewCounter { _this :: self + , _inc :: self -> self + , _display :: self -> IO () + , tag :: a + } + :: Counter a -The type variable e used here represents the element type, while ce is the type -of the container itself. Within this framework, we might want to define -instances of this class for lists or characteristic functions (both of which -can be used to represent collections of any equality type), bit sets (which can -be used to represent collections of characters), or hash tables (which can be -used to represent any collection whose elements have a hash function). Omitting -standard implementation details, this would lead to the following declarations: +As before, only one selector function is generated here, that for tag. +Nevertheless, you can still use all the field names in pattern matching and record construction. + + + + + +Generalised Algebraic Data Types (GADTs) + +Generalised Algebraic Data Types generalise ordinary algebraic data types +by allowing constructors to have richer return types. Here is an example: - instance Eq e => Collects e [e] where ... - instance Eq e => Collects e (e -> Bool) where ... - instance Collects Char BitSet where ... - instance (Hashable e, Collects a ce) - => Collects e (Array Int ce) where ... + data Term a where + Lit :: Int -> Term Int + Succ :: Term Int -> Term Int + IsZero :: Term Int -> Term Bool + If :: Term Bool -> Term a -> Term a -> Term a + Pair :: Term a -> Term b -> Term (a,b) -All this looks quite promising; we have a class and a range of interesting +Notice that the return type of the constructors is not always Term a, as is the +case with ordinary data types. This generality allows us to +write a well-typed eval function +for these Terms: + + eval :: Term a -> a + eval (Lit i) = i + eval (Succ t) = 1 + eval t + eval (IsZero t) = eval t == 0 + eval (If b e1 e2) = if eval b then eval e1 else eval e2 + eval (Pair e1 e2) = (eval e1, eval e2) + +The key point about GADTs is that pattern matching causes type refinement. +For example, in the right hand side of the equation + + eval :: Term a -> a + eval (Lit i) = ... + +the type a is refined to Int. That's the whole point! +A precise specification of the type rules is beyond what this user manual aspires to, +but the design closely follows that described in +the paper Simple +unification-based type inference for GADTs, +(ICFP 2006). +The general principle is this: type refinement is only carried out +based on user-supplied type annotations. +So if no type signature is supplied for eval, no type refinement happens, +and lots of obscure error messages will +occur. However, the refinement is quite general. For example, if we had: + + eval :: Term a -> a -> a + eval (Lit i) j = i+j + +the pattern match causes the type a to be refined to Int (because of the type +of the constructor Lit), and that refinement also applies to the type of j, and +the result type of the case expression. Hence the addition i+j is legal. + + +These and many other examples are given in papers by Hongwei Xi, and +Tim Sheard. There is a longer introduction +on the wiki, +and Ralf Hinze's +Fun with phantom types also has a number of examples. Note that papers +may use different notation to that implemented in GHC. + + +The rest of this section outlines the extensions to GHC that support GADTs. + + +A GADT can only be declared using GADT-style syntax (); +the old Haskell-98 syntax for data declarations always declares an ordinary data type. +The result type of each constructor must begin with the type constructor being defined, +but for a GADT the arguments to the type constructor can be arbitrary monotypes. +For example, in the Term data +type above, the type of each constructor must end with Term ty, but +the ty may not be a type variable (e.g. the Lit +constructor). + + + +You cannot use a deriving clause for a GADT; only for +an ordianary data type. + + + +As mentioned in , record syntax is supported. +For example: + + data Term a where + Lit { val :: Int } :: Term Int + Succ { num :: Term Int } :: Term Int + Pred { num :: Term Int } :: Term Int + IsZero { arg :: Term Int } :: Term Bool + Pair { arg1 :: Term a + , arg2 :: Term b + } :: Term (a,b) + If { cnd :: Term Bool + , tru :: Term a + , fls :: Term a + } :: Term a + +However, for GADTs there is the following additional constraint: +every constructor that has a field f must have +the same result type (modulo alpha conversion) +Hence, in the above example, we cannot merge the num +and arg fields above into a +single name. Although their field types are both Term Int, +their selector functions actually have different types: + + + num :: Term Int -> Term Int + arg :: Term Bool -> Term Int + + + + + + + + + + + + +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.Typeable and Data.Generics respectively, and the +appropriate class must be in scope before it can be mentioned in the deriving clause. + +An instance of Typeable can only be derived if the +data type has seven or fewer type parameters, all of kind *. +The reason for this is that the Typeable class is derived using the scheme +described in + +Scrap More Boilerplate: Reflection, Zips, and Generalised Casts +. +(Section 7.4 of the paper describes the multiple Typeable classes that +are used, and only Typeable1 up to +Typeable7 are provided in the library.) +In other cases, there is nothing to stop the programmer writing a TypableX +class, whose kind suits that of the data type constructor, and +then writing the data type instance by hand. + + + + +Generalised derived instances for newtypes + + +When you define an abstract type using newtype, you may want +the new type to inherit some instances from its representation. In +Haskell 98, you can inherit instances of Eq, Ord, +Enum and Bounded by deriving them, but for any +other classes you have to write an explicit instance declaration. For +example, if you define + + + newtype Dollars = Dollars Int + + +and you want to use arithmetic on Dollars, you have to +explicitly define an instance of Num: + + + instance Num Dollars where + Dollars a + Dollars b = Dollars (a+b) + ... + +All the instance does is apply and remove the newtype +constructor. It is particularly galling that, since the constructor +doesn't appear at run-time, this instance declaration defines a +dictionary which is wholly equivalent to the Int +dictionary, only slower! + + + + Generalising the deriving clause + +GHC now permits such instances to be derived instead, so one can write + + newtype Dollars = Dollars Int deriving (Eq,Show,Num) + + +and the implementation uses the same Num dictionary +for Dollars as for Int. Notionally, the compiler +derives an instance declaration of the form + + + instance Num Int => Num Dollars + + +which just adds or removes the newtype constructor according to the type. + + + +We can also derive instances of constructor classes in a similar +way. For example, suppose we have implemented state and failure monad +transformers, such that + + + instance Monad m => Monad (State s m) + instance Monad m => Monad (Failure m) + +In Haskell 98, we can define a parsing monad by + + type Parser tok m a = State [tok] (Failure m) a + + +which is automatically a monad thanks to the instance declarations +above. With the extension, we can make the parser type abstract, +without needing to write an instance of class Monad, via + + + newtype Parser tok m a = Parser (State [tok] (Failure m) a) + deriving Monad + +In this case the derived instance declaration is of the form + + instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) + + +Notice that, since Monad is a constructor class, the +instance is a partial application of the new type, not the +entire left hand side. We can imagine that the type declaration is +``eta-converted'' to generate the context of the instance +declaration. + + + +We can even derive instances of multi-parameter classes, provided the +newtype is the last class parameter. In this case, a ``partial +application'' of the class appears in the deriving +clause. For example, given the class + + + class StateMonad s m | m -> s where ... + instance Monad m => StateMonad s (State s m) where ... + +then we can derive an instance of StateMonad for Parsers by + + newtype Parser tok m a = Parser (State [tok] (Failure m) a) + deriving (Monad, StateMonad [tok]) + + +The derived instance is obtained by completing the application of the +class to the new type: + + + instance StateMonad [tok] (State [tok] (Failure m)) => + StateMonad [tok] (Parser tok m) + + + + +As a result of this extension, all derived instances in newtype + declarations are treated uniformly (and implemented just by reusing +the dictionary for the representation type), except +Show and Read, which really behave differently for +the newtype and its representation. + + + + A more precise specification + +Derived instance declarations are constructed as follows. Consider the +declaration (after expansion of any type synonyms) + + + newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm) + + +where + + + The ci are partial applications of + classes of the form C t1'...tj', where the arity of C + is exactly j+1. That is, C lacks exactly one type argument. + + + The k is chosen so that ci (T v1...vk) is well-kinded. + + + The type t is an arbitrary type. + + + The type variables vk+1...vn do not occur in t, + nor in the ci, and + + + None of the ci is Read, Show, + 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 t => ci (T v1...vk) + +As an example which does not work, consider + + newtype NonMonad m s = NonMonad (State s m s) deriving Monad + +Here we cannot derive the instance + + instance Monad (State s m) => Monad (NonMonad m) + + +because the type variable s occurs in State s m, +and so cannot be "eta-converted" away. It is a good thing that this +deriving clause is rejected, because NonMonad m is +not, in fact, a monad --- for the same reason. Try defining +>>= with the correct type: you won't be able to. + + + +Notice also that the order of class parameters becomes +important, since we can only derive instances for the last one. If the +StateMonad class above were instead defined as + + + class StateMonad m s | m -> s where ... + + +then we would not have been able to derive an instance for the +Parser type above. We hypothesise that multi-parameter +classes usually have one "main" parameter for which deriving new +instances is most interesting. + +Lastly, all of this applies only for classes other than +Read, Show, Typeable, +and Data, for which the built-in derivation applies (section +4.3.3. of the Haskell Report). +(For the standard classes Eq, Ord, +Ix, and Bounded it is immaterial whether +the standard method is used or the one described here.) + + + + + + +Stand-alone deriving declarations + + +GHC now allows stand-alone deriving declarations, enabled by -fglasgow-exts: + + data Foo a = Bar a | Baz String + + derive instance Eq (Foo a) + +The token "derive" is a keyword only when followed by "instance"; +you can use it as a variable name elsewhere. +The stand-alone syntax is generalised for newtypes in exactly the same +way that ordinary deriving clauses are generalised (). +For example: + + newtype Foo a = MkFoo (State Int a) + + derive instance MonadState Int Foo + +GHC always treats the last parameter of the instance +(Foo in this exmample) as the type whose instance is being derived. + + + + + + + + + +Other type system extensions + + +Class declarations + + +This section, and the next one, documents GHC's type-class extensions. +There's lots of background in the paper Type +classes: exploring the design space (Simon Peyton Jones, Mark +Jones, Erik Meijer). + + +All the extensions are enabled by the flag. + + + +Multi-parameter type classes + +Multi-parameter type classes are permitted. For example: + + + + class Collection c a where + union :: c a -> c a -> c a + ...etc. + + + + + + +The superclasses of a class declaration + + +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: + + + + class Functor (m k) => FiniteMap m k where + ... + + class (Monad m, Monad (t m)) => Transform t m where + lift :: m a -> (t m) a + + + + + +As in Haskell 98, The class hierarchy must be acyclic. However, the definition +of "acyclic" involves only the superclass relationships. For example, +this is OK: + + + + class C a where { + op :: D b => a -> b -> b + } + + class C a => D a where { ... } + + + +Here, C is a superclass of D, but it's OK for a +class operation op of C to mention D. (It +would not be OK for D to be a superclass of C.) + + + + + + + +Class method types + + +Haskell 98 prohibits class method types to mention constraints on the +class type variable, thus: + + class Seq s a where + fromList :: [a] -> s a + elem :: Eq a => a -> s a -> Bool + +The type of elem is illegal in Haskell 98, because it +contains the constraint Eq a, constrains only the +class type variable (in this case a). +GHC lifts this restriction. + + + + + + + +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, +. + + +Functional dependencies are introduced by a vertical bar in the syntax of a +class declaration; e.g. + + class (Monad m) => MonadState s m | m -> s where ... + + class Foo a b c | a b -> c where ... + +There should be more documentation, but there isn't (yet). Yell if you need it. + + +Rules for functional dependencies + +In a class declaration, all of the class type variables must be reachable (in the sense +mentioned in ) +from the free variables of each method type. +For example: + + + class Coll s a where + empty :: s + insert :: s -> a -> s + + +is not OK, because the type of empty doesn't mention +a. Functional dependencies can make the type variable +reachable: + + class Coll s a | s -> a where + empty :: s + insert :: s -> a -> s + + +Alternatively Coll might be rewritten + + + class Coll s a where + empty :: s a + insert :: s a -> a -> s 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: + + + + class CollE s where + empty :: s + + class CollE s => Coll s a where + insert :: s -> a -> s + + + + + + +Background on functional dependencies + +The following description of the motivation and use of functional dependencies is taken +from the Hugs user manual, reproduced here (with minor changes) by kind +permission of Mark Jones. + + +Consider the following class, intended as part of a +library for collection types: + + class Collects e ce where + empty :: ce + insert :: e -> ce -> ce + member :: e -> ce -> Bool + +The type variable e used here represents the element type, while ce is the type +of the container itself. Within this framework, we might want to define +instances of this class for lists or characteristic functions (both of which +can be used to represent collections of any equality type), bit sets (which can +be used to represent collections of characters), or hash tables (which can be +used to represent any collection whose elements have a hash function). Omitting +standard implementation details, this would lead to the following declarations: + + instance Eq e => Collects e [e] where ... + instance Eq e => Collects e (e -> Bool) where ... + instance Collects Char BitSet where ... + instance (Hashable e, Collects a ce) + => Collects e (Array Int ce) where ... + +All this looks quite promising; we have a class and a range of interesting implementations. Unfortunately, there are some serious problems with the class declaration. First, the empty function has an ambiguous type: @@ -1987,7 +2548,7 @@ the context and head of the instance declaration can each consist of arbitrary following rules: -For each assertion in the context: +The Paterson Conditions: for each assertion in the context No type variable has more occurrences in the assertion than in the head The assertion has fewer constructors and variables (taken together @@ -1995,7 +2556,7 @@ For each assertion in the context: -The coverage condition. For each functional dependency, +The Coverage Condition. For each functional dependency, tvsleft -> tvsright, of the class, every type variable in @@ -2007,11 +2568,15 @@ corresponding type in the instance declaration. These restrictions ensure that context reduction terminates: each reduction step makes the problem smaller by at least one -constructor. For example, the following would make the type checker -loop if it wasn't excluded: - - instance C a => C a where ... - +constructor. Both the Paterson Conditions and the Coverage Condition are lifted +if you give the +flag (). +You can find lots of background material about the reason for these +restrictions in the paper +Understanding functional dependencies via Constraint Handling Rules. + + For example, these are OK: instance C Int [a] -- Multiple parameters @@ -2063,11 +2628,6 @@ something more specific does not: op = ... -- Default -You can find lots of background material about the reason for these -restrictions in the paper -Understanding functional dependencies via Constraint Handling Rules. - @@ -2132,8 +2692,8 @@ makes instance inference go into a loop, because it requires the constraint Nevertheless, GHC allows you to experiment 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 +option, both the Paterson Conditions and the Coverage Condition +(described in ) are lifted. 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. @@ -2405,55 +2965,7 @@ territory free in case we need it later. - -For-all hoisting - -It is often convenient to use generalised type synonyms (see ) at the right hand -end of an arrow, thus: - - type Discard a = forall b. a -> b -> a - - g :: Int -> Discard Int - g x y z = x+y - -Simply expanding the type synonym would give - - g :: Int -> (forall b. Int -> b -> Int) - -but GHC "hoists" the forall to give the isomorphic type - - g :: forall b. Int -> Int -> b -> Int - -In general, the rule is this: to determine the type specified by any explicit -user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly -performs the transformation: - - type1 -> forall a1..an. context2 => type2 -==> - forall a1..an. context2 => type1 -> type2 - -(In fact, GHC tries to retain as much synonym information as possible for use in -error messages, but that is a usability issue.) This rule applies, of course, whether -or not the forall comes from a synonym. For example, here is another -valid way to write g's type signature: - - g :: Int -> Int -> forall b. b -> Int - - - -When doing this hoisting operation, GHC eliminates duplicate constraints. For -example: - - type Foo a = (?x::Int) => Bool -> a - g :: Foo (Foo Int) - -means - - g :: (?x::Int) => Bool -> Bool -> Int - - - - + @@ -2861,7 +3373,7 @@ and you'd be right. That is why they are an experimental feature. ================ END OF Linear Implicit Parameters commented out --> - + Explicitly-kinded quantification @@ -2911,847 +3423,584 @@ single lexeme in Haskell. 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. - - - - - -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) - -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 - - 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 arrow. As g2 -shows, the polymorphic type on the left of the function arrow can be overloaded. - - -The function f3 has a rank-3 type; -it has 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 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! - - - - -Examples - - - -In a data or newtype declaration one can quantify -the types of the constructor arguments. Here are several examples: - - - - - -data T a = T1 (forall b. b -> b -> b) a - -data MonadT m = MkMonad { return :: forall a. a -> m a, - bind :: forall a b. m a -> (a -> m b) -> m b - } - -newtype Swizzle = MkSwizzle (Ord a => [a] -> [a]) - - - - - -The constructors have rank-2 types: - - - - - -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 - - - - - -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: - - - data T a = MkT (Either a b) (b -> b) - - -it's just as if you had written this: - - - 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 construct values of types T1, MonadT, Swizzle by applying -the constructor to suitable values, just as usual. For example, - - - - - - 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 - - mkTs :: (forall b. b -> b -> b) -> a -> [T a] - mkTs f x y = [T1 f x, T1 f y] - - - - - -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: - - - - - - f :: T a -> a -> (a, Char) - f (T1 w k) x = (w k x, w 'c' 'd') - - g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b] - g (MkSwizzle s) xs f = s (map f (s xs)) - - 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) - - - - - -In the function h we use the record selectors return -and bind to extract the polymorphic bind and return functions -from the MonadT data structure, rather than using pattern -matching. - - - - -Type inference - - -In general, type inference for arbitrary-rank types is undecidable. -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: - - \ 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. + f :: (Int :: *) -> Int + g :: forall a. a -> (a :: *) + +The syntax is + + atype ::= '(' ctype '::' kind ') + +The parentheses are required. - - + - -Implicit quantification + +Arbitrary-rank polymorphism + -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: - - f :: a -> a - f :: forall a. 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 ... - +Haskell type signatures are implicitly quantified. The new keyword forall +allows us to say exactly what this means. For example: -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 + g :: b -> b -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. - - - - - - -Impredicative polymorphism - -GHC supports impredicative polymorphism. This means -that you can call a polymorphic function at a polymorphic type, and -parameterise data structures over polymorphic types. For example: +means this: - f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) - f (Just g) = Just (g [3], g "hello") - f Nothing = Nothing + g :: forall b. (b -> b) -Notice here that the Maybe type is parameterised by the -polymorphic type (forall a. [a] -> -[a]). - -The technical details of this extension are described in the paper -Boxy types: -type inference for higher-rank types and impredicativity, -which appeared at ICFP 2006. +The two are treated identically. - - - -Lexically scoped type variables - -GHC supports lexically scoped type variables, without -which some type signatures are simply impossible to write. For example: +However, GHC's type system supports arbitrary-rank +explicit universal quantification in +types. +For example, all the following types are legal: -f :: forall a. [a] -> [a] -f xs = ys ++ ys - where - ys :: [a] - ys = reverse xs + f1 :: forall a b. a -> b -> a + g1 :: forall a b. (Ord a, Eq b) => a -> b -> a + + f2 :: (forall a. a->a) -> Int -> Int + g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int + + f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool + + f4 :: Int -> (forall a. a -> a) -The type signature for f brings the type variable a into scope; it scopes over -the entire definition of f. -In particular, it is in scope at the type signature for ys. -In Haskell 98 it is not possible to declare -a type for ys; a major benefit of scoped type variables is that -it becomes possible to do so. +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. -Lexically-scoped type variables are enabled by -. + +The functions f2 and g2 have rank-2 types; +the forall is on the left of a function arrow. As g2 +shows, the polymorphic type on the left of the function arrow can be overloaded. -Note: GHC 6.6 contains substantial changes to the way that scoped type -variables work, compared to earlier releases. Read this section -carefully! - - -Overview - -The design follows the following principles - -A scoped type variable stands for a type variable, and not for -a type. (This is a change from GHC's earlier -design.) -Furthermore, distinct lexical type variables stand for distinct -type variables. This means that every programmer-written type signature -(includin one that contains free scoped type variables) denotes a -rigid type; that is, the type is fully known to the type -checker, and no inference is involved. -Lexical type variables may be alpha-renamed freely, without -changing the program. - + +The function f3 has a rank-3 type; +it has rank-2 types on the left of a function arrow. -A lexically scoped type variable can be bound by: +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: -A declaration type signature () -An expression type signature () -A pattern type signature () -Class and instance declarations () + On the left or right (see f4, for example) +of a function arrow + 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 ) +Of course forall becomes a keyword; you can't use forall as +a type variable any more! + + + +Examples + + -In Haskell, a programmer-written type signature is implicitly quantifed over -its free type variables (Section -4.1.2 -of the Haskel Report). -Lexically scoped type variables affect this implicit quantification rules -as follows: any type variable that is in scope is not universally -quantified. For example, if type variable a is in scope, -then +In a data or newtype declaration one can quantify +the types of the constructor arguments. Here are several examples: + + + + - (e :: a -> a) means (e :: a -> a) - (e :: b -> b) means (e :: forall b. b->b) - (e :: a -> b) means (e :: forall b. a->b) +data T a = T1 (forall b. b -> b -> b) a + +data MonadT m = MkMonad { return :: forall a. a -> m a, + bind :: forall a b. m a -> (a -> m b) -> m b + } + +newtype Swizzle = MkSwizzle (Ord a => [a] -> [a]) - + - + +The constructors have rank-2 types: + + - -Declaration type signatures -A declaration type signature that has explicit -quantification (using forall) brings into scope the -explicitly-quantified -type variables, in the definition of the named function(s). For example: - f :: forall a. [a] -> [a] - f (x:xs) = xs ++ [ x :: a ] +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 "forall a" brings "a" into scope in -the definition of "f". + -This only happens if the quantification in f's type -signature is explicit. For example: + + +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: + - g :: [a] -> [a] - g (x:xs) = xs ++ [ x :: a ] + data T a = MkT (Either a b) (b -> b) -This program will be rejected, because "a" does not scope -over the definition of "f", so "x::a" -means "x::forall a. a" by Haskell's usual implicit -quantification rules. - - - -Expression type signatures +it's just as if you had written this: -An expression type signature that has explicit -quantification (using forall) brings into scope the -explicitly-quantified -type variables, in the annotated expression. For example: - f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool ) + data T a = MkT (forall b. Either a b) (forall b. b -> b) -Here, the type signature forall a. ST s Bool brings the -type variable s into scope, in the annotated expression -(op >>= \(x :: STRef s Int) -> g x). + +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.) - - - -Pattern type signatures -A type signature may occur in any pattern; this is a pattern type -signature. -For example: - - -- f and g assume that 'a' is already in scope - f = \(x::Int, y::a) -> x - g (x::a) = x - h ((x,y) :: (Int,Bool)) = (y,x) - -In the case where all the type variables in the pattern type sigature are -already in scope (i.e. bound by the enclosing context), matters are simple: the -signature simply constrains the type of the pattern in the obvious way. +You construct values of types T1, MonadT, Swizzle by applying +the constructor to suitable values, just as usual. For example, + -There is only one situation in which you can write a pattern type signature that -mentions a type variable that is not already in scope, namely in pattern match -of an existential data constructor. For example: + - data T = forall a. MkT [a] + 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 - k :: T -> T - k (MkT [t::a]) = MkT t3 - where - t3::[a] = [t,t,t] + mkTs :: (forall b. b -> b -> b) -> a -> [T a] + mkTs f x y = [T1 f x, T1 f y] -Here, the pattern type signature (t::a) mentions a lexical type -variable that is not already in scope. Indeed, it cannot already be in scope, -because it is bound by the pattern match. GHC's rule is that in this situation -(and only then), a pattern type signature can mention a type variable that is -not already in scope; the effect is to bring it into scope, standing for the -existentially-bound type variable. + + -If this seems a little odd, we think so too. But we must have -some way to bring such type variables into scope, else we -could not name existentially-bound type variables in subequent type signatures. +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.) + -This is (now) the only situation in which a pattern type -signature is allowed to mention a lexical variable that is not already in -scope. -For example, both f and g would be -illegal if a was not already in scope. +When you use pattern matching, the bound variables may now have +polymorphic types. For example: - - - - + - -Class and instance declarations - -The type variables in the head of a class or instance declaration -scope over the methods defined in the where part. For example: + +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: + + f :: a -> a + f :: forall a. 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 ... + + + +Notice that GHC does not find the innermost possible quantification +point. For example: - class C a where - op :: [a] -> a + f :: (a -> a) -> Int + -- MEANS + f :: forall a. (a -> a) -> Int + -- NOT + f :: (forall a. a -> a) -> Int - op xs = let ys::[a] - ys = reverse xs - in - head ys + + 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. - - -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.Typeable and Data.Generics respectively, and the -appropriate class must be in scope before it can be mentioned in the deriving clause. - -An instance of Typeable can only be derived if the -data type has seven or fewer type parameters, all of kind *. -The reason for this is that the Typeable class is derived using the scheme -described in - -Scrap More Boilerplate: Reflection, Zips, and Generalised Casts -. -(Section 7.4 of the paper describes the multiple Typeable classes that -are used, and only Typeable1 up to -Typeable7 are provided in the library.) -In other cases, there is nothing to stop the programmer writing a TypableX -class, whose kind suits that of the data type constructor, and -then writing the data type instance by hand. + +Impredicative polymorphism + +GHC supports impredicative polymorphism. This means +that you can call a polymorphic function at a polymorphic type, and +parameterise data structures over polymorphic types. For example: + + f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) + f (Just g) = Just (g [3], g "hello") + f Nothing = Nothing + +Notice here that the Maybe type is parameterised by the +polymorphic type (forall a. [a] -> +[a]). + +The technical details of this extension are described in the paper +Boxy types: +type inference for higher-rank types and impredicativity, +which appeared at ICFP 2006. - -Generalised derived instances for newtypes + +Lexically scoped type variables + -When you define an abstract type using newtype, you may want -the new type to inherit some instances from its representation. In -Haskell 98, you can inherit instances of Eq, Ord, -Enum and Bounded by deriving them, but for any -other classes you have to write an explicit instance declaration. For -example, if you define - - - newtype Dollars = Dollars Int - - -and you want to use arithmetic on Dollars, you have to -explicitly define an instance of Num: - - - instance Num Dollars where - Dollars a + Dollars b = Dollars (a+b) - ... +GHC supports lexically scoped type variables, without +which some type signatures are simply impossible to write. For example: + +f :: forall a. [a] -> [a] +f xs = ys ++ ys + where + ys :: [a] + ys = reverse xs -All the instance does is apply and remove the newtype -constructor. It is particularly galling that, since the constructor -doesn't appear at run-time, this instance declaration defines a -dictionary which is wholly equivalent to the Int -dictionary, only slower! +The type signature for f brings the type variable a into scope; it scopes over +the entire definition of f. +In particular, it is in scope at the type signature for ys. +In Haskell 98 it is not possible to declare +a type for ys; a major benefit of scoped type variables is that +it becomes possible to do so. + +Lexically-scoped type variables are enabled by +. +Note: GHC 6.6 contains substantial changes to the way that scoped type +variables work, compared to earlier releases. Read this section +carefully! + +Overview - Generalising the deriving clause +The design follows the following principles + +A scoped type variable stands for a type variable, and not for +a type. (This is a change from GHC's earlier +design.) +Furthermore, distinct lexical type variables stand for distinct +type variables. This means that every programmer-written type signature +(includin one that contains free scoped type variables) denotes a +rigid type; that is, the type is fully known to the type +checker, and no inference is involved. +Lexical type variables may be alpha-renamed freely, without +changing the program. + + -GHC now permits such instances to be derived instead, so one can write - - newtype Dollars = Dollars Int deriving (Eq,Show,Num) - - -and the implementation uses the same Num dictionary -for Dollars as for Int. Notionally, the compiler -derives an instance declaration of the form - - - instance Num Int => Num Dollars - - -which just adds or removes the newtype constructor according to the type. +A lexically scoped type variable can be bound by: + +A declaration type signature () +An expression type signature () +A pattern type signature () +Class and instance declarations () + +In Haskell, a programmer-written type signature is implicitly quantifed over +its free type variables (Section +4.1.2 +of the Haskel Report). +Lexically scoped type variables affect this implicit quantification rules +as follows: any type variable that is in scope is not universally +quantified. For example, if type variable a is in scope, +then + + (e :: a -> a) means (e :: a -> a) + (e :: b -> b) means (e :: forall b. b->b) + (e :: a -> b) means (e :: forall b. a->b) + + -We can also derive instances of constructor classes in a similar -way. For example, suppose we have implemented state and failure monad -transformers, such that - - instance Monad m => Monad (State s m) - instance Monad m => Monad (Failure m) - -In Haskell 98, we can define a parsing monad by - - type Parser tok m a = State [tok] (Failure m) a - + -which is automatically a monad thanks to the instance declarations -above. With the extension, we can make the parser type abstract, -without needing to write an instance of class Monad, via - - newtype Parser tok m a = Parser (State [tok] (Failure m) a) - deriving Monad + +Declaration type signatures +A declaration type signature that has explicit +quantification (using forall) brings into scope the +explicitly-quantified +type variables, in the definition of the named function(s). For example: + + f :: forall a. [a] -> [a] + f (x:xs) = xs ++ [ x :: a ] -In this case the derived instance declaration is of the form - - instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) - - -Notice that, since Monad is a constructor class, the -instance is a partial application of the new type, not the -entire left hand side. We can imagine that the type declaration is -``eta-converted'' to generate the context of the instance -declaration. +The "forall a" brings "a" into scope in +the definition of "f". - - -We can even derive instances of multi-parameter classes, provided the -newtype is the last class parameter. In this case, a ``partial -application'' of the class appears in the deriving -clause. For example, given the class - - - class StateMonad s m | m -> s where ... - instance Monad m => StateMonad s (State s m) where ... - -then we can derive an instance of StateMonad for Parsers by - - newtype Parser tok m a = Parser (State [tok] (Failure m) a) - deriving (Monad, StateMonad [tok]) +This only happens if the quantification in f's type +signature is explicit. For example: + + g :: [a] -> [a] + g (x:xs) = xs ++ [ x :: a ] +This program will be rejected, because "a" does not scope +over the definition of "f", so "x::a" +means "x::forall a. a" by Haskell's usual implicit +quantification rules. + + -The derived instance is obtained by completing the application of the -class to the new type: + +Expression type signatures - - instance StateMonad [tok] (State [tok] (Failure m)) => - StateMonad [tok] (Parser tok m) +An expression type signature that has explicit +quantification (using forall) brings into scope the +explicitly-quantified +type variables, in the annotated expression. For example: + + f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool ) +Here, the type signature forall a. ST s Bool brings the +type variable s into scope, in the annotated expression +(op >>= \(x :: STRef s Int) -> g x). - -As a result of this extension, all derived instances in newtype - declarations are treated uniformly (and implemented just by reusing -the dictionary for the representation type), except -Show and Read, which really behave differently for -the newtype and its representation. - - A more precise specification + +Pattern type signatures -Derived instance declarations are constructed as follows. Consider the -declaration (after expansion of any type synonyms) - - - newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm) - - -where - - - The ci are partial applications of - classes of the form C t1'...tj', where the arity of C - is exactly j+1. That is, C lacks exactly one type argument. - - - The k is chosen so that ci (T v1...vk) is well-kinded. - - - The type t is an arbitrary type. - - - The type variables vk+1...vn do not occur in t, - nor in the ci, and - - - None of the ci is Read, Show, - 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 t => ci (T v1...vk) +A type signature may occur in any pattern; this is a pattern type +signature. +For example: + + -- f and g assume that 'a' is already in scope + f = \(x::Int, y::a) -> x + g (x::a) = x + h ((x,y) :: (Int,Bool)) = (y,x) -As an example which does not work, consider - - newtype NonMonad m s = NonMonad (State s m s) deriving Monad - -Here we cannot derive the instance - - instance Monad (State s m) => Monad (NonMonad m) - - -because the type variable s occurs in State s m, -and so cannot be "eta-converted" away. It is a good thing that this -deriving clause is rejected, because NonMonad m is -not, in fact, a monad --- for the same reason. Try defining ->>= with the correct type: you won't be able to. +In the case where all the type variables in the pattern type sigature are +already in scope (i.e. bound by the enclosing context), matters are simple: the +signature simply constrains the type of the pattern in the obvious way. +There is only one situation in which you can write a pattern type signature that +mentions a type variable that is not already in scope, namely in pattern match +of an existential data constructor. For example: + + data T = forall a. MkT [a] -Notice also that the order of class parameters becomes -important, since we can only derive instances for the last one. If the -StateMonad class above were instead defined as - - - class StateMonad m s | m -> s where ... + k :: T -> T + k (MkT [t::a]) = MkT t3 + where + t3::[a] = [t,t,t] - -then we would not have been able to derive an instance for the -Parser type above. We hypothesise that multi-parameter -classes usually have one "main" parameter for which deriving new -instances is most interesting. +Here, the pattern type signature (t::a) mentions a lexical type +variable that is not already in scope. Indeed, it cannot already be in scope, +because it is bound by the pattern match. GHC's rule is that in this situation +(and only then), a pattern type signature can mention a type variable that is +not already in scope; the effect is to bring it into scope, standing for the +existentially-bound type variable. -Lastly, all of this applies only for classes other than -Read, Show, Typeable, -and Data, for which the built-in derivation applies (section -4.3.3. of the Haskell Report). -(For the standard classes Eq, Ord, -Ix, and Bounded it is immaterial whether -the standard method is used or the one described here.) + +If this seems a little odd, we think so too. But we must have +some way to bring such type variables into scope, else we +could not name existentially-bound type variables in subequent type signatures. + + +This is (now) the only situation in which a pattern type +signature is allowed to mention a lexical variable that is not already in +scope. +For example, both f and g would be +illegal if a was not already in scope. + + - + + +Class and instance declarations + +The type variables in the head of a class or instance declaration +scope over the methods defined in the where part. For example: + + + + class C a where + op :: [a] -> a + + op xs = let ys::[a] + ys = reverse xs + in + head ys + + + Generalised typing of mutually recursive bindings @@ -3815,186 +4064,111 @@ pattern binding must have the same context. For example, this is fine: - - - - - - -Generalised Algebraic Data Types (GADTs) + +Overloaded string literals + -Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you -to give the type signatures of constructors explicitly. For example: + +GHC supports overloaded string literals. Normally a +string literal has type String, but with overloaded string +literals enabled (with -foverloaded-strings) + a string literal has type (IsString a) => a. + + +This means that the usual string syntax can be used, e.g., for packed strings +and other variations of string like types. String literals behave very much +like integer literals, i.e., they can be used in both expressions and patterns. +If used in a pattern the literal with be replaced by an equality test, in the same +way as an integer literal is. + + +The class IsString is defined as: - data Term a where - Lit :: Int -> Term Int - Succ :: Term Int -> Term Int - IsZero :: Term Int -> Term Bool - If :: Term Bool -> Term a -> Term a -> Term a - Pair :: Term a -> Term b -> Term (a,b) +class IsString a where + fromString :: String -> a -Notice that the return type of the constructors is not always Term a, as is the -case with ordinary vanilla data types. Now we can write a well-typed eval function -for these Terms: +The only predefined instance is the obvious one to make strings work as usual: - eval :: Term a -> a - eval (Lit i) = i - eval (Succ t) = 1 + eval t - eval (IsZero t) = eval t == 0 - eval (If b e1 e2) = if eval b then eval e1 else eval e2 - eval (Pair e1 e2) = (eval e1, eval e2) +instance IsString [Char] where + fromString cs = cs -These and many other examples are given in papers by Hongwei Xi, and -Tim Sheard. There is a longer introduction -on the wiki, -and Ralf Hinze's -Fun with phantom types also has a number of examples. Note that papers -may use different notation to that implemented in GHC. +The class IsString is not in scope by default. If you want to mention +it explicitly (for exmaple, to give an instance declaration for it), you can import it +from module GHC.Exts. -The rest of this section outlines the extensions to GHC that support GADTs. -It is far from comprehensive, but the design closely follows that described in -the paper Simple -unification-based type inference for GADTs, -which appeared in ICFP 2006. +Haskell's defaulting mechanism is extended to cover string literals, when is specified. +Specifically: - Data type declarations have a 'where' form, as exemplified above. The type signature of -each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal -Haskell data type declaration, the type variable(s) in the "data Term a where" header -have no scope. Indeed, one can write a kind signature instead: - - data Term :: * -> * where ... - -or even a mixture of the two: - - data Foo a :: (* -> *) -> * where ... - -The type variables (if given) may be explicitly kinded, so we could also write the header for Foo -like this: - - data Foo a (b :: * -> *) where ... - +Each type in a default declaration must be an +instance of Num or of IsString. -There are no restrictions on the type of the data constructor, except that the result -type must begin with the type constructor being defined. For example, in the Term data -type above, the type of each constructor must end with ... -> Term .... +The standard defaulting rule (Haskell Report, Section 4.3.4) +is extended thus: defaulting applies when all the unresolved constraints involve standard classes +or IsString; and at least one is a numeric class +or IsString. - - -You can use record syntax on a GADT-style data type declaration: - - - data Term a where - Lit { val :: Int } :: Term Int - Succ { num :: Term Int } :: Term Int - Pred { num :: Term Int } :: Term Int - IsZero { arg :: Term Int } :: Term Bool - Pair { arg1 :: Term a - , arg2 :: Term b - } :: Term (a,b) - If { cnd :: Term Bool - , tru :: Term a - , fls :: Term a - } :: Term a - -For every constructor that has a field f, (a) the type of -field f must be the same; and (b) the -result type of the constructor must be the same; both modulo alpha conversion. -Hence, in our example, we cannot merge the num and arg -fields above into a -single name. Although their field types are both Term Int, -their selector functions actually have different types: - - - num :: Term Int -> Term Int - arg :: Term Bool -> Term Int - - -At the moment, record updates are not yet possible with GADT, so support is -limited to record construction, selection and pattern matching: - + + + +A small example: - someTerm :: Term Bool - someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } } - - eval :: Term a -> a - eval Lit { val = i } = i - eval Succ { num = t } = eval t + 1 - eval Pred { num = t } = eval t - 1 - eval IsZero { arg = t } = eval t == 0 - eval Pair { arg1 = t1, arg2 = t2 } = (eval t1, eval t2) - eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t) - +module Main where - +import GHC.Exts( IsString(..) ) - -You can use strictness annotations, in the obvious places -in the constructor type: - - data Term a where - Lit :: !Int -> Term Int - If :: Term Bool -> !(Term a) -> !(Term a) -> Term a - Pair :: Term a -> Term b -> Term (a,b) - - +newtype MyString = MyString String deriving (Eq, Show) +instance IsString MyString where + fromString = MyString - -You can use a deriving clause on a GADT-style data type -declaration, but only if the data type could also have been declared in -Haskell-98 syntax. For example, these two declarations are equivalent - - data Maybe1 a where { - Nothing1 :: Maybe1 a ; - Just1 :: a -> Maybe1 a - } deriving( Eq, Ord ) +greet :: MyString -> MyString +greet "hello" = "world" +greet other = other - data Maybe2 a = Nothing2 | Just2 a - deriving( Eq, Ord ) +main = do + print $ greet "hello" + print $ greet "fool" -This simply allows you to declare a vanilla Haskell-98 data type using the -where form without losing the deriving clause. - + + +Note that deriving Eq is necessary for the pattern matching +to work since it gets translated into an equality comparison. + + - -Pattern matching causes type refinement. For example, in the right hand side of the equation - - eval :: Term a -> a - eval (Lit i) = ... - -the type a is refined to Int. (That's the whole point!) -A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper -about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page. + +Type families + - The general principle is this: type refinement is only carried out based on user-supplied type annotations. -So if no type signature is supplied for eval, no type refinement happens, and lots of obscure error messages will -occur. However, the refinement is quite general. For example, if we had: - - eval :: Term a -> a -> a - eval (Lit i) j = i+j - -the pattern match causes the type a to be refined to Int (because of the type -of the constructor Lit, and that refinement also applies to the type of j, and -the result type of the case expression. Hence the addition i+j is legal. + +GHC supports the definition of type families indexed by types. They may be +seen as an extension of Haskell 98's class-based overloading of values to +types. When type families are declared in classes, they are also known as +associated types. - - + +There are two forms of type families: data families and type synonym families. +Currently, only the former are fully implemented, while we are still working +on the latter. As a result, the specification of the language extension is +also still to some degree in flux. Hence, a more detailed description of +the language extension and its use is currently available +from the Haskell +wiki page on type families. The material will be moved to this user's +guide when it has stabilised. - -Notice that GADTs generalise existential types. For example, these two declarations are equivalent: - - data T a = forall b. MkT b (b->a) - data T' a where { MKT :: b -> (b->a) -> T' a } - + +Type families are enabled by the flag . - - + + + + + @@ -4103,6 +4277,14 @@ Tim Sheard is going to expand it.) (It would make sense to do so, but it's hard to implement.) + + Furthermore, you can only run a function at compile time if it is imported + from another module that is not part of a mutually-recursive group of modules + that includes the module currently being compiled. For example, when compiling module A, + you can only run Template Haskell functions imported from B if B does not import A (directly or indirectly). + The reason should be clear: to run B we must compile and run A, but we are currently type-checking A. + + The flag -ddump-splices shows the expansion of all top-level splices as they happen. @@ -4722,7 +4904,7 @@ Because the preprocessor targets Haskell (rather than Core), - + Bang patterns <indexterm><primary>Bang patterns</primary></indexterm> @@ -4737,7 +4919,7 @@ than the material below. Bang patterns are enabled by the flag . - + Informal description of bang patterns @@ -4792,7 +4974,7 @@ is part of the syntax of let bindings. - + Syntax and semantics @@ -4866,7 +5048,7 @@ a module. - + Assertions <indexterm><primary>Assertions</primary></indexterm> @@ -5835,12 +6017,6 @@ The following are good consumers: - length - - - - - ++ (on its first argument)