X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=41bba186e9805d95278f5e04755f90e1ca0cf69f;hb=1ed54200532d9a9b1b58ac914dae28c1ecb48699;hp=7e085836e590386c98f5f5e957e2fae01dc6be54;hpb=395f018ba53d1bc09a03aa5083032dc96c911c6c;p=ghc-hetmet.git diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 7e08583..41bba18 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -106,9 +106,7 @@ documentation describes all the libraries that come with GHC. This option enables the language extension defined in the - Haskell 98 Foreign Function Interface Addendum plus deprecated - syntax of previous versions of the FFI for backwards - compatibility. + Haskell 98 Foreign Function Interface Addendum. New reserved words: foreign. @@ -116,7 +114,7 @@ documentation describes all the libraries that come with GHC. - ,: + ,: These two flags control how generalisation is done. @@ -941,14 +939,10 @@ definitions; you must define such a function in prefix form. - -Type system extensions + +Extensions to data types and type synonyms - - -Data types and type synonyms - - + Data types with no constructors With the flag, GHC lets you declare @@ -966,9 +960,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, classes, and type variables @@ -1035,9 +1029,9 @@ to be written infix, very much like expressions. More specifically: - + - + Liberalised type synonyms @@ -1127,10 +1121,10 @@ this will be rejected: because GHC does not allow unboxed tuples on the left of a function arrow. - + - + Existentially quantified data constructors @@ -1311,7 +1305,7 @@ universal quantification earlier. - + Record Constructors @@ -1363,20 +1357,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: @@ -1517,7 +1497,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 ) @@ -1543,11 +1523,580 @@ declarations. Define your own instances! + + + + + +Declaring data types with explicit constructor signatures + +GHC allows you to declare an algebraic data type by +giving the type signatures of constructors explicitly. For example: + + data Maybe a where + Nothing :: Maybe a + Just :: a -> Maybe a + +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: + + data Foo = forall a. MkFoo a (a -> Bool) + data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' } + + +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: + + data Set a where + MkSet :: Eq a => [a] -> Set a + + makeSet :: Eq a => [a] -> Set a + makeSet xs = MkSet (nub xs) + + 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. + +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 + + data Eq a => Set' a = MkSet' [a] + +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. + +For example, a possible application of GHC's behaviour is to reify dictionaries: + + data NumInst a where + MkNumInst :: Num a => NumInst a + + intInst :: NumInst Int + intInst = MkNumInst + + plus :: NumInst a -> a -> a -> a + plus MkNumInst p q = p + q + +Here, a value of type NumInst a is equivalent +to an explicit (Num a) dictionary. + + + +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: + + data T a where + T1 :: Eq b => b -> T b + T2 :: (Show c, Ix c) => c -> [c] -> T c + + + + +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: + + 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 ... + + + + + +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) + + + + +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 ) + + data Maybe2 a = Nothing2 | Just2 a + deriving( Eq, Ord ) + + + + +You can use record syntax on a GADT-style data type declaration: + + + 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 = [] } + + shortName :: Person -> Bool + hasChildren (Adult { children = kids }) = not (null kids) + hasChildren (Child {}) = False + + + + +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: + +data Counter a where + NewCounter { _this :: self + , _inc :: self -> self + , _display :: self -> IO () + , tag :: a + } + :: Counter a + +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: + + 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) + +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 @@ -2384,79 +2933,31 @@ universally quantified type variable b: The next type is illegal because the constraint Eq b does not -mention a: - - - - forall a. Eq b => burble - - - -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. - - - - - - - - - - -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 +mention a: + + - g :: (?x::Int) => Bool -> Bool -> Int + forall a. Eq b => burble + + +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. + + + + + + + @@ -2957,6 +3458,8 @@ For example, all the following types are legal: g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool + + f4 :: Int -> (forall a. a -> a) Here, f1 and g1 are rank-1 types, and can be written in standard Haskell (e.g. f1 :: a->b->a). @@ -2979,7 +3482,8 @@ 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 left or right (see f4, for example) +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 @@ -2987,14 +3491,6 @@ 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! @@ -3301,6 +3797,7 @@ changing the program. 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 () @@ -3352,6 +3849,23 @@ quantification rules. + +Expression type signatures + +An expression type signature that has explicit +quantification (using forall) brings into scope the +explicitly-quantified +type variables, in the annotated expression. For example: + + 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). + + + + Pattern type signatures @@ -3360,7 +3874,7 @@ signature. For example: -- f and g assume that 'a' is already in scope - f = \(x::Int, y) -> x + f = \(x::Int, y::a) -> x g (x::a) = x h ((x,y) :: (Int,Bool)) = (y,x) @@ -3403,314 +3917,82 @@ 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 - - - - - - - -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 + + + +Class and instance declarations -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 +The type variables in the head of a class or instance declaration +scope over the methods defined in the where part. For example: - - 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.) + + class C a where + op :: [a] -> a + + op xs = let ys::[a] + ys = reverse xs + in + head ys + + Generalised typing of mutually recursive bindings @@ -3777,178 +4059,6 @@ pattern binding must have the same context. For example, this is fine: - - - -Generalised Algebraic Data Types - -Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you -to give the type signatures of constructors explicitly. For example: - - 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) - -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: - - 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) - -These and many other examples are given in papers by Hongwei Xi, and Tim Sheard. - - -The rest of this section outlines the extensions to GHC that support GADTs. -It is far from comprehensive, but the design closely follows that described in -the paper Simple -unification-based type inference for GADTs, -which appeared in ICFP 2006. - - - Data type declarations have a 'where' form, as exemplified above. The type signature of -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 ... - - - - -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 .... - - - -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: - - - 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) - - - - - -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) - - - - -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 :: Maybe a ; - Just1 :: a -> Maybe a - } deriving( Eq, Ord ) - - data Maybe2 a = Nothing2 | Just2 a - deriving( Eq, Ord ) - -This simply allows you to declare a vanilla Haskell-98 data type using the -where form without losing the deriving clause. - - - -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. - - 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. - - - - - -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 } - - - - - - @@ -4761,7 +4871,7 @@ f !x = 3 Is this a definition of the infix function "(!)", or of the "f" with a bang pattern? GHC resolves this -ambiguity inf favour of the latter. If you want to define +ambiguity in favour of the latter. If you want to define (!) with bang-patterns enabled, you have to do so using prefix notation: @@ -6084,6 +6194,22 @@ r) -> described in this section. All are exported by GHC.Exts. + The <literal>seq</literal> function + +The function seq is as described in the Haskell98 Report. + + seq :: a -> b -> b + +It evaluates its first argument to head normal form, and then returns its +second argument as the result. The reason that it is documented here is +that, despite seq's polymorphism, its +second argument can have an unboxed type, or +can be an unboxed tuple; for example (seq x 4#) +or (seq x (# p,q #)). This requires b +to be instantiated to an unboxed type, which is not usually allowed. + + + The <literal>inline</literal> function The inline function is somewhat experimental. @@ -6142,6 +6268,11 @@ If lazy were not lazy, par would look strict in y which would defeat the whole purpose of par. + +Like seq, the argument of lazy can have +an unboxed type. + + The <literal>unsafeCoerce#</literal> function @@ -6157,7 +6288,14 @@ It is generally used when you want to write a program that you know is well-typed, but where Haskell's type system is not expressive enough to prove that it is well typed. + +The argument to unsafeCoerce# can have unboxed types, +although extremely bad things will happen if you coerce a boxed type +to an unboxed type. + + +