From: simonpj Date: Wed, 26 Oct 2005 13:03:39 +0000 (+0000) Subject: [project @ 2005-10-26 13:03:39 by simonpj] X-Git-Tag: Initial_conversion_from_CVS_complete~125 X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=03aaa24e66ad6191d160c3d12377b4e56feaa435 [project @ 2005-10-26 13:03:39 by simonpj] Improve documentation of typeclass extensions; merge to stable if it goes easily --- diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml index c9dfaf0..36b7bf8 100644 --- a/ghc/docs/users_guide/glasgow_exts.xml +++ b/ghc/docs/users_guide/glasgow_exts.xml @@ -1429,19 +1429,20 @@ declarations. Define your own instances! Class declarations -This section documents GHC's implementation of multi-parameter type -classes. There's lots of background in the paper Type classes: exploring the design space (Simon Peyton Jones, Mark Jones, Erik Meijer). -There are the following constraints on class declarations: - - +All the extensions are enabled by the flag. + + +Multi-parameter type classes - Multi-parameter type classes are permitted. For example: +Multi-parameter type classes are permitted. For example: @@ -1450,39 +1451,16 @@ There are the following constraints on class declarations: ...etc. - - - - - - - The class hierarchy must be acyclic. However, the definition -of "acyclic" involves only the superclass relationships. For example, -this is OK: - - - - class C a where { - op :: D b => a -> b -> b - } - - class C a => D a where { ... } - - - -Here, C is a superclass of D, but it's OK for a -class operation op of C to mention D. (It -would not be OK for D to be a superclass of C.) + - - - + +The superclasses of a class declaration - There are no restrictions on the context in 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: +be acyclic. So these class declarations are OK: @@ -1495,62 +1473,33 @@ be acyclic. So these class declarations are OK: - - - - - All of the class type variables must be reachable (in the sense -mentioned in ) -from the free variables of each method type -. For example: +As in Haskell 98, The class hierarchy must be acyclic. However, the definition +of "acyclic" involves only the superclass relationships. For example, +this is OK: - class Coll s a where - empty :: s - insert :: s -> a -> s - - - -is not OK, because the type of empty doesn't mention -a. This rule is a consequence of Rule 1(a), above, for -types, and has the same motivation. - -Sometimes, offending class declarations exhibit misunderstandings. For -example, Coll might be rewritten - + class C a where { + op :: D b => a -> b -> b + } - - class Coll s a where - empty :: s a - insert :: s a -> a -> s a + class C a => D a where { ... } -which makes the connection between the type of a collection of -a's (namely (s a)) and the element type a. -Occasionally this really doesn't work, in which case you can split the -class like this: - - - - class CollE s where - empty :: s - - class CollE s => Coll s a where - insert :: s -> a -> s - +Here, C is a superclass of D, but it's OK for a +class operation op of C to mention D. (It +would not be OK for D to be a superclass of C.) + + - - - - Class method types + Haskell 98 prohibits class method types to mention constraints on the class type variable, thus: @@ -1562,186 +1511,120 @@ class type variable, thus: 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. - -With the GHC lifts this restriction. - + - - -Type signatures + +Functional dependencies + -The context of a type signature + 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, +. + -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 +Functional dependencies are introduced by a vertical bar in the syntax of a +class declaration; e.g. - g :: Eq [a] => ... - g :: Ord (T a ()) => ... + class (Monad m) => MonadState s m | m -> s where ... + + class Foo a b c | a b -> c where ... +There should be more documentation, but there isn't (yet). Yell if you need it. -GHC imposes the following restrictions on the constraints in a type signature. -Consider the type: +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: - forall tv1..tvn (c1, ...,cn) => type + class Coll s a where + empty :: s + insert :: s -> a -> s -(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 ). - - - - - - - - - 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: - - +is not OK, because the type of empty doesn't mention +a. Functional dependencies can make the type variable +reachable: - forall a. Eq a => Int + class Coll s a | s -> a where + empty :: s + insert :: s -> a -> s +Alternatively Coll might be rewritten -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 -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: - 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 Coll s a where + empty :: s a + insert :: s a -> a -> s a -This is fine, because in fact a does functionally determine b -but that is not immediately apparent from f's type. - - - - - 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: +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: - forall a. C a b => burble - - + class CollE s where + empty :: s -The next type is illegal because the constraint Eq b does not -mention a: + class CollE s => Coll s a where + insert :: s -> a -> s + + + - - 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. - - + - + +Instance declarations - - + +Instance heads - -For-all hoisting -It is often convenient to use generalised type synonyms (see ) at the right hand -end of an arrow, thus: - - type Discard a = forall b. a -> b -> a - - g :: Int -> Discard Int - g x y z = x+y - -Simply expanding the type synonym would give - - g :: Int -> (forall b. Int -> b -> Int) - -but GHC "hoists" the forall to give the isomorphic type - - g :: forall b. Int -> Int -> b -> Int - -In general, the rule is this: to determine the type specified by any explicit -user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly -performs the transformation: - - type1 -> forall a1..an. context2 => type2 -==> - forall a1..an. context2 => type1 -> type2 - -(In fact, GHC tries to retain as much synonym information as possible for use in -error messages, but that is a usability issue.) This rule applies, of course, whether -or not the forall comes from a synonym. For example, here is another -valid way to write g's type signature: - - g :: Int -> Int -> forall b. b -> Int - +The head of an instance declaration is the part to the +right of the "=>". 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. -When doing this hoisting operation, GHC eliminates duplicate constraints. For -example: - - type Foo a = (?x::Int) => Bool -> a - g :: Foo (Foo Int) - -means +The flag lifts this restriction and allows the +instance head to be of form C t1 ... tn where t1 +... tn are arbitrary types (provided, of course, everything is +well-kinded). In particular, types ti can be type variables +or structured types, and can contain repeated occurrences of a single type +variable. +Examples: - g :: (?x::Int) => Bool -> Bool -> Int + instance Eq (T a a) where ... + -- Repeated type variable + + instance Eq (S [a]) where ... + -- Structured type + + instance C Int [a] where ... + -- Multiple parameters - - - - -Instance declarations - Overlapping instances @@ -1892,7 +1775,7 @@ but this is not: instance F a where ... -Note that instance heads may contain repeated type variables. +Note that instance heads may contain repeated type variables (). For example, this is OK: instance Stateful (ST s) (MutVar s) where ... @@ -1981,6 +1864,174 @@ allowing these idioms interesting idioms. + +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 + + g :: Eq [a] => ... + g :: Ord (T a ()) => ... + + + +GHC imposes the following restrictions on the constraints in a type signature. +Consider the type: + + + forall tv1..tvn (c1, ...,cn) => type + + +(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 ). + + + + + + + + + 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: + + + + forall a. Eq a => Int + + + +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 +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: + + class C a b | a -> b where ... + class C a b => D a b where ... + f :: forall a b. D a b => a -> a + +This is fine, because in fact a does functionally determine b +but that is not immediately apparent from f's type. + + + + + + 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: + + + + forall a. C a b => burble + + + +The next type is illegal because the constraint Eq b does not +mention a: + + + + forall a. Eq b => burble + + + +The reason for this restriction is milder than the other one. The +excluded types are never useful or necessary (because the offending +context doesn't need to be witnessed at this point; it can be floated +out). Furthermore, floating them out increases sharing. Lastly, +excluding them is a conservative choice; it leaves a patch of +territory free in case we need it later. + + + + + + + + + + +For-all hoisting + +It is often convenient to use generalised type synonyms (see ) at the right hand +end of an arrow, thus: + + type Discard a = forall b. a -> b -> a + + g :: Int -> Discard Int + g x y z = x+y + +Simply expanding the type synonym would give + + g :: Int -> (forall b. Int -> b -> Int) + +but GHC "hoists" the forall to give the isomorphic type + + g :: forall b. Int -> Int -> b -> Int + +In general, the rule is this: to determine the type specified by any explicit +user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly +performs the transformation: + + type1 -> forall a1..an. context2 => type2 +==> + forall a1..an. context2 => type1 -> type2 + +(In fact, GHC tries to retain as much synonym information as possible for use in +error messages, but that is a usability issue.) This rule applies, of course, whether +or not the forall comes from a synonym. For example, here is another +valid way to write g's type signature: + + g :: Int -> Int -> forall b. b -> Int + + + +When doing this hoisting operation, GHC eliminates duplicate constraints. For +example: + + type Foo a = (?x::Int) => Bool -> a + g :: Foo (Foo Int) + +means + + g :: (?x::Int) => Bool -> Bool -> Int + + + + + + + Implicit parameters @@ -2378,30 +2429,6 @@ and you'd be right. That is why they are an experimental feature. - -Functional dependencies - - - Functional dependencies are implemented as described by Mark Jones -in “Type Classes with Functional Dependencies”, Mark P. Jones, -In Proceedings of the 9th European Symposium on Programming, -ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782, -. - - -Functional dependencies are introduced by a vertical bar in the syntax of a -class declaration; e.g. - - class (Monad m) => MonadState s m | m -> s where ... - - class Foo a b c | a b -> c where ... - -There should be more documentation, but there isn't (yet). Yell if you need it. - - - - - Explicitly-kinded quantification