X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=36bb71ce71a03185c8cfb1a3239e899a1ed5e0d8;hb=1f28aaa6116d9cb90966b1bb6cdcbe52fe938867;hp=f8ea3c72645da34b71d9bbea37386246c21f3dc6;hpb=90bbfd9f775c1018d6d5c4a9df7c3b277bb89e3d;p=ghc-hetmet.git
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index f8ea3c7..36bb71c 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.
@@ -243,6 +241,14 @@ documentation describes all the libraries that come with GHC.
+
+
+ Enables overloaded string literals (see ).
+
+
+
+ Enables lexically-scoped type variables (see .GHC comes with a large collection of libraries arranged
- hierarchically; see the accompanying library documentation.
- There is an ongoing project to create and maintain a stable set
- of core libraries used by several Haskell
- compilers, and the libraries that GHC comes with represent the
- current status of that project. For more details, see Haskell
- Libraries.
-
+ hierarchically; see the accompanying library
+ documentation. More libraries to install are available
+ from HackageDB.
@@ -622,7 +625,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
@@ -647,7 +650,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
@@ -941,14 +944,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 constructorsWith the flag, GHC lets you declare
@@ -962,13 +961,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
@@ -1035,9 +1034,9 @@ to be written infix, very much like expressions. More specifically:
-
+
-
+Liberalised type synonyms
@@ -1127,10 +1126,10 @@ this will be rejected:
because GHC does not allow unboxed tuples on the left of a function arrow.
-
+
-
+Existentially quantified data constructors
@@ -1224,7 +1223,7 @@ that collection of packages in a uniform manner. You can express
quite a bit of object-oriented-like programming this way.
-
+Why existential?
@@ -1247,9 +1246,9 @@ But Haskell programmers can safely think of the ordinary
adding a new existential quantification construct.
-
+
-
+Type classes
@@ -1309,9 +1308,9 @@ Notice the way that the syntax fits smoothly with that used for
universal quantification earlier.
-
+
-
+Record Constructors
@@ -1328,7 +1327,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
@@ -1363,20 +1362,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:
@@ -1388,10 +1373,10 @@ setTag obj t = obj{ tag = t }
-
+
-
+Restrictions
@@ -1513,41 +1498,610 @@ are convincing reasons to change it.
-
- You can't use deriving to define instances of a
-data type with existentially quantified data constructors.
+
+ You can't use deriving to define instances of a
+data type with existentially quantified data constructors.
+
+Reason: in most cases it would not make sense. For example:;
+
+
+data T = forall a. MkT [a] deriving( Eq )
+
+
+To derive Eq in the standard way we would need to have equality
+between the single component of two MkT constructors:
+
+
+instance Eq T where
+ (MkT a) == (MkT b) = ???
+
+
+But a and b have distinct types, and so can't be compared.
+It's just about possible to imagine examples in which the derived instance
+would make sense, but it seems altogether simpler simply to prohibit such
+declarations. Define your own instances!
+
+
+
+
+
+
+
+
+
+
+
+
+
+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 Typeable and Data
+
+
+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 sameNum 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.)
+
+
+
+
-Reason: in most cases it would not make sense. For example:#
+
+Stand-alone deriving declarations
+
+GHC now allows stand-alone deriving declarations, enabled by -fglasgow-exts:
-data T = forall a. MkT [a] deriving( Eq )
-
-
-To derive Eq in the standard way we would need to have equality
-between the single component of two MkT constructors:
+ data Foo a = Bar a | Baz String
-
-instance Eq T where
- (MkT a) == (MkT b) = ???
+ 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)
-But a and b have distinct types, and so can't be compared.
-It's just about possible to imagine examples in which the derived instance
-would make sense, but it seems altogether simpler simply to prohibit such
-declarations. Define your own instances!
-
-
-
-
-
+ 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 extensionsClass declarations
@@ -1989,7 +2543,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 headThe assertion has fewer constructors and variables (taken together
@@ -1997,7 +2551,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
@@ -2009,11 +2563,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
@@ -2065,11 +2623,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.
-
@@ -2134,8 +2687,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.
@@ -2407,54 +2960,6 @@ 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
-
-
-
@@ -2863,7 +3368,7 @@ and you'd be right. That is why they are an experimental feature.
================ END OF Linear Implicit Parameters commented out -->
-
+Explicitly-kinded quantification
@@ -2957,6 +3462,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,22 +3486,14 @@ 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 )
+ 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 )
-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 +3800,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 +3852,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
@@ -3430,285 +3947,55 @@ alternative in h is a.
There are a couple of syntactic wrinkles. First, notice that all three
examples would parse quite differently with parentheses:
-
- {- f assumes that 'a' is already in scope -}
- f x (y :: [a]) = [x,y,x]
-
- g = \ (x :: [Int]) -> [3,4]
-
- h :: forall a. [a] -> a
- h xs = case xs of
- ((y:ys) :: a) -> y
-
-Now the signature is on the pattern; and
-h would certainly be ill-typed (since the pattern
-(y:ys) cannot have the type a.
-
-Second, to avoid ambiguity, the type after the “::” in a result
-pattern signature on a lambda or case must be atomic (i.e. a single
-token or a parenthesised type of some sort). To see why,
-consider how one would parse this:
-
- \ x :: a -> b -> x
-
-
-
-
- -->
-
-
-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 Typeable and Data
-
-
-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 sameNum 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])
-
+
+ {- f assumes that 'a' is already in scope -}
+ f x (y :: [a]) = [x,y,x]
-The derived instance is obtained by completing the application of the
-class to the new type:
+ g = \ (x :: [Int]) -> [3,4]
-
- instance StateMonad [tok] (State [tok] (Failure m)) =>
- StateMonad [tok] (Parser tok m)
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ ((y:ys) :: a) -> y
-
-
+Now the signature is on the pattern; and
+h would certainly be ill-typed (since the pattern
+(y:ys) cannot have the type a.
-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.
+Second, to avoid ambiguity, the type after the “::” in a result
+pattern signature on a lambda or case must be atomic (i.e. a single
+token or a parenthesised type of some sort). To see why,
+consider how one would parse this:
+
+ \ x :: a -> b -> x
+
- 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)
-
+
+Class and instance declarations
+
-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)
-
+The type variables in the head of a class or instance declaration
+scope over the methods defined in the where part. For example:
-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 C a where
+ op :: [a] -> a
-
- class StateMonad m s | m -> s where ...
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
-
-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.)
+
Generalised typing of mutually recursive bindings
@@ -3772,181 +4059,84 @@ pattern binding must have the same context. For example, this is fine:
-
-
-
-
-
-
-Generalised Algebraic Data Types
+
+Overloaded string literals
+
-Generalised Algebraic Data Types (GADTs) 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.
+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 ...
-
-
-
-
-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 ....
+Each type in a default declaration must be an
+instance of Numor of 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:
-
-
- 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)
-
-
+The standard defaulting rule (Haskell Report, Section 4.3.4)
+is extended thus: defaulting applies when all the unresolved constraints involve standard classes
+orIsString; and at least one is a numeric class
+orIsString.
-
-
-You can use strictness annotations, in the obvious places
-in the constructor type:
+
+
+
+A small example:
- 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)
-
-
+module Main where
-
-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 )
+import GHC.Exts( IsString(..) )
- 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.
-
+newtype MyString = MyString String deriving (Eq, Show)
+instance IsString MyString where
+ fromString = MyString
-
-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.
+greet :: MyString -> MyString
+greet "hello" = "world"
+greet other = other
- 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
+main = do
+ print $ greet "hello"
+ print $ greet "fool"
-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.
-
-
+
+Note that deriving Eq is necessary for the pattern matching
+to work since it gets translated into an equality comparison.
+
-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 }
-
-
-
-
-
+
+
@@ -4055,6 +4245,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.
@@ -4674,7 +4872,7 @@ Because the preprocessor targets Haskell (rather than Core),
-
+Bang patterns
Bang patterns
@@ -4689,7 +4887,7 @@ than the material below.
Bang patterns are enabled by the flag .
-
+Informal description of bang patterns
@@ -4744,7 +4942,7 @@ is part of the syntax of let bindings.
-
+Syntax and semantics
@@ -4759,7 +4957,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:
@@ -4818,7 +5016,7 @@ a module.
-
+Assertions
Assertions
@@ -5787,12 +5985,6 @@ The following are good consumers:
- length
-
-
-
-
-++ (on its first argument)
@@ -6082,6 +6274,22 @@ r) ->
described in this section. All are exported by
GHC.Exts.
+The seq 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 inline function
The inline function is somewhat experimental.
@@ -6140,6 +6348,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 unsafeCoerce# function
@@ -6155,7 +6368,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.
+
+
+