[[project @ 2003-07-28 13:31:37 by simonpj] simonpj**20030728133137 Reorganise the type-system-extension part of GlaExts docs ] { hunk ./ghc/docs/users_guide/glasgow_exts.sgml 777 - + + +Data types and type synonyms + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 799 - + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 801 - + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 852 - + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 854 - -Explicitly-kinded quantification + +Liberalised type synonyms hunk ./ghc/docs/users_guide/glasgow_exts.sgml 858 -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. +Type synonmys are like macros at the type level, and +GHC does validity checking on types only after expanding type synonyms. +That means that GHC can be very much more liberal about type synonyms than Haskell 98: + + You can write a forall (including overloading) +in a type synonym, thus: + + type Discard a = forall b. Show b => a -> b -> (a, String) + + f :: Discard a + f x y = (x, show y) + + g :: Discard Int -> (Int,Bool) -- A rank-2 type + g f = f Int True + + + + + +You can write an unboxed tuple in a type synonym: + + type Pr = (# Int, Int #) + + h :: Int -> Pr + h x = (# x, x #) + + + + +You can apply a type synonym to a forall type: + + type Foo a = a -> a -> Bool + + f :: Foo (forall b. b->b) + +After expanding the synonym, f has the legal (in GHC) type: + + f :: (forall b. b->b) -> (forall b. b->b) -> Bool + + + + +You can apply a type synonym to a partially applied type synonym: + + type Generic i o = forall x. i x -> o x + type Id x = x + + foo :: Generic Id [] + +After epxanding the synonym, foo has the legal (in GHC) type: + + foo :: forall x. x -> [x] + + + + + + + +GHC currently does kind checking before expanding synonyms (though even that +could be changed.) hunk ./ghc/docs/users_guide/glasgow_exts.sgml 921 -GHC now instead allows you to specify the kind of a type variable directly, wherever -a type variable is explicitly bound. Namely: +After expanding type synonyms, GHC does validity checking on types, looking for +the following mal-formedness which isn't detected simply by kind checking: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 924 -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 - + +Type constructor applied to a type involving for-alls. + + +Unboxed tuple on left of an arrow. + + +Partially-applied type synonym. + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 934 +So, for example, +this will be rejected: + + type Pr = (# Int, Int #) + + h :: Pr -> Int + h x = ... + +because GHC does not allow unboxed tuples on the left of a function arrow. hunk ./ghc/docs/users_guide/glasgow_exts.sgml 944 + + + + +Existentially quantified data constructors + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 952 -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. +The idea of using existential quantification in data type declarations +was suggested by Laufer (I believe, thought doubtless someone will +correct me), and implemented in Hope+. It's been in Lennart +Augustsson's hbc Haskell compiler for several years, and +proved very useful. Here's the idea. Consider the declaration: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 960 -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. + + + data Foo = forall a. MkFoo a (a -> Bool) + | Nil + + + + + +The data type Foo has two constructors with types: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 971 - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 972 + + + + MkFoo :: forall a. a -> (a -> Bool) -> Foo + Nil :: Foo + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 981 - -Class method types - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 982 -Haskell 98 prohibits class method types to mention constraints on the -class type variable, thus: +Notice that the type variable a in the type of MkFoo +does not appear in the data type itself, which is plain Foo. +For example, the following expression is fine: + + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 990 - class Seq s a where - fromList :: [a] -> s a - elem :: Eq a => a -> s a -> Bool + [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] hunk ./ghc/docs/users_guide/glasgow_exts.sgml 992 -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). + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 994 + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 996 -With the GHC lifts this restriction. +Here, (MkFoo 3 even) packages an integer with a function +even that maps an integer to Bool; and MkFoo 'c' +isUpper packages a character with a compatible function. These +two things are each of type Foo and can be put in a list. hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1002 - + +What can we do with a value of type Foo?. In particular, +what happens when we pattern-match on MkFoo? + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1007 - -Multi-parameter type classes - + + + + f (MkFoo val fn) = ??? + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1016 -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). +Since all we know about val and fn is that they +are compatible, the only (useful) thing we can do with them is to +apply fn to val to get a boolean. For example: + + + + + + f :: Foo -> Bool + f (MkFoo val fn) = fn val + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1030 + +What this allows us to do is to package heterogenous values +together with a bunch of functions that manipulate them, and then treat +that collection of packages in a uniform manner. You can express +quite a bit of object-oriented-like programming this way. + + + +Why existential? + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1041 - -Types + +What has this to do with existential quantification? +Simply that MkFoo has the (nearly) isomorphic type + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1047 -GHC imposes the following restrictions on the form of a qualified -type, whether declared in a type signature -or inferred. Consider the type: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1049 - forall tv1..tvn (c1, ...,cn) => type + MkFoo :: (exists a . (a, a -> Bool)) -> Foo hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1052 -(Here, I write the "foralls" explicitly, although the Haskell source -language omits them; in Haskell 1.4, 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 ). hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1055 +But Haskell programmers can safely think of the ordinary +universally quantified type given above, thereby avoiding +adding a new existential quantification construct. + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1060 - - + + + +Type classes hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1066 - Each universally quantified type variable -tvi must be reachable from type. +An easy extension (implemented in hbc) is to allow +arbitrary contexts before the constructor. For example: + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1070 -A type variable is "reachable" if it it is functionally dependent -(see ) -on the type variables free in type. -The reason for this is that a value with a type that does not obey -this restriction could not be used without introducing -ambiguity. -Here, for example, is an illegal type: + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1072 + +data Baz = forall a. Eq a => Baz1 a a + | forall b. Show b => Baz2 b (b -> b) + + + + + +The two constructors have the types you'd expect: + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1086 - forall a. Eq a => Int +Baz1 :: forall a. Eq a => a -> a -> Baz +Baz2 :: forall b. Show b => b -> (b -> b) -> Baz hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1090 + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1092 -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. + +But when pattern matching on Baz1 the matched values can be compared +for equality, and when pattern matching on Baz2 the first matched +value can be converted to a string (as well as applying the function to it). +So this program is legal: + + + + + + f :: Baz -> String + f (Baz1 p q) | p == q = "Yes" + | otherwise = "No" + f (Baz2 v fn) = show (fn v) + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1109 - + + +Operationally, in a dictionary-passing implementation, the +constructors Baz1 and Baz2 must store the +dictionaries for Eq and Show respectively, and +extract it on pattern matching. + + + +Notice the way that the syntax fits smoothly with that used for +universal quantification earlier. + + + + + +Restrictions + + +There are several restrictions on the ways in which existentially-quantified +constructors can be use. + + + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1138 - Every constraint ci must mention at least one of the -universally quantified type variables tvi. + When pattern matching, each pattern match introduces a new, +distinct, type for each existential type variable. These types cannot +be unified with any other type, nor can they escape from the scope of +the pattern match. For example, these fragments are incorrect: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1143 -For example, this type is OK because C a b mentions the -universally quantified type variable b: + + +f1 (MkFoo a f) = a + + + +Here, the type bound by MkFoo "escapes", because a +is the result of f1. One way to see why this is wrong is to +ask what type f1 has: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1155 - forall a. C a b => burble + f1 :: Foo -> a -- Weird! hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1159 -The next type is illegal because the constraint Eq b does not -mention a: +What is this "a" in the result type? Clearly we don't mean +this: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1164 - forall a. Eq b => burble + f1 :: forall a. Foo -> a -- Wrong! hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1168 -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 original program is just plain wrong. Here's another sort of error + + + + f2 (Baz1 a b) (Baz1 p q) = a==q + + + +It's ok to say a==b or p==q, but +a==q is wrong because it equates the two distinct types arising +from the two Baz1 constructors. + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1183 + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1185 - + +You can't pattern-match on an existentially quantified +constructor in a let or where group of +bindings. So this is illegal: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1190 - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1191 + + f3 x = a==b where { Baz1 a b = x } + + +Instead, use a case expression: + + + f3 x = case x of Baz1 a b -> a==b + + +In general, you can only pattern-match +on an existentially-quantified constructor in a case expression or +in the patterns of a function definition. + +The reason for this restriction is really an implementation one. +Type-checking binding groups is already a nightmare without +existentials complicating the picture. Also an existential pattern +binding at the top level of a module doesn't make sense, because it's +not clear how to prevent the existentially-quantified type "escaping". +So for now, there's a simple-to-state restriction. We'll see how +annoying it is. hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1213 - -Unlike Haskell 1.4, constraints in types do not have to be of -the form (class type-variables). Thus, these type signatures -are perfectly OK hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1214 + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1218 +You can't use existential quantification for newtype +declarations. So this is illegal: + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1223 - f :: Eq (m a) => [m a] -> [m a] - g :: Eq [a] => ... + newtype T = forall a. Ord a => MkT a hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1226 + +Reason: a value of type T must be represented as a pair +of a dictionary for Ord t and a value of type t. +That contradicts the idea that newtype should have no +concrete representation. You can get just the same efficiency and effect +by using data instead of newtype. If there is no +overloading involved, then there is more of a case for allowing +an existentially-quantified newtype, because the data +because the data version does carry an implementation cost, +but single-field existentially quantified constructors aren't much +use. So the simple restriction (no existential stuff on newtype) +stands, unless there are convincing reasons to change it. + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1241 + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1245 -This choice recovers principal types, a property that Haskell 1.4 does not have. + You can't use deriving to define instances of a +data type with existentially quantified data constructors. + +Reason: in most cases it would not make sense. For example:# + + +data T = forall a. MkT [a] deriving( Eq ) + + +To derive Eq in the standard way we would need to have equality +between the single component of two MkT constructors: + + +instance Eq T where + (MkT a) == (MkT b) = ??? + + +But a and b have distinct types, and so can't be compared. +It's just about possible to imagine examples in which the derived instance +would make sense, but it seems altogether simpler simply to prohibit such +declarations. Define your own instances! + + + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1273 + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1276 - + + + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1284 - +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: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1402 + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1404 + +Class method types + +Haskell 98 prohibits class method types to mention constraints on the +class type variable, thus: + + class Seq s a where + fromList :: [a] -> s a + elem :: Eq a => a -> s a -> Bool + +The type of elem is illegal in Haskell 98, because it +contains the constraint Eq a, constrains only the +class type variable (in this case a). + + +With the GHC lifts this restriction. hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1424 - -Instance declarations + + + +Type signatures + +The context of a type signature + +Unlike Haskell 1.4, constraints in types do not have to be of +the form (class type-variables). Thus, these type signatures +are perfectly OK + + f :: Eq (m a) => [m a] -> [m a] + g :: Eq [a] => ... + +This choice recovers principal types, a property that Haskell 1.4 does not have. + + +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 1.4, 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 ). + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1461 - Instance declarations may not overlap. The two instance + Each universally quantified type variable +tvi must be reachable from type. + +A type variable is "reachable" if it it is functionally dependent +(see ) +on the type variables free in type. +The reason for this is that a value with a type that does not obey +this restriction could not be used without introducing +ambiguity. +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. + + + + + + + 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 + + + + + + + + +Instance declarations + + +Overlapping instances + +In general, instance declarations may not overlap. The two instance hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1673 - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1674 - - - - - There are no restrictions on the type in an instance -head, except that at least one must not be a type variable. -The instance "head" is the bit after the "=>" in an instance decl. For -example, these are OK: - - - - instance C Int a where ... - - instance D (Int, Int) where ... - - instance E [[a]] where ... - - - -Note that instance heads may contain repeated type variables. -For example, this is OK: - - - - instance Stateful (ST s) (MutVar s) where ... - + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1676 -See for an experimental -extension to lift this restriction. - - - + +Type synonyms in the instance head hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1680 - Unlike Haskell 1.4, instance heads may use type -synonyms. As always, using a type synonym is just shorthand for +Unlike Haskell 1.4, 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 hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1716 - - + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1718 - -The types in an instance-declaration context must all -be type variables. Thus + +Undecidable instances hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1721 +An instance declaration must normally obey the following rules: + +At least one of the types in the head of +an instance declaration must not be a type variable. +For example, these are OK: hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1728 -instance C a b => Eq (a,b) where ... - + instance C Int a where ... hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1730 + instance D (Int, Int) where ... hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1732 -is OK, but + instance E [[a]] where ... + +but this is not: + + instance F a where ... + +Note that instance heads may contain repeated type variables. +For example, this is OK: + + instance Stateful (ST s) (MutVar s) where ... + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1747 + +All of the types in the context of +an instance declaration must be type variables. +Thus + +instance C a b => Eq (a,b) where ... + +is OK, but hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1758 - - -is not OK. See for an experimental -extension to lift this restriction. - - - +is not OK. hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1761 - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1762 - - - - - - - - -Undecidable instances - -The rules for instance declarations state that: - -At least one of the types in the head of -an instance declaration must not be a type variable. - -All of the types in the context of -an instance declaration must be type variables. - - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1822 + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1828 -Implicit parameters - +Implicit parameters hunk ./ghc/docs/users_guide/glasgow_exts.sgml 1987 -Linear implicit parameters - +Linear implicit parameters hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2179 + + +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 + + + + + +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. + + + + hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2546 - -Liberalised type synonyms - - - -Type synonmys are like macros at the type level, and -GHC does validity checking on types only after expanding type synonyms. -That means that GHC can be very much more liberal about type synonyms than Haskell 98: - - You can write a forall (including overloading) -in a type synonym, thus: - - type Discard a = forall b. Show b => a -> b -> (a, String) - - f :: Discard a - f x y = (x, show y) - - g :: Discard Int -> (Int,Bool) -- A rank-2 type - g f = f Int True - - - - - -You can write an unboxed tuple in a type synonym: - - type Pr = (# Int, Int #) - - h :: Int -> Pr - h x = (# x, x #) - - - - -You can apply a type synonym to a forall type: - - type Foo a = a -> a -> Bool - - f :: Foo (forall b. b->b) - -After expanding the synonym, f has the legal (in GHC) type: - - f :: (forall b. b->b) -> (forall b. b->b) -> Bool - - - - -You can apply a type synonym to a partially applied type synonym: - - type Generic i o = forall x. i x -> o x - type Id x = x - - foo :: Generic Id [] - -After epxanding the synonym, foo has the legal (in GHC) type: - - foo :: forall x. x -> [x] - - - - - - - -GHC currently does kind checking before expanding synonyms (though even that -could be changed.) - - -After expanding type synonyms, GHC does validity checking on types, looking for -the following mal-formedness which isn't detected simply by kind checking: - - -Type constructor applied to a type involving for-alls. - - -Unboxed tuple on left of an arrow. - - -Partially-applied type synonym. - - -So, for example, -this will be rejected: - - type Pr = (# Int, Int #) - - h :: Pr -> Int - h x = ... - -because GHC does not allow unboxed tuples on the left of a function arrow. - - - - -For-all hoisting - -It is often convenient to use generalised type synonyms at the right hand -end of an arrow, thus: - - type Discard a = forall b. a -> b -> a hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2547 - 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 - - - - - - -Existentially quantified data constructors - - - -The idea of using existential quantification in data type declarations -was suggested by Laufer (I believe, thought doubtless someone will -correct me), and implemented in Hope+. It's been in Lennart -Augustsson's hbc Haskell compiler for several years, and -proved very useful. Here's the idea. Consider the declaration: - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2548 - - - - data Foo = forall a. MkFoo a (a -> Bool) - | Nil - - - - - -The data type Foo has two constructors with types: - - - - - - MkFoo :: forall a. a -> (a -> Bool) -> Foo - Nil :: Foo - - - - - -Notice that the type variable a in the type of MkFoo -does not appear in the data type itself, which is plain Foo. -For example, the following expression is fine: - - - - - - [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] - - - - - -Here, (MkFoo 3 even) packages an integer with a function -even that maps an integer to Bool; and MkFoo 'c' -isUpper packages a character with a compatible function. These -two things are each of type Foo and can be put in a list. - - - -What can we do with a value of type Foo?. In particular, -what happens when we pattern-match on MkFoo? - - - - - - f (MkFoo val fn) = ??? - - - - - -Since all we know about val and fn is that they -are compatible, the only (useful) thing we can do with them is to -apply fn to val to get a boolean. For example: - - - - - - f :: Foo -> Bool - f (MkFoo val fn) = fn val - - - - - -What this allows us to do is to package heterogenous values -together with a bunch of functions that manipulate them, and then treat -that collection of packages in a uniform manner. You can express -quite a bit of object-oriented-like programming this way. - - - -Why existential? - - - -What has this to do with existential quantification? -Simply that MkFoo has the (nearly) isomorphic type - - - - - - MkFoo :: (exists a . (a, a -> Bool)) -> Foo - - - - - -But Haskell programmers can safely think of the ordinary -universally quantified type given above, thereby avoiding -adding a new existential quantification construct. - - - - - -Type classes - - -An easy extension (implemented in hbc) is to allow -arbitrary contexts before the constructor. For example: - - - - - -data Baz = forall a. Eq a => Baz1 a a - | forall b. Show b => Baz2 b (b -> b) - - - - - -The two constructors have the types you'd expect: - - - - - -Baz1 :: forall a. Eq a => a -> a -> Baz -Baz2 :: forall b. Show b => b -> (b -> b) -> Baz - - - - - -But when pattern matching on Baz1 the matched values can be compared -for equality, and when pattern matching on Baz2 the first matched -value can be converted to a string (as well as applying the function to it). -So this program is legal: - - - - - - f :: Baz -> String - f (Baz1 p q) | p == q = "Yes" - | otherwise = "No" - f (Baz2 v fn) = show (fn v) - - - - - -Operationally, in a dictionary-passing implementation, the -constructors Baz1 and Baz2 must store the -dictionaries for Eq and Show respectively, and -extract it on pattern matching. - - - -Notice the way that the syntax fits smoothly with that used for -universal quantification earlier. - - - - - -Restrictions - - -There are several restrictions on the ways in which existentially-quantified -constructors can be use. - - - - - - - - - When pattern matching, each pattern match introduces a new, -distinct, type for each existential type variable. These types cannot -be unified with any other type, nor can they escape from the scope of -the pattern match. For example, these fragments are incorrect: - - - -f1 (MkFoo a f) = a - - - -Here, the type bound by MkFoo "escapes", because a -is the result of f1. One way to see why this is wrong is to -ask what type f1 has: - - - - f1 :: Foo -> a -- Weird! - - - -What is this "a" in the result type? Clearly we don't mean -this: - - - - f1 :: forall a. Foo -> a -- Wrong! - - - -The original program is just plain wrong. Here's another sort of error - - - - f2 (Baz1 a b) (Baz1 p q) = a==q - - - -It's ok to say a==b or p==q, but -a==q is wrong because it equates the two distinct types arising -from the two Baz1 constructors. - - - - - - - -You can't pattern-match on an existentially quantified -constructor in a let or where group of -bindings. So this is illegal: - - - - f3 x = a==b where { Baz1 a b = x } - - -Instead, use a case expression: - - - f3 x = case x of Baz1 a b -> a==b - - -In general, you can only pattern-match -on an existentially-quantified constructor in a case expression or -in the patterns of a function definition. - -The reason for this restriction is really an implementation one. -Type-checking binding groups is already a nightmare without -existentials complicating the picture. Also an existential pattern -binding at the top level of a module doesn't make sense, because it's -not clear how to prevent the existentially-quantified type "escaping". -So for now, there's a simple-to-state restriction. We'll see how -annoying it is. - - - - - - -You can't use existential quantification for newtype -declarations. So this is illegal: - - - - newtype T = forall a. Ord a => MkT a - - - -Reason: a value of type T must be represented as a pair -of a dictionary for Ord t and a value of type t. -That contradicts the idea that newtype should have no -concrete representation. You can get just the same efficiency and effect -by using data instead of newtype. If there is no -overloading involved, then there is more of a case for allowing -an existentially-quantified newtype, because the data -because the data version does carry an implementation cost, -but single-field existentially quantified constructors aren't much -use. So the simple restriction (no existential stuff on newtype) -stands, unless there 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:# - - -data T = forall a. MkT [a] deriving( Eq ) - - -To derive Eq in the standard way we would need to have equality -between the single component of two MkT constructors: - - -instance Eq T where - (MkT a) == (MkT b) = ??? - - -But a and b have distinct types, and so can't be compared. -It's just about possible to imagine examples in which the derived instance -would make sense, but it seems altogether simpler simply to prohibit such -declarations. Define your own instances! - - - - - - - - - - hunk ./ghc/docs/users_guide/glasgow_exts.sgml 5147 + }