X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=docs%2Fusers_guide%2Fglasgow_exts.xml;h=d9a6198788717b1d2299784935c4a47e0e0dfb50;hb=78b620de24ceb4621cead67bd642f72749b41052;hp=c370ce3388308a602a0f020a8745652fed0b5d3e;hpb=ea283aa74e6fd2bec2b88eae19908bba903adea1;p=ghc-hetmet.git
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index c370ce3..d9a6198 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -241,6 +241,14 @@ documentation describes all the libraries that come with GHC.
+
+
+ Enables overloaded string literals (see ).
+
+
+
+ Enables lexically-scoped type variables (see
-clunky env var1 var1 = case lookup env var1 of
+clunky env var1 var2 = case lookup env var1 of
Nothing -> fail
Just val1 -> case lookup env var2 of
Nothing -> fail
@@ -645,7 +653,7 @@ Here is how I would write clunky:
-clunky env var1 var1
+clunky env var1 var2
| Just val1 <- lookup env var1
, Just val2 <- lookup env var2
= val1 + val2
@@ -939,14 +947,10 @@ definitions; you must define such a function in prefix form.
-
-Type system extensions
-
-
-
-Data types and type synonyms
+
+Extensions to data types and type synonyms
-
+Data types with no constructorsWith the flag, GHC lets you declare
@@ -960,13 +964,13 @@ a data type with no constructors. For example:Syntactically, the declaration lacks the "= constrs" part. The
type can be parameterised over types of any kind, but if the kind is
not * then an explicit kind annotation must be used
-(see ).
+(see ).
Such data types have only one value, namely bottom.
Nevertheless, they can be useful when defining "phantom types".
-
+
-
+Infix type constructors, classes, and type variables
@@ -1033,9 +1037,9 @@ to be written infix, very much like expressions. More specifically:
-
+
-
+Liberalised type synonyms
@@ -1125,10 +1129,10 @@ this will be rejected:
because GHC does not allow unboxed tuples on the left of a function arrow.
-
+
-
+Existentially quantified data constructors
@@ -1222,7 +1226,7 @@ that collection of packages in a uniform manner. You can express
quite a bit of object-oriented-like programming this way.
-
+Why existential?
@@ -1245,9 +1249,9 @@ But Haskell programmers can safely think of the ordinary
adding a new existential quantification construct.
-
+
-
+Type classes
@@ -1307,9 +1311,9 @@ Notice the way that the syntax fits smoothly with that used for
universal quantification earlier.
-
+
-
+Record Constructors
@@ -1326,7 +1330,7 @@ data Counter a = forall self. NewCounter
Here tag is a public field, with a well-typed selector
function tag :: Counter a -> a. The self
type is hidden from the outside; any attempt to apply _this,
-_inc or _output as functions will raise a
+_inc or _display as functions will raise a
compile-time error. In other words, GHC defines a record selector function
only for fields whose type does not mention the existentially-quantified variables.
(This example used an underscore in the fields for which record selectors
@@ -1361,20 +1365,6 @@ main = do
display (inc (inc counterB)) -- prints "##"
-In GADT declarations (see ), the explicit
-forall may be omitted. For example, we can express
-the same Counter a using GADT:
-
-
-data Counter a where
- NewCounter { _this :: self
- , _inc :: self -> self
- , _display :: self -> IO ()
- , tag :: a
- }
- :: Counter a
-
-
At the moment, record update syntax is only supported for Haskell 98 data types,
so the following function does not work:
@@ -1386,10 +1376,10 @@ setTag obj t = obj{ tag = t }
-
+
-
+Restrictions
@@ -1515,7 +1505,7 @@ are convincing reasons to change it.
You can't use deriving to define instances of a
data type with existentially quantified data constructors.
-Reason: in most cases it would not make sense. For example:#
+Reason: in most cases it would not make sense. For example:;
data T = forall a. MkT [a] deriving( Eq )
@@ -1540,2218 +1530,2475 @@ declarations. Define your own instances!
-
-
+
+
+Declaring data types with explicit constructor signatures
-
-Class declarations
-
-
-This section, and the next one, documents GHC's type-class extensions.
-There's lots of background in the paper Type
-classes: exploring the design space (Simon Peyton Jones, Mark
-Jones, Erik Meijer).
-
-
-All the extensions are enabled by the flag.
-
-
-
-Multi-parameter type classes
-
-Multi-parameter type classes are permitted. For example:
-
-
+GHC allows you to declare an algebraic data type by
+giving the type signatures of constructors explicitly. For example:
- class Collection c a where
- union :: c a -> c a -> c a
- ...etc.
+ data Maybe a where
+ Nothing :: Maybe a
+ Just :: a -> Maybe a
-
-
-
-
-
-The superclasses of a class declaration
-
-
-There are no restrictions on the context in a class declaration
-(which introduces superclasses), except that the class hierarchy must
-be acyclic. So these class declarations are OK:
-
-
+The form is called a "GADT-style declaration"
+because Generalised Algebraic Data Types, described in ,
+can only be declared using this form.
+Notice that GADT-style syntax generalises existential types ().
+For example, these two declarations are equivalent:
- class Functor (m k) => FiniteMap m k where
- ...
-
- class (Monad m, Monad (t m)) => Transform t m where
- lift :: m a -> (t m) a
+ data Foo = forall a. MkFoo a (a -> Bool)
+ data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
-
-
-
-As in Haskell 98, The class hierarchy must be acyclic. However, the definition
-of "acyclic" involves only the superclass relationships. For example,
-this is OK:
-
-
+Any data type that can be declared in standard Haskell-98 syntax
+can also be declared using GADT-style syntax.
+The choice is largely stylistic, but GADT-style declarations differ in one important respect:
+they treat class constraints on the data constructors differently.
+Specifically, if the constructor is given a type-class context, that
+context is made available by pattern matching. For example:
- class C a where {
- op :: D b => a -> b -> b
- }
-
- class C a => D a where { ... }
-
+ data Set a where
+ MkSet :: Eq a => [a] -> Set a
+ makeSet :: Eq a => [a] -> Set a
+ makeSet xs = MkSet (nub xs)
-Here, C is a superclass of D, but it's OK for a
-class operation op of C to mention D. (It
-would not be OK for D to be a superclass of C.)
+ insert :: a -> Set a -> Set a
+ insert a (MkSet as) | a `elem` as = MkSet as
+ | otherwise = MkSet (a:as)
+
+A use of MkSet as a constructor (e.g. in the definition of makeSet)
+gives rise to a (Eq a)
+constraint, as you would expect. The new feature is that pattern-matching on MkSet
+(as in the definition of insert) makes available an (Eq a)
+context. In implementation terms, the MkSet constructor has a hidden field that stores
+the (Eq a) dictionary that is passed to MkSet; so
+when pattern-matching that dictionary becomes available for the right-hand side of the match.
+In the example, the equality dictionary is used to satisfy the equality constraint
+generated by the call to elem, so that the type of
+insert itself has no Eq constraint.
-
-
-
-
-
-
-Class method types
-
-
-Haskell 98 prohibits class method types to mention constraints on the
-class type variable, thus:
+This behaviour contrasts with Haskell 98's peculiar treament of
+contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report).
+In Haskell 98 the defintion
- class Seq s a where
- fromList :: [a] -> s a
- elem :: Eq a => a -> s a -> Bool
+ data Eq a => Set' a = MkSet' [a]
-The type of elem is illegal in Haskell 98, because it
-contains the constraint Eq a, constrains only the
-class type variable (in this case a).
-GHC lifts this restriction.
-
-
-
-
-
-
-
-Functional dependencies
-
-
- Functional dependencies are implemented as described by Mark Jones
-in “Type Classes with Functional Dependencies”, Mark P. Jones,
-In Proceedings of the 9th European Symposium on Programming,
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
-.
-
+gives MkSet' the same type as MkSet above. But instead of
+making available an (Eq a) constraint, pattern-matching
+on MkSet'requires an (Eq a) constraint!
+GHC faithfully implements this behaviour, odd though it is. But for GADT-style declarations,
+GHC's behaviour is much more useful, as well as much more intuitive.
-Functional dependencies are introduced by a vertical bar in the syntax of a
-class declaration; e.g.
+For example, a possible application of GHC's behaviour is to reify dictionaries:
- class (Monad m) => MonadState s m | m -> s where ...
+ data NumInst a where
+ MkNumInst :: Num a => NumInst a
- class Foo a b c | a b -> c where ...
+ intInst :: NumInst Int
+ intInst = MkNumInst
+
+ plus :: NumInst a -> a -> a -> a
+ plus MkNumInst p q = p + q
-There should be more documentation, but there isn't (yet). Yell if you need it.
+Here, a value of type NumInst a is equivalent
+to an explicit (Num a) dictionary.
-Rules for functional dependencies
-In a class declaration, all of the class type variables must be reachable (in the sense
-mentioned in )
-from the free variables of each method type.
-For example:
+The rest of this section gives further details about GADT-style data
+type declarations.
+
+
+
+The result type of each data constructor must begin with the type constructor being defined.
+If the result type of all constructors
+has the form T a1 ... an, where a1 ... an
+are distinct type variables, then the data type is ordinary;
+otherwise is a generalised data type ().
+
+
+The type signature of
+each constructor is independent, and is implicitly universally quantified as usual.
+Different constructors may have different universally-quantified type variables
+and different type-class constraints.
+For example, this is fine:
- class Coll s a where
- empty :: s
- insert :: s -> a -> s
+ data T a where
+ T1 :: Eq b => b -> T b
+ T2 :: (Show c, Ix c) => c -> [c] -> T c
+
-is not OK, because the type of empty doesn't mention
-a. Functional dependencies can make the type variable
-reachable:
+
+Unlike a Haskell-98-style
+data type declaration, the type variable(s) in the "data Set a where" header
+have no scope. Indeed, one can write a kind signature instead:
- class Coll s a | s -> a where
- empty :: s
- insert :: s -> a -> s
+ data Set :: * -> * where ...
+
+or even a mixture of the two:
+
+ data Foo a :: (* -> *) -> * where ...
+
+The type variables (if given) may be explicitly kinded, so we could also write the header for Foo
+like this:
+
+ data Foo a (b :: * -> *) where ...
+
-Alternatively Coll might be rewritten
+
+You can use strictness annotations, in the obvious places
+in the constructor type:
- class Coll s a where
- empty :: s a
- insert :: s a -> a -> s a
+ data Term a where
+ Lit :: !Int -> Term Int
+ If :: Term Bool -> !(Term a) -> !(Term a) -> Term a
+ Pair :: Term a -> Term b -> Term (a,b)
+
+
+You can use a deriving clause on a GADT-style data type
+declaration. For example, these two declarations are equivalent
+
+ data Maybe1 a where {
+ Nothing1 :: Maybe1 a ;
+ Just1 :: a -> Maybe1 a
+ } deriving( Eq, Ord )
-which makes the connection between the type of a collection of
-a's (namely (s a)) and the element type a.
-Occasionally this really doesn't work, in which case you can split the
-class like this:
+ data Maybe2 a = Nothing2 | Just2 a
+ deriving( Eq, Ord )
+
+
+
+You can use record syntax on a GADT-style data type declaration:
- class CollE s where
- empty :: s
-
- class CollE s => Coll s a where
- insert :: s -> a -> s
+ data Person where
+ Adult { name :: String, children :: [Person] } :: Person
+ Child { name :: String } :: Person
+As usual, for every constructor that has a field f, the type of
+field f must be the same (modulo alpha conversion).
-
-
+
+At the moment, record updates are not yet possible with GADT-style declarations,
+so support is limited to record construction, selection and pattern matching.
+For exmaple
+
+ aPerson = Adult { name = "Fred", children = [] }
-
-Background on functional dependencies
+ shortName :: Person -> Bool
+ hasChildren (Adult { children = kids }) = not (null kids)
+ hasChildren (Child {}) = False
+
+
-The following description of the motivation and use of functional dependencies is taken
-from the Hugs user manual, reproduced here (with minor changes) by kind
-permission of Mark Jones.
-
-
-Consider the following class, intended as part of a
-library for collection types:
+
+As in the case of existentials declared using the Haskell-98-like record syntax
+(),
+record-selector functions are generated only for those fields that have well-typed
+selectors.
+Here is the example of that section, in GADT-style syntax:
- class Collects e ce where
- empty :: ce
- insert :: e -> ce -> ce
- member :: e -> ce -> Bool
+data Counter a where
+ NewCounter { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+ :: Counter a
-The type variable e used here represents the element type, while ce is the type
-of the container itself. Within this framework, we might want to define
-instances of this class for lists or characteristic functions (both of which
-can be used to represent collections of any equality type), bit sets (which can
-be used to represent collections of characters), or hash tables (which can be
-used to represent any collection whose elements have a hash function). Omitting
-standard implementation details, this would lead to the following declarations:
+As before, only one selector function is generated here, that for tag.
+Nevertheless, you can still use all the field names in pattern matching and record construction.
+
+
+
+
+
+Generalised Algebraic Data Types (GADTs)
+
+Generalised Algebraic Data Types generalise ordinary algebraic data types
+by allowing constructors to have richer return types. Here is an example:
- instance Eq e => Collects e [e] where ...
- instance Eq e => Collects e (e -> Bool) where ...
- instance Collects Char BitSet where ...
- instance (Hashable e, Collects a ce)
- => Collects e (Array Int ce) where ...
+ data Term a where
+ Lit :: Int -> Term Int
+ Succ :: Term Int -> Term Int
+ IsZero :: Term Int -> Term Bool
+ If :: Term Bool -> Term a -> Term a -> Term a
+ Pair :: Term a -> Term b -> Term (a,b)
-All this looks quite promising; we have a class and a range of interesting
-implementations. Unfortunately, there are some serious problems with the class
-declaration. First, the empty function has an ambiguous type:
+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:
- empty :: Collects e ce => ce
+ 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)
-By "ambiguous" we mean that there is a type variable e that appears on the left
-of the => symbol, but not on the right. The problem with
-this is that, according to the theoretical foundations of Haskell overloading,
-we cannot guarantee a well-defined semantics for any term with an ambiguous
-type.
-
-
-We can sidestep this specific problem by removing the empty member from the
-class declaration. However, although the remaining members, insert and member,
-do not have ambiguous types, we still run into problems when we try to use
-them. For example, consider the following two functions:
+The key point about GADTs is that pattern matching causes type refinement.
+For example, in the right hand side of the equation
- f x y = insert x . insert y
- g = f True 'a'
+ eval :: Term a -> a
+ eval (Lit i) = ...
-for which GHC infers the following types:
+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:
- f :: (Collects a c, Collects b c) => a -> b -> c -> c
- g :: (Collects Bool c, Collects Char c) => c -> c
+ eval :: Term a -> a -> a
+ eval (Lit i) j = i+j
-Notice that the type for f allows the two parameters x and y to be assigned
-different types, even though it attempts to insert each of the two values, one
-after the other, into the same collection. If we're trying to model collections
-that contain only one type of value, then this is clearly an inaccurate
-type. Worse still, the definition for g is accepted, without causing a type
-error. As a result, the error in this code will not be flagged at the point
-where it appears. Instead, it will show up only when we try to use g, which
-might even be in a different module.
+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.
-
-An attempt to use constructor classes
-
-Faced with the problems described above, some Haskell programmers might be
-tempted to use something like the following version of the class declaration:
-
- class Collects e c where
- empty :: c e
- insert :: e -> c e -> c e
- member :: e -> c e -> Bool
-
-The key difference here is that we abstract over the type constructor c that is
-used to form the collection type c e, and not over that collection type itself,
-represented by ce in the original class declaration. This avoids the immediate
-problems that we mentioned above: empty has type Collects e c => c
-e, which is not ambiguous.
+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 function f from the previous section has a more accurate type:
-
- f :: (Collects e c) => e -> e -> c e -> c e
-
-The function g from the previous section is now rejected with a type error as
-we would hope because the type of f does not allow the two arguments to have
-different types.
-This, then, is an example of a multiple parameter class that does actually work
-quite well in practice, without ambiguity problems.
-There is, however, a catch. This version of the Collects class is nowhere near
-as general as the original class seemed to be: only one of the four instances
-for Collects
-given above can be used with this version of Collects because only one of
-them---the instance for lists---has a collection type that can be written in
-the form c e, for some type constructor c, and element type e.
-
-
-
-Adding functional dependencies
+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).
+
-
-To get a more useful version of the Collects class, Hugs provides a mechanism
-that allows programmers to specify dependencies between the parameters of a
-multiple parameter class (For readers with an interest in theoretical
-foundations and previous work: The use of dependency information can be seen
-both as a generalization of the proposal for `parametric type classes' that was
-put forward by Chen, Hudak, and Odersky, or as a special case of Mark Jones's
-later framework for "improvement" of qualified types. The
-underlying ideas are also discussed in a more theoretical and abstract setting
-in a manuscript [implparam], where they are identified as one point in a
-general design space for systems of implicit parameterization.).
+
+You cannot use a deriving clause for a GADT; only for
+an ordianary data type.
+
-To start with an abstract example, consider a declaration such as:
+
+As mentioned in , record syntax is supported.
+For example:
- class C a b where ...
+ 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
-which tells us simply that C can be thought of as a binary relation on types
-(or type constructors, depending on the kinds of a and b). Extra clauses can be
-included in the definition of classes to add information about dependencies
-between parameters, as in the following examples:
+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:
+
- class D a b | a -> b where ...
- class E a b | a -> b, b -> a where ...
+ num :: Term Int -> Term Int
+ arg :: Term Bool -> Term Int
-The notation a -> b used here between the | and where
-symbols --- not to be
-confused with a function type --- indicates that the a parameter uniquely
-determines the b parameter, and might be read as "a determines b." Thus D is
-not just a relation, but actually a (partial) function. Similarly, from the two
-dependencies that are included in the definition of E, we can see that E
-represents a (partial) one-one mapping between types.
+
+
+
+
+
+
+
+
+
+
+Deriving clause for classes Typeable and Data
+
-More generally, dependencies take the form x1 ... xn -> y1 ... ym,
-where x1, ..., xn, and y1, ..., yn are type variables with n>0 and
-m>=0, meaning that the y parameters are uniquely determined by the x
-parameters. Spaces can be used as separators if more than one variable appears
-on any single side of a dependency, as in t -> a b. Note that a class may be
-annotated with multiple dependencies using commas as separators, as in the
-definition of E above. Some dependencies that we can write in this notation are
-redundant, and will be rejected because they don't serve any useful
-purpose, and may instead indicate an error in the program. Examples of
-dependencies like this include a -> a ,
-a -> a a ,
-a -> , etc. There can also be
-some redundancy if multiple dependencies are given, as in
-a->b,
- b->c , a->c , and
-in which some subset implies the remaining dependencies. Examples like this are
-not treated as errors. Note that dependencies appear only in class
-declarations, and not in any other part of the language. In particular, the
-syntax for instance declarations, class constraints, and types is completely
-unchanged.
+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.
-By including dependencies in a class declaration, we provide a mechanism for
-the programmer to specify each multiple parameter class more precisely. The
-compiler, on the other hand, is responsible for ensuring that the set of
-instances that are in scope at any given point in the program is consistent
-with any declared dependencies. For example, the following pair of instance
-declarations cannot appear together in the same scope because they violate the
-dependency for D, even though either one on its own would be acceptable:
-
- instance D Bool Int where ...
- instance D Bool Char where ...
-
-Note also that the following declaration is not allowed, even by itself:
-
- instance D [a] b where ...
-
-The problem here is that this instance would allow one particular choice of [a]
-to be associated with more than one choice for b, which contradicts the
-dependency specified in the definition of D. More generally, this means that,
-in any instance of the form:
-
- instance D t s where ...
-
-for some particular types t and s, the only variables that can appear in s are
-the ones that appear in t, and hence, if the type t is known, then s will be
-uniquely determined.
+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
+
-The benefit of including dependency information is that it allows us to define
-more general multiple parameter classes, without ambiguity problems, and with
-the benefit of more accurate types. To illustrate this, we return to the
-collection class example, and annotate the original definition of Collects
-with a simple dependency:
-
- class Collects e ce | ce -> e where
- empty :: ce
- insert :: e -> ce -> ce
- member :: e -> ce -> Bool
+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)
+ ...
-The dependency ce -> e here specifies that the type e of elements is uniquely
-determined by the type of the collection ce. Note that both parameters of
-Collects are of kind *; there are no constructor classes here. Note too that
-all of the instances of Collects that we gave earlier can be used
-together with this new definition.
+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
-What about the ambiguity problems that we encountered with the original
-definition? The empty function still has type Collects e ce => ce, but it is no
-longer necessary to regard that as an ambiguous type: Although the variable e
-does not appear on the right of the => symbol, the dependency for class
-Collects tells us that it is uniquely determined by ce, which does appear on
-the right of the => symbol. Hence the context in which empty is used can still
-give enough information to determine types for both ce and e, without
-ambiguity. More generally, we need only regard a type as ambiguous if it
-contains a variable on the left of the => that is not uniquely determined
-(either directly or indirectly) by the variables on the right.
+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.
-Dependencies also help to produce more accurate types for user defined
-functions, and hence to provide earlier detection of errors, and less cluttered
-types for programmers to work with. Recall the previous definition for a
-function f:
-
- f x y = insert x y = insert x . insert y
+
+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
-for which we originally obtained a type:
-
- f :: (Collects a c, Collects b c) => a -> b -> c -> c
+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])
-Given the dependency information that we have for Collects, however, we can
-deduce that a and b must be equal because they both appear as the second
-parameter in a Collects constraint with the same first parameter c. Hence we
-can infer a shorter and more accurate type for f:
-
- f :: (Collects a c) => a -> a -> c -> c
+
+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)
-In a similar way, the earlier definition of g will now be flagged as a type error.
-Although we have given only a few examples here, it should be clear that the
-addition of dependency information can help to make multiple parameter classes
-more useful in practice, avoiding ambiguity problems, and allowing more general
-sets of instance declarations.
+
+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.
-
-
-
-
-Instance declarations
-
-Relaxed rules for instance declarations
+ A more precise specification
+
+Derived instance declarations are constructed as follows. Consider the
+declaration (after expansion of any type synonyms)
-An instance declaration has the form
-
- instance ( assertion1, ..., assertionn) => classtype1 ... typem where ...
-
-The part before the "=>" is the
-context, while the part after the
-"=>" is the head of the instance declaration.
-
+
+ newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm)
+
-
-In Haskell 98 the head of an instance declaration
-must be of the form C (T a1 ... an), where
-C is the class, T is a type constructor,
-and the a1 ... an are distinct type variables.
-Furthermore, the assertions in the context of the instance declaration
-must be of the form C a where a
-is a type variable that occurs in the head.
-
-
-The flag loosens these restrictions
-considerably. Firstly, multi-parameter type classes are permitted. Secondly,
-the context and head of the instance declaration can each consist of arbitrary
-(well-kinded) assertions (C t1 ... tn) subject only to the
-following rules:
-
+where
+
-For each assertion in the context:
-
-No type variable has more occurrences in the assertion than in the head
-The assertion has fewer constructors and variables (taken together
- and counting repetitions) than the head
-
+ 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 coverage condition. For each functional dependency,
-tvsleft->
-tvsright, of the class,
-every type variable in
-S(tvsright) must appear in
-S(tvsleft), where S is the
-substitution mapping each type variable in the class declaration to the
-corresponding type in the instance declaration.
+
+ The k is chosen so that ci (T v1...vk) is well-kinded.
-
-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 ...
+
+ 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)
-For example, these are OK:
-
- instance C Int [a] -- Multiple parameters
- instance Eq (S [a]) -- Structured type in head
+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)
+
- -- Repeated type variable in head
- instance C4 a a => C4 [a] [a]
- instance Stateful (ST s) (MutVar s)
+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.
+
+
- -- Head can consist of type variables only
- instance C a
- instance (Eq a, Show b) => C2 a b
+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
- -- Non-type variables in context
- instance Show (s a) => Show (Sized s a)
- instance C2 Int a => C3 Bool [a]
- instance C2 Int a => C3 [a] b
-
-But these are not:
-
- -- Context assertion no smaller than head
- instance C a => C a where ...
- -- (C b b) has more more occurrences of b than the head
- instance C b b => Foo [b] where ...
+
+ 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
-The same restrictions apply to instances generated by
-deriving clauses. Thus the following is accepted:
+GHC now allows stand-alone deriving declarations, enabled by -fglasgow-exts:
- data MinHeap h a = H a (h a)
- deriving (Show)
+ data Foo a = Bar a | Baz String
+
+ derive instance Eq (Foo a)
-because the derived instance
+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:
- instance (Show a, Show (h a)) => Show (MinHeap h a)
+ newtype Foo a = MkFoo (State Int a)
+
+ derive instance MonadState Int Foo
-conforms to the above rules.
+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
-A useful idiom permitted by the above rules is as follows.
-If one allows overlapping instance declarations then it's quite
-convenient to have a "default instance" declaration that applies if
-something more specific does not:
+Multi-parameter type classes are permitted. For example:
+
+
- instance C a where
- op = ... -- Default
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...etc.
-
-You can find lots of background material about the reason for these
-restrictions in the paper
-Understanding functional dependencies via Constraint Handling Rules.
+
-
-Undecidable instances
+
+The superclasses of a class declaration
-Sometimes even the rules of are too onerous.
-For example, sometimes you might want to use the following to get the
-effect of a "class synonym":
-
- class (C1 a, C2 a, C3 a) => C a where { }
+There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic. So these class declarations are OK:
- instance (C1 a, C2 a, C3 a) => C a where { }
-
-This allows you to write shorter signatures:
-
- f :: C a => ...
-
-instead of
-
- f :: (C1 a, C2 a, C3 a) => ...
-
-The restrictions on functional dependencies () are particularly troublesome.
-It is tempting to introduce type variables in the context that do not appear in
-the head, something that is excluded by the normal rules. For example:
-
- class HasConverter a b | a -> b where
- convert :: a -> b
-
- data Foo a = MkFoo a
- instance (HasConverter a b,Show b) => Show (Foo a) where
- show (MkFoo value) = show (convert value)
-
-This is dangerous territory, however. Here, for example, is a program that would make the
-typechecker loop:
-
- class D a
- class F a b | a->b
- instance F [a] [[a]]
- instance (D c, F a c) => D [a] -- 'c' is not mentioned in the head
-
-Similarly, it can be tempting to lift the coverage condition:
- class Mul a b c | a b -> c where
- (.*.) :: a -> b -> c
+ class Functor (m k) => FiniteMap m k where
+ ...
- instance Mul Int Int Int where (.*.) = (*)
- instance Mul Int Float Float where x .*. y = fromIntegral x * y
- instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
-The third instance declaration does not obey the coverage condition;
-and indeed the (somewhat strange) definition:
+
+
+
+
+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:
+
+
- f = \ b x y -> if b then x .*. [y] else y
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
-makes instance inference go into a loop, because it requires the constraint
-(Mul a [b] b).
-
-
-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
-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.
-
+
+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.)
+
-
-Overlapping instances
-
-In general, GHC requires that that it be unambiguous which instance
-declaration
-should be used to resolve a type-class constraint. This behaviour
-can be modified by two flags:
--fallow-overlapping-instances
-
-and
--fallow-incoherent-instances
-, 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 ().
+
+
+
+Class method types
+
-When GHC tries to resolve, say, the constraint C Int Bool,
-it tries to match every instance declaration against the
-constraint,
-by instantiating the head of the instance declaration. For example, consider
-these declarations:
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
- instance context1 => C Int a where ... -- (A)
- instance context2 => C a Bool where ... -- (B)
- instance context3 => C Int [a] where ... -- (C)
- instance context4 => C Int [Int] where ... -- (D)
+ class Seq s a where
+ fromList :: [a] -> s a
+ elem :: Eq a => a -> s a -> Bool
-The instances (A) and (B) match the constraint C Int Bool,
-but (C) and (D) do not. When matching, GHC takes
-no account of the context of the instance declaration
-(context1 etc).
-GHC's default behaviour is that exactly one instance must match the
-constraint it is trying to resolve.
-It is fine for there to be a potential of overlap (by
-including both declarations (A) and (B), say); an error is only reported if a
-particular constraint matches more than one.
+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.
-
-The flag instructs GHC to allow
-more than one instance to match, provided there is a most specific one. For
-example, the constraint C Int [Int] matches instances (A),
-(C) and (D), but the last is more specific, and hence is chosen. If there is no
-most-specific match, the program is rejected.
+
+
+
+
+
+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,
+.
-However, GHC is conservative about committing to an overlapping instance. For example:
+Functional dependencies are introduced by a vertical bar in the syntax of a
+class declaration; e.g.
- f :: [b] -> [b]
- f x = ...
+ class (Monad m) => MonadState s m | m -> s where ...
+
+ class Foo a b c | a b -> c where ...
-Suppose that from the RHS of f we get the constraint
-C Int [b]. But
-GHC does not commit to instance (C), because in a particular
-call of f, b might be instantiate
-to Int, in which case instance (D) would be more specific still.
-So GHC rejects the program. If you add the flag ,
-GHC will instead pick (C), without complaining about
-the problem of subsequent instantiations.
-
-
-The willingness to be overlapped or incoherent is a property of
-the instance declaration itself, controlled by the
-presence or otherwise of the
-and flags when that mdodule is
-being defined. Neither flag is required in a module that imports and uses the
-instance declaration. Specifically, during the lookup process:
-
-
-An instance declaration is ignored during the lookup process if (a) a more specific
-match is found, and (b) the instance declaration was compiled with
-. The flag setting for the
-more-specific instance does not matter.
-
-
-Suppose an instance declaration does not matche the constraint being looked up, but
-does unify with it, so that it might match when the constraint is further
-instantiated. Usually GHC will regard this as a reason for not committing to
-some other constraint. But if the instance declaration was compiled with
-, GHC will skip the "does-it-unify?"
-check for that declaration.
-
-
-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.
+There should be more documentation, but there isn't (yet). Yell if you need it.
+
+Rules for functional dependencies
-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.
-
-
+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:
-
-Type synonyms in the instance head
+
+ class Coll s a where
+ empty :: s
+ insert :: s -> a -> s
+
-
-Unlike Haskell 98, instance heads may use type
-synonyms. (The instance "head" is the bit after the "=>" in an instance decl.)
-As always, using a type synonym is just shorthand for
-writing the RHS of the type synonym definition. For example:
+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
- type Point = (Int,Int)
- instance C Point where ...
- instance C [Point] where ...
+ class Coll s a where
+ empty :: s a
+ insert :: s a -> a -> s a
-is legal. However, if you added
+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:
- instance C (Int,Int) where ...
+ class CollE s where
+ empty :: s
+
+ class CollE s => Coll s a where
+ insert :: s -> a -> s
+
+
-as well, then the compiler will complain about the overlapping
-(actually, identical) instance declarations. As always, type synonyms
-must be fully applied. You cannot, for example, write:
+
+Background on functional dependencies
+
+The following description of the motivation and use of functional dependencies is taken
+from the Hugs user manual, reproduced here (with minor changes) by kind
+permission of Mark Jones.
+
+
+Consider the following class, intended as part of a
+library for collection types:
+
+ class Collects e ce where
+ empty :: ce
+ insert :: e -> ce -> ce
+ member :: e -> ce -> Bool
+
+The type variable e used here represents the element type, while ce is the type
+of the container itself. Within this framework, we might want to define
+instances of this class for lists or characteristic functions (both of which
+can be used to represent collections of any equality type), bit sets (which can
+be used to represent collections of characters), or hash tables (which can be
+used to represent any collection whose elements have a hash function). Omitting
+standard implementation details, this would lead to the following declarations:
+
+ instance Eq e => Collects e [e] where ...
+ instance Eq e => Collects e (e -> Bool) where ...
+ instance Collects Char BitSet where ...
+ instance (Hashable e, Collects a ce)
+ => Collects e (Array Int ce) where ...
+
+All this looks quite promising; we have a class and a range of interesting
+implementations. Unfortunately, there are some serious problems with the class
+declaration. First, the empty function has an ambiguous type:
+
+ empty :: Collects e ce => ce
+
+By "ambiguous" we mean that there is a type variable e that appears on the left
+of the => symbol, but not on the right. The problem with
+this is that, according to the theoretical foundations of Haskell overloading,
+we cannot guarantee a well-defined semantics for any term with an ambiguous
+type.
+
+
+We can sidestep this specific problem by removing the empty member from the
+class declaration. However, although the remaining members, insert and member,
+do not have ambiguous types, we still run into problems when we try to use
+them. For example, consider the following two functions:
+
+ f x y = insert x . insert y
+ g = f True 'a'
+
+for which GHC infers the following types:
+
+ f :: (Collects a c, Collects b c) => a -> b -> c -> c
+ g :: (Collects Bool c, Collects Char c) => c -> c
+
+Notice that the type for f allows the two parameters x and y to be assigned
+different types, even though it attempts to insert each of the two values, one
+after the other, into the same collection. If we're trying to model collections
+that contain only one type of value, then this is clearly an inaccurate
+type. Worse still, the definition for g is accepted, without causing a type
+error. As a result, the error in this code will not be flagged at the point
+where it appears. Instead, it will show up only when we try to use g, which
+might even be in a different module.
+
+An attempt to use constructor classes
+
+Faced with the problems described above, some Haskell programmers might be
+tempted to use something like the following version of the class declaration:
- type P a = [[a]]
- instance Monad P where ...
+ class Collects e c where
+ empty :: c e
+ insert :: e -> c e -> c e
+ member :: e -> c e -> Bool
-
-
-This design decision is independent of all the others, and easily
-reversed, but it makes sense to me.
-
+The key difference here is that we abstract over the type constructor c that is
+used to form the collection type c e, and not over that collection type itself,
+represented by ce in the original class declaration. This avoids the immediate
+problems that we mentioned above: empty has type Collects e c => c
+e, which is not ambiguous.
-
-
-
-
-
-
-Type signatures
-
-The context of a type signature
-Unlike Haskell 98, constraints in types do not have to be of
-the form (class type-variable) or
-(class (type-variable type-variable ...)). Thus,
-these type signatures are perfectly OK
+The function f from the previous section has a more accurate type:
- g :: Eq [a] => ...
- g :: Ord (T a ()) => ...
+ f :: (Collects e c) => e -> e -> c e -> c e
+The function g from the previous section is now rejected with a type error as
+we would hope because the type of f does not allow the two arguments to have
+different types.
+This, then, is an example of a multiple parameter class that does actually work
+quite well in practice, without ambiguity problems.
+There is, however, a catch. This version of the Collects class is nowhere near
+as general as the original class seemed to be: only one of the four instances
+for Collects
+given above can be used with this version of Collects because only one of
+them---the instance for lists---has a collection type that can be written in
+the form c e, for some type constructor c, and element type e.
+
+
+Adding functional dependencies
+
-GHC imposes the following restrictions on the constraints in a type signature.
-Consider the type:
+To get a more useful version of the Collects class, Hugs provides a mechanism
+that allows programmers to specify dependencies between the parameters of a
+multiple parameter class (For readers with an interest in theoretical
+foundations and previous work: The use of dependency information can be seen
+both as a generalization of the proposal for `parametric type classes' that was
+put forward by Chen, Hudak, and Odersky, or as a special case of Mark Jones's
+later framework for "improvement" of qualified types. The
+underlying ideas are also discussed in a more theoretical and abstract setting
+in a manuscript [implparam], where they are identified as one point in a
+general design space for systems of implicit parameterization.).
+To start with an abstract example, consider a declaration such as:
- forall tv1..tvn (c1, ...,cn) => type
+ class C a b where ...
-
-(Here, we write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 98, all the free type variables of an
-explicit source-language type signature are universally quantified,
-except for the class type variables in a class declaration. However,
-in GHC, you can give the foralls if you want. See ).
+which tells us simply that C can be thought of as a binary relation on types
+(or type constructors, depending on the kinds of a and b). Extra clauses can be
+included in the definition of classes to add information about dependencies
+between parameters, as in the following examples:
+
+ class D a b | a -> b where ...
+ class E a b | a -> b, b -> a where ...
+
+The notation a -> b used here between the | and where
+symbols --- not to be
+confused with a function type --- indicates that the a parameter uniquely
+determines the b parameter, and might be read as "a determines b." Thus D is
+not just a relation, but actually a (partial) function. Similarly, from the two
+dependencies that are included in the definition of E, we can see that E
+represents a (partial) one-one mapping between types.
-
-
-
-
-
+More generally, dependencies take the form x1 ... xn -> y1 ... ym,
+where x1, ..., xn, and y1, ..., yn are type variables with n>0 and
+m>=0, meaning that the y parameters are uniquely determined by the x
+parameters. Spaces can be used as separators if more than one variable appears
+on any single side of a dependency, as in t -> a b. Note that a class may be
+annotated with multiple dependencies using commas as separators, as in the
+definition of E above. Some dependencies that we can write in this notation are
+redundant, and will be rejected because they don't serve any useful
+purpose, and may instead indicate an error in the program. Examples of
+dependencies like this include a -> a ,
+a -> a a ,
+a -> , etc. There can also be
+some redundancy if multiple dependencies are given, as in
+a->b,
+ b->c , a->c , and
+in which some subset implies the remaining dependencies. Examples like this are
+not treated as errors. Note that dependencies appear only in class
+declarations, and not in any other part of the language. In particular, the
+syntax for instance declarations, class constraints, and types is completely
+unchanged.
+
- Each universally quantified type variable
-tvi must be reachable from type.
-
-A type variable a is "reachable" if it it appears
-in the same constraint as either a type variable free in in
-type, or another reachable type variable.
-A value with a type that does not obey
-this reachability restriction cannot be used without introducing
-ambiguity; that is why the type is rejected.
-Here, for example, is an illegal type:
-
-
+By including dependencies in a class declaration, we provide a mechanism for
+the programmer to specify each multiple parameter class more precisely. The
+compiler, on the other hand, is responsible for ensuring that the set of
+instances that are in scope at any given point in the program is consistent
+with any declared dependencies. For example, the following pair of instance
+declarations cannot appear together in the same scope because they violate the
+dependency for D, even though either one on its own would be acceptable:
- forall a. Eq a => Int
+ instance D Bool Int where ...
+ instance D Bool Char where ...
-
-
-When a value with this type was used, the constraint Eq tv
-would be introduced where tv is a fresh type variable, and
-(in the dictionary-translation implementation) the value would be
-applied to a dictionary for Eq tv. The difficulty is that we
-can never know which instance of Eq to use because we never
-get any more information about tv.
+Note also that the following declaration is not allowed, even by itself:
+
+ instance D [a] b where ...
+
+The problem here is that this instance would allow one particular choice of [a]
+to be associated with more than one choice for b, which contradicts the
+dependency specified in the definition of D. More generally, this means that,
+in any instance of the form:
+
+ instance D t s where ...
+
+for some particular types t and s, the only variables that can appear in s are
+the ones that appear in t, and hence, if the type t is known, then s will be
+uniquely determined.
-Note
-that the reachability condition is weaker than saying that a is
-functionally dependent on a type variable free in
-type (see ). The reason for this is there
-might be a "hidden" dependency, in a superclass perhaps. So
-"reachable" is a conservative approximation to "functionally dependent".
-For example, consider:
+The benefit of including dependency information is that it allows us to define
+more general multiple parameter classes, without ambiguity problems, and with
+the benefit of more accurate types. To illustrate this, we return to the
+collection class example, and annotate the original definition of Collects
+with a simple dependency:
- class C a b | a -> b where ...
- class C a b => D a b where ...
- f :: forall a b. D a b => a -> a
+ class Collects e ce | ce -> e where
+ empty :: ce
+ insert :: e -> ce -> ce
+ member :: e -> ce -> Bool
-This is fine, because in fact a does functionally determine b
-but that is not immediately apparent from f's type.
+The dependency ce -> e here specifies that the type e of elements is uniquely
+determined by the type of the collection ce. Note that both parameters of
+Collects are of kind *; there are no constructor classes here. Note too that
+all of the instances of Collects that we gave earlier can be used
+together with this new definition.
-
-
-
- Every constraint ci must mention at least one of the
-universally quantified type variables tvi.
-
-For example, this type is OK because C a b mentions the
-universally quantified type variable b:
-
-
+What about the ambiguity problems that we encountered with the original
+definition? The empty function still has type Collects e ce => ce, but it is no
+longer necessary to regard that as an ambiguous type: Although the variable e
+does not appear on the right of the => symbol, the dependency for class
+Collects tells us that it is uniquely determined by ce, which does appear on
+the right of the => symbol. Hence the context in which empty is used can still
+give enough information to determine types for both ce and e, without
+ambiguity. More generally, we need only regard a type as ambiguous if it
+contains a variable on the left of the => that is not uniquely determined
+(either directly or indirectly) by the variables on the right.
+
+
+Dependencies also help to produce more accurate types for user defined
+functions, and hence to provide earlier detection of errors, and less cluttered
+types for programmers to work with. Recall the previous definition for a
+function f:
- forall a. C a b => burble
+ f x y = insert x y = insert x . insert y
-
-
-The next type is illegal because the constraint Eq b does not
-mention a:
-
-
+for which we originally obtained a type:
- forall a. Eq b => burble
+ f :: (Collects a c, Collects b c) => a -> b -> c -> c
+
+Given the dependency information that we have for Collects, however, we can
+deduce that a and b must be equal because they both appear as the second
+parameter in a Collects constraint with the same first parameter c. Hence we
+can infer a shorter and more accurate type for f:
+
+ f :: (Collects a c) => a -> a -> c -> c
+In a similar way, the earlier definition of g will now be flagged as a type error.
+
+
+Although we have given only a few examples here, it should be clear that the
+addition of dependency information can help to make multiple parameter classes
+more useful in practice, avoiding ambiguity problems, and allowing more general
+sets of instance declarations.
+
+
+
+
+
+Instance declarations
-The reason for this restriction is milder than the other one. The
-excluded types are never useful or necessary (because the offending
-context doesn't need to be witnessed at this point; it can be floated
-out). Furthermore, floating them out increases sharing. Lastly,
-excluding them is a conservative choice; it leaves a patch of
-territory free in case we need it later.
+
+Relaxed rules for instance declarations
+An instance declaration has the form
+
+ instance ( assertion1, ..., assertionn) => classtype1 ... typem where ...
+
+The part before the "=>" is the
+context, while the part after the
+"=>" is the head of the instance declaration.
-
+
+In Haskell 98 the head of an instance declaration
+must be of the form C (T a1 ... an), where
+C is the class, T is a type constructor,
+and the a1 ... an are distinct type variables.
+Furthermore, the assertions in the context of the instance declaration
+must be of the form C a where a
+is a type variable that occurs in the head.
+
+
+The flag loosens these restrictions
+considerably. Firstly, multi-parameter type classes are permitted. Secondly,
+the context and head of the instance declaration can each consist of arbitrary
+(well-kinded) assertions (C t1 ... tn) subject only to the
+following rules:
+
+
+The Paterson Conditions: for each assertion in the context
+
+No type variable has more occurrences in the assertion than in the head
+The assertion has fewer constructors and variables (taken together
+ and counting repetitions) than the head
+
+The Coverage Condition. For each functional dependency,
+tvsleft->
+tvsright, of the class,
+every type variable in
+S(tvsright) must appear in
+S(tvsleft), where S is the
+substitution mapping each type variable in the class declaration to the
+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. 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-all hoisting
-It is often convenient to use generalised type synonyms (see ) at the right hand
-end of an arrow, thus:
+For example, these are OK:
- type Discard a = forall b. a -> b -> a
+ instance C Int [a] -- Multiple parameters
+ instance Eq (S [a]) -- Structured type in head
- g :: Int -> Discard Int
- g x y z = x+y
-
-Simply expanding the type synonym would give
-
- g :: Int -> (forall b. Int -> b -> Int)
+ -- Repeated type variable in head
+ instance C4 a a => C4 [a] [a]
+ instance Stateful (ST s) (MutVar s)
+
+ -- Head can consist of type variables only
+ instance C a
+ instance (Eq a, Show b) => C2 a b
+
+ -- Non-type variables in context
+ instance Show (s a) => Show (Sized s a)
+ instance C2 Int a => C3 Bool [a]
+ instance C2 Int a => C3 [a] b
-but GHC "hoists" the forall to give the isomorphic type
+But these are not:
- g :: forall b. Int -> Int -> b -> Int
+ -- Context assertion no smaller than head
+ instance C a => C a where ...
+ -- (C b b) has more more occurrences of b than the head
+ instance C b b => Foo [b] where ...
-In general, the rule is this: to determine the type specified by any explicit
-user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
-performs the transformation:
+
+
+
+The same restrictions apply to instances generated by
+deriving clauses. Thus the following is accepted:
- type1 -> forall a1..an. context2 => type2
-==>
- forall a1..an. context2 => type1 -> type2
+ data MinHeap h a = H a (h a)
+ deriving (Show)
-(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:
+because the derived instance
- g :: Int -> Int -> forall b. b -> Int
+ instance (Show a, Show (h a)) => Show (MinHeap h a)
+conforms to the above rules.
+
-When doing this hoisting operation, GHC eliminates duplicate constraints. For
-example:
-
- type Foo a = (?x::Int) => Bool -> a
- g :: Foo (Foo Int)
-
-means
+A useful idiom permitted by the above rules is as follows.
+If one allows overlapping instance declarations then it's quite
+convenient to have a "default instance" declaration that applies if
+something more specific does not:
- g :: (?x::Int) => Bool -> Bool -> Int
+ instance C a where
+ op = ... -- Default
+
+Undecidable instances
-
-
-
-Implicit parameters
-
- Implicit parameters are implemented as described in
-"Implicit parameters: dynamic scoping with static types",
-J Lewis, MB Shields, E Meijer, J Launchbury,
-27th ACM Symposium on Principles of Programming Languages (POPL'00),
-Boston, Jan 2000.
-
-
-(Most of the following, stil rather incomplete, documentation is
-due to Jeff Lewis.)
-
-Implicit parameter support is enabled with the option
-.
-
-
-A variable is called dynamically bound when it is bound by the calling
-context of a function and statically bound when bound by the callee's
-context. In Haskell, all variables are statically bound. Dynamic
-binding of variables is a notion that goes back to Lisp, but was later
-discarded in more modern incarnations, such as Scheme. Dynamic binding
-can be very confusing in an untyped language, and unfortunately, typed
-languages, in particular Hindley-Milner typed languages like Haskell,
-only support static scoping of variables.
-
-However, by a simple extension to the type class system of Haskell, we
-can support dynamic binding. Basically, we express the use of a
-dynamically bound variable as a constraint on the type. These
-constraints lead to types of the form (?x::t') => t, which says "this
-function uses a dynamically-bound variable ?x
-of type t'". For
-example, the following expresses the type of a sort function,
-implicitly parameterized by a comparison function named cmp.
+Sometimes even the rules of are too onerous.
+For example, sometimes you might want to use the following to get the
+effect of a "class synonym":
- sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+ class (C1 a, C2 a, C3 a) => C a where { }
+
+ instance (C1 a, C2 a, C3 a) => C a where { }
-The dynamic binding constraints are just a new form of predicate in the type class system.
-
-
-An implicit parameter occurs in an expression using the special form ?x,
-where x is
-any valid identifier (e.g. ord ?x is a valid expression).
-Use of this construct also introduces a new
-dynamic-binding constraint in the type of the expression.
-For example, the following definition
-shows how we can define an implicitly parameterized sort function in
-terms of an explicitly parameterized sortBy function:
+This allows you to write shorter signatures:
- sortBy :: (a -> a -> Bool) -> [a] -> [a]
+ f :: C a => ...
+
+instead of
+
+ f :: (C1 a, C2 a, C3 a) => ...
+
+The restrictions on functional dependencies () are particularly troublesome.
+It is tempting to introduce type variables in the context that do not appear in
+the head, something that is excluded by the normal rules. For example:
+
+ class HasConverter a b | a -> b where
+ convert :: a -> b
+
+ data Foo a = MkFoo a
- sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
- sort = sortBy ?cmp
+ instance (HasConverter a b,Show b) => Show (Foo a) where
+ show (MkFoo value) = show (convert value)
-
+This is dangerous territory, however. Here, for example, is a program that would make the
+typechecker loop:
+
+ class D a
+ class F a b | a->b
+ instance F [a] [[a]]
+ instance (D c, F a c) => D [a] -- 'c' is not mentioned in the head
+
+Similarly, it can be tempting to lift the coverage condition:
+
+ class Mul a b c | a b -> c where
+ (.*.) :: a -> b -> c
-
-Implicit-parameter type constraints
-
-Dynamic binding constraints behave just like other type class
-constraints in that they are automatically propagated. Thus, when a
-function is used, its implicit parameters are inherited by the
-function that called it. For example, our sort function might be used
-to pick out the least value in a list:
+ instance Mul Int Int Int where (.*.) = (*)
+ instance Mul Int Float Float where x .*. y = fromIntegral x * y
+ instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
+
+The third instance declaration does not obey the coverage condition;
+and indeed the (somewhat strange) definition:
- least :: (?cmp :: a -> a -> Bool) => [a] -> a
- least xs = head (sort xs)
+ f = \ b x y -> if b then x .*. [y] else y
-Without lifting a finger, the ?cmp parameter is
-propagated to become a parameter of least as well. With explicit
-parameters, the default is that parameters must always be explicit
-propagated. With implicit parameters, the default is to always
-propagate them.
+makes instance inference go into a loop, because it requires the constraint
+(Mul a [b] b).
-An implicit-parameter type constraint differs from other type class constraints in the
-following way: All uses of a particular implicit parameter must have
-the same type. This means that the type of (?x, ?x)
-is (?x::a) => (a,a), and not
-(?x::a, ?x::b) => (a, b), as would be the case for type
-class constraints.
+Nevertheless, GHC allows you to experiment with more liberal rules. If you use
+the experimental flag
+-fallow-undecidable-instances
+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.
- You can't have an implicit parameter in the context of a class or instance
-declaration. For example, both these declarations are illegal:
-
- class (?x::Int) => C a where ...
- instance (?x::a) => Foo [a] where ...
-
-Reason: exactly which implicit parameter you pick up depends on exactly where
-you invoke a function. But the ``invocation'' of instance declarations is done
-behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
-Easiest thing is to outlaw the offending types.
+
+
+
+
+Overlapping instances
-Implicit-parameter constraints do not cause ambiguity. For example, consider:
+In general, GHC requires that that it be unambiguous which instance
+declaration
+should be used to resolve a type-class constraint. This behaviour
+can be modified by two flags:
+-fallow-overlapping-instances
+
+and
+-fallow-incoherent-instances
+, 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
+constraint,
+by instantiating the head of the instance declaration. For example, consider
+these declarations:
- f :: (?x :: [a]) => Int -> Int
- f n = n + length ?x
-
- g :: (Read a, Show a) => String -> String
- g s = show (read s)
-
-Here, g has an ambiguous type, and is rejected, but f
-is fine. The binding for ?x at f's call site is
-quite unambiguous, and fixes the type a.
+ instance context1 => C Int a where ... -- (A)
+ instance context2 => C a Bool where ... -- (B)
+ instance context3 => C Int [a] where ... -- (C)
+ instance context4 => C Int [Int] where ... -- (D)
+
+The instances (A) and (B) match the constraint C Int Bool,
+but (C) and (D) do not. When matching, GHC takes
+no account of the context of the instance declaration
+(context1 etc).
+GHC's default behaviour is that exactly one instance must match the
+constraint it is trying to resolve.
+It is fine for there to be a potential of overlap (by
+including both declarations (A) and (B), say); an error is only reported if a
+particular constraint matches more than one.
-
-
-
-Implicit-parameter bindings
-An implicit parameter is bound using the standard
-let or where binding forms.
-For example, we define the min function by binding
-cmp.
+The flag instructs GHC to allow
+more than one instance to match, provided there is a most specific one. For
+example, the constraint C Int [Int] matches instances (A),
+(C) and (D), but the last is more specific, and hence is chosen. If there is no
+most-specific match, the program is rejected.
+
+
+However, GHC is conservative about committing to an overlapping instance. For example:
- min :: [a] -> a
- min = let ?cmp = (<=) in least
+ f :: [b] -> [b]
+ f x = ...
+Suppose that from the RHS of f we get the constraint
+C Int [b]. But
+GHC does not commit to instance (C), because in a particular
+call of f, b might be instantiate
+to Int, in which case instance (D) would be more specific still.
+So GHC rejects the program. If you add the flag ,
+GHC will instead pick (C), without complaining about
+the problem of subsequent instantiations.
-A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
-bindings can occur, except at top level. That is, they can occur in a let
-(including in a list comprehension, or do-notation, or pattern guards),
-or a where clause.
-Note the following points:
+The willingness to be overlapped or incoherent is a property of
+the instance declaration itself, controlled by the
+presence or otherwise of the
+and flags when that mdodule is
+being defined. Neither flag is required in a module that imports and uses the
+instance declaration. Specifically, during the lookup process:
-An implicit-parameter binding group must be a
-collection of simple bindings to implicit-style variables (no
-function-style bindings, and no type signatures); these bindings are
-neither polymorphic or recursive.
-
-
-You may not mix implicit-parameter bindings with ordinary bindings in a
-single let
-expression; use two nested lets instead.
-(In the case of where you are stuck, since you can't nest where clauses.)
+An instance declaration is ignored during the lookup process if (a) a more specific
+match is found, and (b) the instance declaration was compiled with
+. The flag setting for the
+more-specific instance does not matter.
-
-You may put multiple implicit-parameter bindings in a
-single binding group; but they are not treated
-as a mutually recursive group (as ordinary let bindings are).
-Instead they are treated as a non-recursive group, simultaneously binding all the implicit
-parameter. The bindings are not nested, and may be re-ordered without changing
-the meaning of the program.
-For example, consider:
-
- f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
-
-The use of ?x in the binding for ?y does not "see"
-the binding for ?x, so the type of f is
-
- f :: (?x::Int) => Int -> Int
-
+Suppose an instance declaration does not matche the constraint being looked up, but
+does unify with it, so that it might match when the constraint is further
+instantiated. Usually GHC will regard this as a reason for not committing to
+some other constraint. But if the instance declaration was compiled with
+, GHC will skip the "does-it-unify?"
+check for that declaration.
+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.
-
-Implicit parameters and polymorphic recursion
+
+Type synonyms in the instance head
-Consider these two definitions:
-
- len1 :: [a] -> Int
- len1 xs = let ?acc = 0 in len_acc1 xs
-
- len_acc1 [] = ?acc
- len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs
-
- ------------
-
- len2 :: [a] -> Int
- len2 xs = let ?acc = 0 in len_acc2 xs
-
- len_acc2 :: (?acc :: Int) => [a] -> Int
- len_acc2 [] = ?acc
- len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs
-
-The only difference between the two groups is that in the second group
-len_acc is given a type signature.
-In the former case, len_acc1 is monomorphic in its own
-right-hand side, so the implicit parameter ?acc is not
-passed to the recursive call. In the latter case, because len_acc2
-has a type signature, the recursive call is made to the
-polymoprhic version, which takes ?acc
-as an implicit parameter. So we get the following results in GHCi:
-
- Prog> len1 "hello"
- 0
- Prog> len2 "hello"
- 5
-
-Adding a type signature dramatically changes the result! This is a rather
-counter-intuitive phenomenon, worth watching out for.
-
-
+Unlike Haskell 98, instance heads may use type
+synonyms. (The instance "head" is the bit after the "=>" in an instance decl.)
+As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition. For example:
-Implicit parameters and monomorphism
-GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the
-Haskell Report) to implicit parameters. For example, consider:
- f :: Int -> Int
- f v = let ?x = 0 in
- let y = ?x + v in
- let ?x = 5 in
- y
+ type Point = (Int,Int)
+ instance C Point where ...
+ instance C [Point] where ...
-Since the binding for y falls under the Monomorphism
-Restriction it is not generalised, so the type of y is
-simply Int, not (?x::Int) => Int.
-Hence, (f 9) returns result 9.
-If you add a type signature for y, then y
-will get type (?x::Int) => Int, so the occurrence of
-y in the body of the let will see the
-inner binding of ?x, so (f 9) will return
-14.
-
-
-
-
+The next type is illegal because the constraint Eq b does not
+mention a:
-
-Explicitly-kinded quantification
-
-Haskell infers the kind of each type variable. Sometimes it is nice to be able
-to give the kind explicitly as (machine-checked) documentation,
-just as it is nice to give a type signature for a function. On some occasions,
-it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
-John Hughes had to define the data type:
-
- data Set cxt a = Set [a]
- | Unused (cxt a -> ())
-
-The only use for the Unused constructor was to force the correct
-kind for the type variable cxt.
-
-
-GHC now instead allows you to specify the kind of a type variable directly, wherever
-a type variable is explicitly bound. Namely:
-
-data declarations:
-
- data Set (cxt :: * -> *) a = Set [a]
-
-type declarations:
-
- type T (f :: * -> *) = f Int
-
-class declarations:
-
- class (Eq a) => C (f :: * -> *) a where ...
-
-forall's in type signatures:
-
- f :: forall (cxt :: * -> *). Set cxt Int
-
-
-
+
+ forall a. Eq b => burble
+
+
+
+The reason for this restriction is milder than the other one. The
+excluded types are never useful or necessary (because the offending
+context doesn't need to be witnessed at this point; it can be floated
+out). Furthermore, floating them out increases sharing. Lastly,
+excluding them is a conservative choice; it leaves a patch of
+territory free in case we need it later.
-
-The parentheses are required. Some of the spaces are required too, to
-separate the lexemes. If you write (f::*->*) you
-will get a parse error, because "::*->*" is a
-single lexeme in Haskell.
+
+
+
-
-As part of the same extension, you can put kind annotations in types
-as well. Thus:
-
- f :: (Int :: *) -> Int
- g :: forall a. a -> (a :: *)
-
-The syntax is
-
- atype ::= '(' ctype '::' kind ')
-
-The parentheses are required.
+
+
+
+
+
+Implicit parameters
-
-Arbitrary-rank polymorphism
-
+ Implicit parameters are implemented as described in
+"Implicit parameters: dynamic scoping with static types",
+J Lewis, MB Shields, E Meijer, J Launchbury,
+27th ACM Symposium on Principles of Programming Languages (POPL'00),
+Boston, Jan 2000.
+
+
+(Most of the following, stil rather incomplete, documentation is
+due to Jeff Lewis.)
+
+Implicit parameter support is enabled with the option
+.
-Haskell type signatures are implicitly quantified. The new keyword forall
-allows us to say exactly what this means. For example:
+A variable is called dynamically bound when it is bound by the calling
+context of a function and statically bound when bound by the callee's
+context. In Haskell, all variables are statically bound. Dynamic
+binding of variables is a notion that goes back to Lisp, but was later
+discarded in more modern incarnations, such as Scheme. Dynamic binding
+can be very confusing in an untyped language, and unfortunately, typed
+languages, in particular Hindley-Milner typed languages like Haskell,
+only support static scoping of variables.
+However, by a simple extension to the type class system of Haskell, we
+can support dynamic binding. Basically, we express the use of a
+dynamically bound variable as a constraint on the type. These
+constraints lead to types of the form (?x::t') => t, which says "this
+function uses a dynamically-bound variable ?x
+of type t'". For
+example, the following expresses the type of a sort function,
+implicitly parameterized by a comparison function named cmp.
- g :: b -> b
-
-means this:
-
- g :: forall b. (b -> b)
+ sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
-The two are treated identically.
+The dynamic binding constraints are just a new form of predicate in the type class system.
-
-However, GHC's type system supports arbitrary-rank
-explicit universal quantification in
-types.
-For example, all the following types are legal:
+An implicit parameter occurs in an expression using the special form ?x,
+where x is
+any valid identifier (e.g. ord ?x is a valid expression).
+Use of this construct also introduces a new
+dynamic-binding constraint in the type of the expression.
+For example, the following definition
+shows how we can define an implicitly parameterized sort function in
+terms of an explicitly parameterized sortBy function:
- f1 :: forall a b. a -> b -> a
- g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
-
- f2 :: (forall a. a->a) -> Int -> Int
- g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+ sortBy :: (a -> a -> Bool) -> [a] -> [a]
- f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+ sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+ sort = sortBy ?cmp
-Here, f1 and g1 are rank-1 types, and
-can be written in standard Haskell (e.g. f1 :: a->b->a).
-The forall makes explicit the universal quantification that
-is implicitly added by Haskell.
-
-
-The functions f2 and g2 have rank-2 types;
-the forall is on the left of a function arrow. As g2
-shows, the polymorphic type on the left of the function arrow can be overloaded.
-
-
-The function f3 has a rank-3 type;
-it has rank-2 types on the left of a function arrow.
+
+
+Implicit-parameter type constraints
-GHC allows types of arbitrary rank; you can nest foralls
-arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
-that restriction has now been lifted.)
-In particular, a forall-type (also called a "type scheme"),
-including an operational type class context, is legal:
-
- On the left of a function arrow
- On the right of a function arrow (see )
- As the argument of a constructor, or type of a field, in a data type declaration. For
-example, any of the f1,f2,f3,g1,g2 above would be valid
-field type signatures.
- As the type of an implicit parameter
- In a pattern type signature (see )
-
-There is one place you cannot put a forall:
-you cannot instantiate a type variable with a forall-type. So you cannot
-make a forall-type the argument of a type constructor. So these types are illegal:
+Dynamic binding constraints behave just like other type class
+constraints in that they are automatically propagated. Thus, when a
+function is used, its implicit parameters are inherited by the
+function that called it. For example, our sort function might be used
+to pick out the least value in a list:
- x1 :: [forall a. a->a]
- x2 :: (forall a. a->a, Int)
- x3 :: Maybe (forall a. a->a)
+ least :: (?cmp :: a -> a -> Bool) => [a] -> a
+ least xs = head (sort xs)
-Of course forall becomes a keyword; you can't use forall as
-a type variable any more!
+Without lifting a finger, the ?cmp parameter is
+propagated to become a parameter of least as well. With explicit
+parameters, the default is that parameters must always be explicit
+propagated. With implicit parameters, the default is to always
+propagate them.
-
-
-
-Examples
-
-
-In a data or newtype declaration one can quantify
-the types of the constructor arguments. Here are several examples:
+An implicit-parameter type constraint differs from other type class constraints in the
+following way: All uses of a particular implicit parameter must have
+the same type. This means that the type of (?x, ?x)
+is (?x::a) => (a,a), and not
+(?x::a, ?x::b) => (a, b), as would be the case for type
+class constraints.
+ You can't have an implicit parameter in the context of a class or instance
+declaration. For example, both these declarations are illegal:
+
+ class (?x::Int) => C a where ...
+ instance (?x::a) => Foo [a] where ...
+
+Reason: exactly which implicit parameter you pick up depends on exactly where
+you invoke a function. But the ``invocation'' of instance declarations is done
+behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
+Easiest thing is to outlaw the offending types.
-
+Implicit-parameter constraints do not cause ambiguity. For example, consider:
-data T a = T1 (forall b. b -> b -> b) a
-
-data MonadT m = MkMonad { return :: forall a. a -> m a,
- bind :: forall a b. m a -> (a -> m b) -> m b
- }
+ f :: (?x :: [a]) => Int -> Int
+ f n = n + length ?x
-newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
+ g :: (Read a, Show a) => String -> String
+ g s = show (read s)
-
+Here, g has an ambiguous type, and is rejected, but f
+is fine. The binding for ?x at f's call site is
+quite unambiguous, and fixes the type a.
+
+
+
+Implicit-parameter bindings
-The constructors have rank-2 types:
+An implicit parameter is bound using the standard
+let or where binding forms.
+For example, we define the min function by binding
+cmp.
+
+ min :: [a] -> a
+ min = let ?cmp = (<=) in least
+
-
+A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
+bindings can occur, except at top level. That is, they can occur in a let
+(including in a list comprehension, or do-notation, or pattern guards),
+or a where clause.
+Note the following points:
+
+
+An implicit-parameter binding group must be a
+collection of simple bindings to implicit-style variables (no
+function-style bindings, and no type signatures); these bindings are
+neither polymorphic or recursive.
+
+
+You may not mix implicit-parameter bindings with ordinary bindings in a
+single let
+expression; use two nested lets instead.
+(In the case of where you are stuck, since you can't nest where clauses.)
+
+
+You may put multiple implicit-parameter bindings in a
+single binding group; but they are not treated
+as a mutually recursive group (as ordinary let bindings are).
+Instead they are treated as a non-recursive group, simultaneously binding all the implicit
+parameter. The bindings are not nested, and may be re-ordered without changing
+the meaning of the program.
+For example, consider:
-T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
-MkMonad :: forall m. (forall a. a -> m a)
- -> (forall a b. m a -> (a -> m b) -> m b)
- -> MonadT m
-MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
+ f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
-
+The use of ?x in the binding for ?y does not "see"
+the binding for ?x, so the type of f is
+
+ f :: (?x::Int) => Int -> Int
+
+
+
-
-Notice that you don't need to use a forall if there's an
-explicit context. For example in the first argument of the
-constructor MkSwizzle, an implicit "forall a." is
-prefixed to the argument type. The implicit forall
-quantifies all type variables that are not already in scope, and are
-mentioned in the type quantified over.
-
+
-
-As for type signatures, implicit quantification happens for non-overloaded
-types too. So if you write this:
+Implicit parameters and polymorphic recursion
+
+Consider these two definitions:
- data T a = MkT (Either a b) (b -> b)
-
+ len1 :: [a] -> Int
+ len1 xs = let ?acc = 0 in len_acc1 xs
-it's just as if you had written this:
+ len_acc1 [] = ?acc
+ len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs
-
- data T a = MkT (forall b. Either a b) (forall b. b -> b)
-
+ ------------
-That is, since the type variable b isn't in scope, it's
-implicitly universally quantified. (Arguably, it would be better
-to require explicit quantification on constructor arguments
-where that is what is wanted. Feedback welcomed.)
-
+ len2 :: [a] -> Int
+ len2 xs = let ?acc = 0 in len_acc2 xs
-
-You construct values of types T1, MonadT, Swizzle by applying
-the constructor to suitable values, just as usual. For example,
+ len_acc2 :: (?acc :: Int) => [a] -> Int
+ len_acc2 [] = ?acc
+ len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs
+
+The only difference between the two groups is that in the second group
+len_acc is given a type signature.
+In the former case, len_acc1 is monomorphic in its own
+right-hand side, so the implicit parameter ?acc is not
+passed to the recursive call. In the latter case, because len_acc2
+has a type signature, the recursive call is made to the
+polymoprhic version, which takes ?acc
+as an implicit parameter. So we get the following results in GHCi:
+
+ Prog> len1 "hello"
+ 0
+ Prog> len2 "hello"
+ 5
+
+Adding a type signature dramatically changes the result! This is a rather
+counter-intuitive phenomenon, worth watching out for.
+
-
+Implicit parameters and monomorphism
+GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the
+Haskell Report) to implicit parameters. For example, consider:
- a1 :: T Int
- a1 = T1 (\xy->x) 3
-
- a2, a3 :: Swizzle
- a2 = MkSwizzle sort
- a3 = MkSwizzle reverse
-
- a4 :: MonadT Maybe
- a4 = let r x = Just x
- b m k = case m of
- Just y -> k y
- Nothing -> Nothing
- in
- MkMonad r b
+ f :: Int -> Int
+ f v = let ?x = 0 in
+ let y = ?x + v in
+ let ?x = 5 in
+ y
+
+Since the binding for y falls under the Monomorphism
+Restriction it is not generalised, so the type of y is
+simply Int, not (?x::Int) => Int.
+Hence, (f 9) returns result 9.
+If you add a type signature for y, then y
+will get type (?x::Int) => Int, so the occurrence of
+y in the body of the let will see the
+inner binding of ?x, so (f 9) will return
+14.
+
+
+
- mkTs :: (forall b. b -> b -> b) -> a -> [T a]
- mkTs f x y = [T1 f x, T1 f y]
-
+
+
+
+Explicitly-kinded quantification
+
+
+Haskell infers the kind of each type variable. Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation,
+just as it is nice to give a type signature for a function. On some occasions,
+it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+
+ data Set cxt a = Set [a]
+ | Unused (cxt a -> ())
+
+The only use for the Unused constructor was to force the correct
+kind for the type variable cxt.
-A lexically scoped type variable can be bound by:
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound. Namely:
-A declaration type signature ()
-An expression type signature ()
-A pattern type signature ()
-Class and instance declarations ()
+data declarations:
+
+ data Set (cxt :: * -> *) a = Set [a]
+
+type declarations:
+
+ type T (f :: * -> *) = f Int
+
+class declarations:
+
+ class (Eq a) => C (f :: * -> *) a where ...
+
+forall's in type signatures:
+
+ f :: forall (cxt :: * -> *). Set cxt Int
+
+
-In Haskell, a programmer-written type signature is implicitly quantifed over
-its free type variables (Section
-4.1.2
-of the Haskel Report).
-Lexically scoped type variables affect this implicit quantification rules
-as follows: any type variable that is in scope is not universally
-quantified. For example, if type variable a is in scope,
-then
-
- (e :: a -> a) means (e :: a -> a)
- (e :: b -> b) means (e :: forall b. b->b)
- (e :: a -> b) means (e :: forall b. a->b)
-
+The parentheses are required. Some of the spaces are required too, to
+separate the lexemes. If you write (f::*->*) you
+will get a parse error, because "::*->*" is a
+single lexeme in Haskell.
+
+As part of the same extension, you can put kind annotations in types
+as well. Thus:
+
+ f :: (Int :: *) -> Int
+ g :: forall a. a -> (a :: *)
+
+The syntax is
+
+ atype ::= '(' ctype '::' kind ')
+
+The parentheses are required.
+
+
-
+
+Arbitrary-rank polymorphism
+
-
-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".
+
+Haskell type signatures are implicitly quantified. The new keyword forall
+allows us to say exactly what this means. For example:
-This only happens if the quantification in f's type
-signature is explicit. For example:
+
- g :: [a] -> [a]
- g (x:xs) = xs ++ [ x :: a ]
+ g :: b -> b
-This program will be rejected, because "a" does not scope
-over the definition of "f", so "x::a"
-means "x::forall a. a" by Haskell's usual implicit
-quantification rules.
-
-
-
-
-Expression type signatures
-
-An expression type signature that has explicit
-quantification (using forall) brings into scope the
-explicitly-quantified
-type variables, in the annotated expression. For example:
+means this:
- f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
+ g :: forall b. (b -> b)
-Here, the type signature forall a. ST s Bool brings the
-type variable s into scope, in the annotated expression
-(op >>= \(x :: STRef s Int) -> g x).
+The two are treated identically.
-
-
-
-Pattern type signatures
-A type signature may occur in any pattern; this is a pattern type
-signature.
-For example:
+However, GHC's type system supports arbitrary-rank
+explicit universal quantification in
+types.
+For example, all the following types are legal:
- -- 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)
+ f1 :: forall a b. a -> b -> a
+ g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
+
+ f2 :: (forall a. a->a) -> Int -> Int
+ g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+
+ f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+
+ f4 :: Int -> (forall a. a -> a)
-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.
+Here, f1 and g1 are rank-1 types, and
+can be written in standard Haskell (e.g. f1 :: a->b->a).
+The forall makes explicit the universal quantification that
+is implicitly added by Haskell.
-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]
-
- k :: T -> T
- k (MkT [t::a]) = MkT t3
- where
- t3::[a] = [t,t,t]
-
-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.
+The functions f2 and g2 have rank-2 types;
+the forall is on the left of a function arrow. As g2
+shows, the polymorphic type on the left of the function arrow can be overloaded.
-If this seems a little odd, we think so too. But we must have
-some way to bring such type variables into scope, else we
-could not name existentially-bound type variables in subequent type signatures.
+The function f3 has a rank-3 type;
+it has rank-2 types on the left of a function arrow.
-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.
+GHC allows types of arbitrary rank; you can nest foralls
+arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
+that restriction has now been lifted.)
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
+
+ On the left or right (see f4, for example)
+of a function arrow
+ As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the f1,f2,f3,g1,g2 above would be valid
+field type signatures.
+ As the type of an implicit parameter
+ In a pattern type signature (see )
+
+Of course forall becomes a keyword; you can't use forall as
+a type variable any more!
-
+
+Examples
+
-
+
-
-Class and instance declarations
+The type of the argument can, as usual, be more general than the type
+required, as (MkSwizzle reverse) shows. (reverse
+does not need the Ord constraint.)
+
-The type variables in the head of a class or instance declaration
-scope over the methods defined in the where part. For example:
+
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example:
+
+
- class C a where
- op :: [a] -> a
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
- op xs = let ys::[a]
- ys = reverse xs
- in
- head ys
+ g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
+ g (MkSwizzle s) xs f = s (map f (s xs))
+
+ h :: MonadT m -> [m a] -> m [a]
+ h m [] = return m []
+ h m (x:xs) = bind m x $ \y ->
+ bind m (h m xs) $ \ys ->
+ return m (y:ys)
+
-
-
+
+In the function h we use the record selectors return
+and bind to extract the polymorphic bind and return functions
+from the MonadT data structure, rather than using pattern
+matching.
+
+
-
-Deriving clause for classes Typeable and Data
+
+Type inference
-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.
+In general, type inference for arbitrary-rank types is undecidable.
+GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
+to get a decidable algorithm by requiring some help from the programmer.
+We do not yet have a formal specification of "some help" but the rule is this:
-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.
+For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it.
-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.
+
+What does it mean to "provide" an explicit type for x? You can do that by
+giving a type signature for x directly, using a pattern type signature
+(), thus:
+
+ \ f :: (forall a. a->a) -> (f True, f 'c')
+
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
+
+ (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
+
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f. Similarly, and more commonly,
+one can give a type signature for the function itself:
+
+ h :: (forall a. a->a) -> (Bool,Char)
+ h f = (f True, f 'c')
+
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument. Here is an example we saw earlier:
+
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
+
+Here we do not need to give a type signature to w, because
+it is an argument of constructor T1 and that tells GHC all
+it needs to know.
-
-
-Generalised derived instances for newtypes
+
+
+
+
+Implicit quantification
-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
+GHC performs implicit quantification as follows. At the top level (only) of
+user-written types, if and only if there is no explicit forall,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them. For example, the following pairs are
+equivalent:
+
+ f :: a -> a
+ f :: forall a. a -> a
-
- newtype Dollars = Dollars Int
-
+ g (x::a) = let
+ h :: a -> b -> b
+ h x y = y
+ in ...
+ g (x::a) = let
+ h :: forall b. a -> b -> b
+ h x y = y
+ in ...
+
+
+
+Notice that GHC does not find the innermost possible quantification
+point. For example:
+
+ f :: (a -> a) -> Int
+ -- MEANS
+ f :: forall a. (a -> a) -> Int
+ -- NOT
+ f :: (forall a. a -> a) -> Int
-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)
- ...
+ g :: (Ord a => a -> a) -> Int
+ -- MEANS the illegal type
+ g :: forall a. (Ord a => a -> a) -> Int
+ -- NOT
+ g :: (forall a. Ord a => a -> a) -> Int
+
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple. If you want the latter type, you
+can write your for-alls explicitly. Indeed, doing so is strongly advised
+for rank-2 types.
+
+
+
+
+
+
+Impredicative polymorphism
+
+GHC supports impredicative polymorphism. This means
+that you can call a polymorphic function at a polymorphic type, and
+parameterise data structures over polymorphic types. For example:
+
+ f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+ f (Just g) = Just (g [3], g "hello")
+ f Nothing = Nothing
-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!
+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.
+
+
+
+Lexically scoped type variables
+
- 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
+GHC supports lexically scoped type variables, without
+which some type signatures are simply impossible to write. For example:
+
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
+
+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!
-
- instance Num Int => Num Dollars
-
+
+Overview
-which just adds or removes the newtype constructor according to the type.
+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.
+
+
+
+A lexically scoped type variable can be bound by:
+
+A declaration type signature ()
+An expression type signature ()
+A pattern type signature ()
+Class and instance declarations ()
+
+In Haskell, a programmer-written type signature is implicitly quantifed over
+its free type variables (Section
+4.1.2
+of the Haskel Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is not universally
+quantified. For example, if type variable a is in scope,
+then
+
+ (e :: a -> a) means (e :: a -> a)
+ (e :: b -> b) means (e :: forall b. b->b)
+ (e :: a -> b) means (e :: forall b. a->b)
+
+
-We can also derive instances of constructor classes in a similar
-way. For example, suppose we have implemented state and failure monad
-transformers, such that
-
- instance Monad m => Monad (State s m)
- instance Monad m => Monad (Failure m)
-
-In Haskell 98, we can define a parsing monad by
-
- type Parser tok m a = State [tok] (Failure m) a
-
+
-which is automatically a monad thanks to the instance declarations
-above. With the extension, we can make the parser type abstract,
-without needing to write an instance of class Monad, via
-
- newtype Parser tok m a = Parser (State [tok] (Failure m) a)
- deriving Monad
+
+Declaration type signatures
+A declaration type signature that has explicit
+quantification (using forall) brings into scope the
+explicitly-quantified
+type variables, in the definition of the named function(s). For example:
+
+ f :: forall a. [a] -> [a]
+ f (x:xs) = xs ++ [ x :: a ]
-In this case the derived instance declaration is of the form
-
- instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
-
-
-Notice that, since Monad is a constructor class, the
-instance is a partial application of the new type, not the
-entire left hand side. We can imagine that the type declaration is
-``eta-converted'' to generate the context of the instance
-declaration.
+The "forall a" brings "a" into scope in
+the definition of "f".
-
-
-We can even derive instances of multi-parameter classes, provided the
-newtype is the last class parameter. In this case, a ``partial
-application'' of the class appears in the deriving
-clause. For example, given the class
-
-
- class StateMonad s m | m -> s where ...
- instance Monad m => StateMonad s (State s m) where ...
-
-then we can derive an instance of StateMonad for Parsers by
-
- newtype Parser tok m a = Parser (State [tok] (Failure m) a)
- deriving (Monad, StateMonad [tok])
+This only happens if the quantification in f's type
+signature is explicit. For example:
+
+ g :: [a] -> [a]
+ g (x:xs) = xs ++ [ x :: a ]
+This program will be rejected, because "a" does not scope
+over the definition of "f", so "x::a"
+means "x::forall a. a" by Haskell's usual implicit
+quantification rules.
+
+
-The derived instance is obtained by completing the application of the
-class to the new type:
+
+Expression type signatures
-
- instance StateMonad [tok] (State [tok] (Failure m)) =>
- StateMonad [tok] (Parser tok m)
+An expression type signature that has explicit
+quantification (using forall) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression. For example:
+
+ f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
+Here, the type signature forall a. ST s Bool brings the
+type variable s into scope, in the annotated expression
+(op >>= \(x :: STRef s Int) -> g x).
-
-As a result of this extension, all derived instances in newtype
- declarations are treated uniformly (and implemented just by reusing
-the dictionary for the representation type), except
-Show and Read, which really behave differently for
-the newtype and its representation.
-
- A more precise specification
+
+Pattern type signatures
-Derived instance declarations are constructed as follows. Consider the
-declaration (after expansion of any type synonyms)
-
-
- newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm)
-
-
-where
-
-
- The ci are partial applications of
- classes of the form C t1'...tj', where the arity of C
- is exactly j+1. That is, C lacks exactly one type argument.
-
-
- The k is chosen so that ci (T v1...vk) is well-kinded.
-
-
- The type t is an arbitrary type.
-
-
- The type variables vk+1...vn do not occur in t,
- nor in the ci, and
-
-
- None of the ci is Read, Show,
- Typeable, or Data. These classes
- should not "look through" the type or its constructor. You can still
- derive these classes for a newtype, but it happens in the usual way, not
- via this new mechanism.
-
-
-Then, for each ci, the derived instance
-declaration is:
-
- instance ci t => ci (T v1...vk)
+A type signature may occur in any pattern; this is a pattern type
+signature.
+For example:
+
+ -- f and g assume that 'a' is already in scope
+ f = \(x::Int, y::a) -> x
+ g (x::a) = x
+ h ((x,y) :: (Int,Bool)) = (y,x)
-As an example which does not work, consider
-
- newtype NonMonad m s = NonMonad (State s m s) deriving Monad
-
-Here we cannot derive the instance
-
- instance Monad (State s m) => Monad (NonMonad m)
-
-
-because the type variable s occurs in State s m,
-and so cannot be "eta-converted" away. It is a good thing that this
-deriving clause is rejected, because NonMonad m is
-not, in fact, a monad --- for the same reason. Try defining
->>= with the correct type: you won't be able to.
+In the case where all the type variables in the pattern type sigature are
+already in scope (i.e. bound by the enclosing context), matters are simple: the
+signature simply constrains the type of the pattern in the obvious way.
+There is only one situation in which you can write a pattern type signature that
+mentions a type variable that is not already in scope, namely in pattern match
+of an existential data constructor. For example:
+
+ data T = forall a. MkT [a]
-Notice also that the order of class parameters becomes
-important, since we can only derive instances for the last one. If the
-StateMonad class above were instead defined as
-
-
- class StateMonad m s | m -> s where ...
+ k :: T -> T
+ k (MkT [t::a]) = MkT t3
+ where
+ t3::[a] = [t,t,t]
-
-then we would not have been able to derive an instance for the
-Parser type above. We hypothesise that multi-parameter
-classes usually have one "main" parameter for which deriving new
-instances is most interesting.
+Here, the pattern type signature (t::a) mentions a lexical type
+variable that is not already in scope. Indeed, it cannot already be in scope,
+because it is bound by the pattern match. GHC's rule is that in this situation
+(and only then), a pattern type signature can mention a type variable that is
+not already in scope; the effect is to bring it into scope, standing for the
+existentially-bound type variable.
-Lastly, all of this applies only for classes other than
-Read, Show, Typeable,
-and Data, for which the built-in derivation applies (section
-4.3.3. of the Haskell Report).
-(For the standard classes Eq, Ord,
-Ix, and Bounded it is immaterial whether
-the standard method is used or the one described here.)
+
+If this seems a little odd, we think so too. But we must have
+some way to bring such type variables into scope, else we
+could not name existentially-bound type variables in subequent type signatures.
+
+This is (now) the only situation in which a pattern type
+signature is allowed to mention a lexical variable that is not already in
+scope.
+For example, both f and g would be
+illegal if a was not already in scope.
+
+
+
-
+
+
+Class and instance declarations
+
+The type variables in the head of a class or instance declaration
+scope over the methods defined in the where part. For example:
+
+
+
+ class C a where
+ op :: [a] -> a
+
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
+
+
+
Generalised typing of mutually recursive bindings
@@ -3815,186 +4062,84 @@ pattern binding must have the same context. For example, this is fine:
-
-
-
-
-
-
-Generalised Algebraic Data Types (GADTs)
+
+Overloaded string literals
+
-Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing you
-to give the type signatures of constructors explicitly. For example:
+
+GHC supports overloaded string literals. Normally a
+string literal has type String, but with overloaded string
+literals enabled (with -foverloaded-strings)
+ a string literal has type (IsString a) => a.
+
+
+This means that the usual string syntax can be used, e.g., for packed strings
+and other variations of string like types. String literals behave very much
+like integer literals, i.e., they can be used in both expressions and patterns.
+If used in a pattern the literal with be replaced by an equality test, in the same
+way as an integer literal is.
+
+
+The class IsString is defined as:
- data Term a where
- Lit :: Int -> Term Int
- Succ :: Term Int -> Term Int
- IsZero :: Term Int -> Term Bool
- If :: Term Bool -> Term a -> Term a -> Term a
- Pair :: Term a -> Term b -> Term (a,b)
+class IsString a where
+ fromString :: String -> a
-Notice that the return type of the constructors is not always Term a, as is the
-case with ordinary vanilla data types. Now we can write a well-typed eval function
-for these Terms:
+The only predefined instance is the obvious one to make strings work as usual:
- eval :: Term a -> a
- eval (Lit i) = i
- eval (Succ t) = 1 + eval t
- eval (IsZero t) = eval t == 0
- eval (If b e1 e2) = if eval b then eval e1 else eval e2
- eval (Pair e1 e2) = (eval e1, eval e2)
+instance IsString [Char] where
+ fromString cs = cs
-These and many other examples are given in papers by Hongwei Xi, and
-Tim Sheard. There is a longer introduction
-on the wiki,
-and Ralf Hinze's
-Fun with phantom types also has a number of examples. Note that papers
-may use different notation to that implemented in GHC.
+The class IsString is not in scope by default. If you want to mention
+it explicitly (for exmaple, to give an instance declaration for it), you can import it
+from module GHC.Exts.
-The rest of this section outlines the extensions to GHC that support GADTs.
-It is far from comprehensive, but the design closely follows that described in
-the paper Simple
-unification-based type inference for GADTs,
-which appeared in ICFP 2006.
+Haskell's defaulting mechanism is extended to cover string literals, when is specified.
+Specifically:
- Data type declarations have a 'where' form, as exemplified above. The type signature of
-each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal
-Haskell data type declaration, the type variable(s) in the "data Term a where" header
-have no scope. Indeed, one can write a kind signature instead:
-
- data Term :: * -> * where ...
-
-or even a mixture of the two:
-
- data Foo a :: (* -> *) -> * where ...
-
-The type variables (if given) may be explicitly kinded, so we could also write the header for Foo
-like this:
-
- data Foo a (b :: * -> *) where ...
-
-
-
-
-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 }
-
-
-
-
-
+
+
@@ -4103,6 +4248,14 @@ Tim Sheard is going to expand it.)
(It would make sense to do so, but it's hard to implement.)
+
+ Furthermore, you can only run a function at compile time if it is imported
+ from another module that is not part of a mutually-recursive group of modules
+ that includes the module currently being compiled. For example, when compiling module A,
+ you can only run Template Haskell functions imported from B if B does not import A (directly or indirectly).
+ The reason should be clear: to run B we must compile and run A, but we are currently type-checking A.
+
+
The flag -ddump-splices shows the expansion of all top-level splices as they happen.
@@ -4722,7 +4875,7 @@ Because the preprocessor targets Haskell (rather than Core),
-
+Bang patterns
Bang patterns
@@ -4737,7 +4890,7 @@ than the material below.
Bang patterns are enabled by the flag .
-
+Informal description of bang patterns
@@ -4792,7 +4945,7 @@ is part of the syntax of let bindings.
-
+Syntax and semantics
@@ -4807,7 +4960,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:
@@ -4866,7 +5019,7 @@ a module.
-
+Assertions
Assertions
@@ -5835,12 +5988,6 @@ The following are good consumers:
- length
-
-
-
-
-++ (on its first argument)
@@ -6130,6 +6277,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.
@@ -6188,6 +6351,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
@@ -6203,7 +6371,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.
+
+
+