X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=6dfda6b84fbeee125d1af01fff7ed64496cfb7b4;hb=586149353a755cf7ba7c0bd499a397c3c8230839;hp=319104e108a4937e7f1520f7c43b35a61348c5e6;hpb=d4f8ccee287199f4ac34321f0fad64316950fc25;p=ghc-hetmet.git
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 319104e..6dfda6b 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,11 +114,22 @@ documentation describes all the libraries that come with GHC.
- :
-
+ ,:
+
+
+ These two flags control how generalisation is done.
+ See .
+
+
+
+
+
+
+ :
+
- Switch off the Haskell 98 monomorphism restriction.
+ Use GHCi's extended default rules in a regular module ().
Independent of the
flag.
@@ -140,7 +149,7 @@ documentation describes all the libraries that come with GHC.
-
+
@@ -611,13 +620,13 @@ 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
Just val2 -> val1 + val2
where
- fail = val1 + val2
+ fail = var1 + var2
@@ -636,7 +645,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
@@ -894,18 +903,46 @@ fromInteger :: Integer -> Bool -> Bool
you should be all right.
-
+
+Postfix operators
-
-
-Type system extensions
+
+GHC allows a small extension to the syntax of left operator sections, which
+allows you to define postfix operators. The extension is this: the left section
+
+ (e !)
+
+is equivalent (from the point of view of both type checking and execution) to the expression
+
+ ((!) e)
+
+(for any expression e and operator (!).
+The strict Haskell 98 interpretation is that the section is equivalent to
+
+ (\y -> (!) e y)
+
+That is, the operator must be a function of two arguments. GHC allows it to
+take only one argument, and that in turn allows you to write the function
+postfix.
+
+Since this extension goes beyond Haskell 98, it should really be enabled
+by a flag; but in fact it is enabled all the time. (No Haskell 98 programs
+change their behaviour, of course.)
+
+The extension does not extend to the left-hand side of function
+definitions; you must define such a function in prefix form.
+
+
+
+
-
-Data types and type synonyms
+
+
+Extensions to data types and type synonyms
-
+Data types with no constructorsWith the flag, GHC lets you declare
@@ -923,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
@@ -992,9 +1029,9 @@ to be written infix, very much like expressions. More specifically:
-
+
-
+Liberalised type synonyms
@@ -1084,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
@@ -1268,7 +1305,7 @@ universal quantification earlier.
-
+Record Constructors
@@ -1320,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:
@@ -1474,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 )
@@ -1500,199 +1523,768 @@ 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 = [] }
+ shortName :: Person -> Bool
+ hasChildren (Adult { children = kids }) = not (null kids)
+ hasChildren (Child {}) = False
+
+
-
-Background on functional dependencies
+
+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.
+
+
+
-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:
+
+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:
- class Collects e ce where
- empty :: ce
- insert :: e -> ce -> ce
- member :: e -> ce -> Bool
+ 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)
-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:
+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:
- instance Eq e => Collects e [e] where ...
+ 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.)
+
+
+
+
+
+
+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)
@@ -2022,6 +2614,11 @@ 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.
+
@@ -2090,7 +2687,7 @@ option, you can use arbitrary
types in both an instance context and instance head. Termination is ensured by having a
fixed-depth recursion stack. If you exceed the stack depth you get a
sort of backtrace, and the opportunity to increase the stack depth
-with N.
+with N.
@@ -2107,7 +2704,9 @@ can be modified by two flags:
and
-fallow-incoherent-instances
-, as this section discusses.
+, as this section discusses. Both these
+flags are dynamic flags, and can be set on a per-module basis, using
+an OPTIONS_GHC pragma if desired ().
When GHC tries to resolve, say, the constraint C Int Bool,
it tries to match every instance declaration against the
@@ -2176,8 +2775,20 @@ some other constraint. But if the instance declaration was compiled with
check for that declaration.
-All this makes it possible for a library author to design a library that relies on
-overlapping instances without the library client having to know.
+These rules make it possible for a library author to design a library that relies on
+overlapping instances without the library client having to know.
+
+
+If an instance declaration is compiled without
+,
+then that instance can never be overlapped. This could perhaps be
+inconvenient. Perhaps the rule should instead say that the
+overlapping instance declaration should be compiled in
+this way, rather than the overlapped one. Perhaps overlap
+at a usage site should be permitted regardless of how the instance declarations
+are compiled, if the flag is
+used at the usage site. (Mind you, the exact usage site can occasionally be
+hard to pin down.) We are interested to receive feedback on these points.
The flag implies the
flag, but not vice versa.
@@ -2345,54 +2956,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
-
-
-
@@ -2464,7 +3027,7 @@ function that called it. For example, our sort function might
to pick out the least value in a list:
least :: (?cmp :: a -> a -> Bool) => [a] -> a
- least xs = fst (sort xs)
+ least xs = head (sort xs)
Without lifting a finger, the ?cmp parameter is
propagated to become a parameter of least as well. With explicit
@@ -2624,6 +3187,11 @@ inner binding of ?x, so (f 9) will return
+
+
Explicitly-kinded quantification
@@ -2888,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).
@@ -2910,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
@@ -2918,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!
@@ -3156,670 +3721,278 @@ The latter produces an illegal type, which you might think is silly,
but at least the rule is simple. If you want the latter type, you
can write your for-alls explicitly. Indeed, doing so is strongly advised
for rank-2 types.
-
-
-
-
-
-
-
-
-Scoped type variables
-
-
-
-A lexically scoped type variable can be bound by:
-
-A declaration type signature ()
-A pattern type signature ()
-A result type signature ()
-
-For example:
-
-f (xs::[a]) = ys ++ ys
- where
- ys :: [a]
- ys = reverse xs
-
-The pattern (xs::[a]) includes a type signature for xs.
-This brings the type variable a into scope; it scopes over
-all the patterns and right hand sides for this equation for f.
-In particular, it is in scope at the type signature for y.
-
-
-
-At ordinary type signatures, such as that for ys, any type variables
-mentioned in the type signature that are not in scope are
-implicitly universally quantified. (If there are no type variables in
-scope, all type variables mentioned in the signature are universally
-quantified, which is just as in Haskell 98.) In this case, since a
-is in scope, it is not universally quantified, so the type of ys is
-the same as that of xs. In Haskell 98 it is not possible to declare
-a type for ys; a major benefit of scoped type variables is that
-it becomes possible to do so.
-
-
-
-Scoped type variables are implemented in both GHC and Hugs. Where the
-implementations differ from the specification below, those differences
-are noted.
-
-
-
-So much for the basic idea. Here are the details.
-
-
-
-What a scoped type variable means
-
-A lexically-scoped type variable is simply
-the name for a type. The restriction it expresses is that all occurrences
-of the same name mean the same type. For example:
-
- f :: [Int] -> Int -> Int
- f (xs::[a]) (y::a) = (head xs + y) :: a
-
-The pattern type signatures on the left hand side of
-f express the fact that xs
-must be a list of things of some type a; and that y
-must have this same type. The type signature on the expression (head xs)
-specifies that this expression must have the same type a.
-There is no requirement that the type named by "a" is
-in fact a type variable. Indeed, in this case, the type named by "a" is
-Int. (This is a slight liberalisation from the original rather complex
-rules, which specified that a pattern-bound type variable should be universally quantified.)
-For example, all of these are legal:
-
-
- t (x::a) (y::a) = x+y*2
-
- f (x::a) (y::b) = [x,y] -- a unifies with b
-
- g (x::a) = x + 1::Int -- a unifies with Int
-
- h x = let k (y::a) = [x,y] -- a is free in the
- in k x -- environment
-
- k (x::a) True = ... -- a unifies with Int
- k (x::Int) False = ...
-
- w :: [b] -> [b]
- w (x::a) = x -- a unifies with [b]
-
-
-
-
-
-Scope and implicit quantification
-
-
-
-
-
-
-
-All the type variables mentioned in a pattern,
-that are not already in scope,
-are brought into scope by the pattern. We describe this set as
-the type variables bound by the pattern.
-For example:
-
- f (x::a) = let g (y::(a,b)) = fst y
- in
- g (x,True)
-
-The pattern (x::a) brings the type variable
-a into scope, as well as the term
-variable x. The pattern (y::(a,b))
-contains an occurrence of the already-in-scope type variable a,
-and brings into scope the type variable b.
-
-
-
-
-
-The type variable(s) bound by the pattern have the same scope
-as the term variable(s) bound by the pattern. For example:
-
- let
- f (x::a) = <...rhs of f...>
- (p::b, q::b) = (1,2)
- in <...body of let...>
-
-Here, the type variable a scopes over the right hand side of f,
-just like x does; while the type variable b scopes over the
-body of the let, and all the other definitions in the let,
-just like p and q do.
-Indeed, the newly bound type variables also scope over any ordinary, separate
-type signatures in the let group.
-
-
-
-
-
-
-The type variables bound by the pattern may be
-mentioned in ordinary type signatures or pattern
-type signatures anywhere within their scope.
-
-
-
-
-
-
- In ordinary type signatures, any type variable mentioned in the
-signature that is in scope is not universally quantified.
-
-
-
-
-
-
-
- Ordinary type signatures do not bring any new type variables
-into scope (except in the type signature itself!). So this is illegal:
-
-
- f :: a -> a
- f x = x::a
-
-
-It's illegal because a is not in scope in the body of f,
-so the ordinary signature x::a is equivalent to x::forall a.a;
-and that is an incorrect typing.
-
-
-
-
-
-
-The pattern type signature is a monotype:
-
-
-
-
-A pattern type signature cannot contain any explicit forall quantification.
-
-
-
-The type variables bound by a pattern type signature can only be instantiated to monotypes,
-not to type schemes.
-
-
-
-There is no implicit universal quantification on pattern type signatures (in contrast to
-ordinary type signatures).
-
-
-
-
-
-
-
-
-
-The type variables in the head of a class or instance declaration
-scope over the methods defined in the where part. For example:
-
-
-
- class C a where
- op :: [a] -> a
-
- op xs = let ys::[a]
- ys = reverse xs
- in
- head ys
-
-
-
-(Not implemented in Hugs yet, Dec 98).
-
-
-
-
-
-
-
-
-
-
-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 ]
-
-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:
-
- 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.
-
-
-
-
-Where a pattern type signature can occur
-
-
-A pattern type signature can occur in any pattern. For example:
-
-
-
-
-A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
-
-
-
- f ((x,y)::(a,b)) = (y,x) :: (b,a)
-
-
-
-
-
-
-
-
- Pattern type signatures, including the result part, can be used
-in lambda abstractions:
-
-
- (\ (x::a, y) :: a -> x)
-
-
-
-
-
-
- Pattern type signatures, including the result part, can be used
-in case expressions:
-
-
- case e of { ((x::a, y) :: (a,b)) -> x }
-
-
-Note that the -> symbol in a case alternative
-leads to difficulties when parsing a type signature in the pattern: in
-the absence of the extra parentheses in the example above, the parser
-would try to interpret the -> as a function
-arrow and give a parse error later.
-
-
-
-
-
-
-
-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
-
-
-
-
-
-
-
-
-
- Pattern type signatures can bind existential type variables.
-For example:
-
-
-
- data T = forall a. MkT [a]
-
- f :: T -> T
- f (MkT [t::a]) = MkT t3
- where
- t3::[a] = [t,t,t]
-
-
-
-
-
-
-
-
-
-
-Pattern type signatures
-can be used in pattern bindings:
+
+
+
-
- f x = let (y, z::a) = x in ...
- f1 x = let (y, z::Int) = x in ...
- f2 (x::(Int,a)) = let (y, z::a) = x in ...
- f3 :: (b->b) = \x -> x
-
-In all such cases, the binding is not generalised over the pattern-bound
-type variables. Thus f3 is monomorphic; f3
-has type b -> b for some type b,
-and notforall b. b -> b.
-In contrast, the binding
+
+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:
- f4 :: b->b
- f4 = \x -> x
+ f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+ f (Just g) = Just (g [3], g "hello")
+ f Nothing = Nothing
-makes a polymorphic function, but b is not in scope anywhere
-in f4's scope.
-
+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.
-Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures. The two can be used independently or together.
-
-
+
-
-Result type signatures
+
+Lexically scoped type variables
+
-The result type of a function can be given a signature, thus:
-
-
+GHC supports lexically scoped type variables, without
+which some type signatures are simply impossible to write. For example:
- f (x::a) :: [a] = [x,x,x]
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
+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
-The final :: [a] after all the patterns gives a signature to the
-result type. Sometimes this is the only way of naming the type variable
-you want:
-
-
-
- f :: Int -> [a] -> [a]
- f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
- in \xs -> map g (reverse xs `zip` xs)
-
-
+The 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 type variables bound in a result type signature scope over the right hand side
-of the definition. However, consider this corner-case:
-
- rev1 :: [a] -> [a] = \xs -> reverse xs
-
- foo ys = rev (ys::[a])
-
-The signature on rev1 is considered a pattern type signature, not a result
-type signature, and the type variables it binds have the same scope as rev1
-itself (i.e. the right-hand side of rev1 and the rest of the module too).
-In particular, the expression (ys::[a]) is OK, because the type variable a
-is in scope (otherwise it would mean (ys::forall a.[a]), which would be rejected).
+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 ()
+
-As mentioned above, rev1 is made monomorphic by this scoping rule.
-For example, the following program would be rejected, because it claims that rev1
-is polymorphic:
+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
- rev1 :: [b] -> [b]
- rev1 :: [a] -> [a] = \xs -> reverse xs
+ (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)
-
-Result type signatures are not yet implemented in Hugs.
-
-
-
-
-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.
+
+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 ]
+
+The "forall a" brings "a" into scope in
+the definition of "f".
-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.
+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.
-
-
-
-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:
+
+Expression type signatures
-
- instance Num Dollars where
- Dollars a + Dollars b = Dollars (a+b)
- ...
+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 )
-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!
+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).
+
- Generalising the deriving clause
+
+Pattern type signatures
-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.
+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.
+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]
-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
+ k :: T -> T
+ k (MkT [t::a]) = MkT t3
+ where
+ t3::[a] = [t,t,t]
-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.
+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.
-
-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)
-
+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.
-
-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.
+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.
+
+
- A more precise specification
-
-Derived instance declarations are constructed as follows. Consider the
-declaration (after expansion of any type synonyms)
+
+
+
+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
@@ -3886,190 +4059,31 @@ 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 extensions to GHC are these:
-
-
- 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 }
-
-
-
-
-
-
Template Haskell
-Template Haskell allows you to do compile-time meta-programming in Haskell. There is a "home page" for
-Template Haskell at
-http://www.haskell.org/th/, while
-the background to
+Template Haskell allows you to do compile-time meta-programming in
+Haskell.
+The background to
the main technical innovations is discussed in "
Template Meta-programming for Haskell" (Proc Haskell Workshop 2002).
-The details of the Template Haskell design are still in flux. Make sure you
-consult the online library reference material
+
+
+There is a Wiki page about
+Template Haskell at
+http://www.haskell.org/th/, and that is the best place to look for
+further details.
+You may also
+consult the online
+Haskell library reference material
(search for the type ExpQ).
[Temporary: many changes to the original design are described in
"http://research.microsoft.com/~simonpj/tmp/notes2.ps".
-Not all of these changes are in GHC 6.2.]
+Not all of these changes are in GHC 6.6.]
The first example from that paper is set out below as a worked example to help get you started.
@@ -4770,6 +4784,150 @@ Because the preprocessor targets Haskell (rather than Core),
+
+
+
+Bang patterns
+Bang patterns
+
+GHC supports an extension of pattern matching called bang
+patterns. Bang patterns are under consideration for Haskell Prime.
+The Haskell
+prime feature description contains more discussion and examples
+than the material below.
+
+
+Bang patterns are enabled by the flag .
+
+
+
+Informal description of bang patterns
+
+
+The main idea is to add a single new production to the syntax of patterns:
+
+ pat ::= !pat
+
+Matching an expression e against a pattern !p is done by first
+evaluating e (to WHNF) and then matching the result against p.
+Example:
+
+f1 !x = True
+
+This definition makes f1 is strict in x,
+whereas without the bang it would be lazy.
+Bang patterns can be nested of course:
+
+f2 (!x, y) = [x,y]
+
+Here, f2 is strict in x but not in
+y.
+A bang only really has an effect if it precedes a variable or wild-card pattern:
+
+f3 !(x,y) = [x,y]
+f4 (x,y) = [x,y]
+
+Here, f3 and f4 are identical; putting a bang before a pattern that
+forces evaluation anyway does nothing.
+
+Bang patterns work in case expressions too, of course:
+
+g5 x = let y = f x in body
+g6 x = case f x of { y -> body }
+g7 x = case f x of { !y -> body }
+
+The functions g5 and g6 mean exactly the same thing.
+But g7 evalutes (f x), binds y to the
+result, and then evaluates body.
+
+Bang patterns work in let and where
+definitions too. For example:
+
+let ![x,y] = e in b
+
+is a strict pattern: operationally, it evaluates e, matches
+it against the pattern [x,y], and then evaluates b
+The "!" should not be regarded as part of the pattern; after all,
+in a function argument ![x,y] means the
+same as [x,y]. Rather, the "!"
+is part of the syntax of let bindings.
+
+
+
+
+
+Syntax and semantics
+
+
+
+We add a single new production to the syntax of patterns:
+
+ pat ::= !pat
+
+There is one problem with syntactic ambiguity. Consider:
+
+f !x = 3
+
+Is this a definition of the infix function "(!)",
+or of the "f" with a bang pattern? GHC resolves this
+ambiguity in favour of the latter. If you want to define
+(!) with bang-patterns enabled, you have to do so using
+prefix notation:
+
+(!) f x = 3
+
+The semantics of Haskell pattern matching is described in
+Section 3.17.2 of the Haskell Report. To this description add
+one extra item 10, saying:
+Matching
+the pattern !pat against a value v behaves as follows:
+if v is bottom, the match diverges
+ otherwise, pat is matched against
+ v
+
+
+Similarly, in Figure 4 of
+Section 3.17.3, add a new case (t):
+
+case v of { !pat -> e; _ -> e' }
+ = v `seq` case v of { pat -> e; _ -> e' }
+
+
+That leaves let expressions, whose translation is given in
+Section
+3.12
+of the Haskell Report.
+In the translation box, first apply
+the following transformation: for each pattern pi that is of
+form !qi = ei, transform it to (xi,!qi) = ((),ei), and and replace e0
+by (xi `seq` e0). Then, when none of the left-hand-side patterns
+have a bang at the top, apply the rules in the existing box.
+
+The effect of the let rule is to force complete matching of the pattern
+qi before evaluation of the body is begun. The bang is
+retained in the translated form in case qi is a variable,
+thus:
+
+ let !y = f x in b
+
+
+
+
+The let-binding can be recursive. However, it is much more common for
+the let-binding to be non-recursive, in which case the following law holds:
+(let !p = rhs in body)
+ is equivalent to
+(case rhs of !p -> body)
+
+
+A pattern with a bang at the outermost level is not allowed at the top level of
+a module.
+
+
+
+
@@ -5378,7 +5536,9 @@ The programmer can specify rewrite rules as part of the source program
(in a pragma). GHC applies these rewrite rules wherever it can, provided (a)
the flag () is on,
and (b) the flag
-() is not specified.
+() is not specified, and (c) the
+ ()
+flag is active.
@@ -6012,7 +6172,7 @@ r)
GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
r) ->
tpl2})
- (%note "foo"
+ (%note "bar"
eta);
@@ -6034,6 +6194,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.
@@ -6068,7 +6244,7 @@ shortcoming is something that could be fixed, with some kind of pragma.)
-The inline function
+The lazy function
The lazy function restrains strictness analysis a little:
@@ -6092,16 +6268,40 @@ 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
+
+The function unsafeCoerce# allows you to side-step the
+typechecker entirely. It has type
+
+ unsafeCoerce# :: a -> b
+
+That is, it allows you to coerce any type into any other type. If you use this
+function, you had better get it right, otherwise segmentation faults await.
+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.
+
+
+
Generic classes
- (Note: support for generic classes is currently broken in
- GHC 5.02).
-
The ideas behind this extension are described in detail in "Derivable type classes",
Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
@@ -6352,6 +6552,51 @@ Just to finish with, here's another example I rather like:
+
+Control over monomorphism
+
+GHC supports two flags that control the way in which generalisation is
+carried out at let and where bindings.
+
+
+
+Switching off the dreaded Monomorphism Restriction
+
+
+Haskell's monomorphism restriction (see
+Section
+4.5.5
+of the Haskell Report)
+can be completely switched off by
+.
+
+
+
+
+Monomorphic pattern bindings
+
+
+
+ As an experimental change, we are exploring the possibility of
+ making pattern bindings monomorphic; that is, not generalised at all.
+ A pattern binding is a binding whose LHS has no function arguments,
+ and is not a simple variable. For example:
+
+ f x = x -- Not a pattern binding
+ f = \x -> x -- Not a pattern binding
+ f :: Int -> Int = \x -> x -- Not a pattern binding
+
+ (g,h) = e -- A pattern binding
+ (f) = e -- A pattern binding
+ [x] = e -- A pattern binding
+
+Experimentally, GHC now makes pattern bindings monomorphic by
+default. Use to recover the
+standard behaviour.
+
+
+
+