-</ProgramListing>
-
-it's just as if you had written this:
-
-<ProgramListing>
- data T a = MkT (forall b. Either a b) (forall b. b -> b)
-</ProgramListing>
-
-That is, since the type variable <Literal>b</Literal> isn't in scope, it's
-implicitly universally quantified. (Arguably, it would be better
-to <Emphasis>require</Emphasis> explicit quantification on constructor arguments
-where that is what is wanted. Feedback welcomed.)
-</Para>
-
-</Sect2>
-
-<Sect2>
-<Title>Construction </Title>
-
-<Para>
-You construct values of types <Literal>T1, MonadT, Swizzle</Literal> by applying
-the constructor to suitable values, just as usual. For example,
-</Para>
-
-<Para>
-
-<ProgramListing>
-(T1 (\xy->x) 3) :: T Int
-
-(MkSwizzle sort) :: Swizzle
-(MkSwizzle reverse) :: Swizzle
-
-(let r x = Just x
- b m k = case m of
- Just y -> k y
- Nothing -> Nothing
- in
- MkMonad r b) :: MonadT Maybe
-</ProgramListing>
-
-</Para>
-
-<Para>
-The type of the argument can, as usual, be more general than the type
-required, as <Literal>(MkSwizzle reverse)</Literal> shows. (<Function>reverse</Function>
-does not need the <Literal>Ord</Literal> constraint.)
-</Para>
-
-</Sect2>
-
-<Sect2>
-<Title>Pattern matching</Title>
-
-<Para>
-When you use pattern matching, the bound variables may now have
-polymorphic types. For example:
-</Para>
-
-<Para>
-
-<ProgramListing>
- f :: T a -> a -> (a, Char)
- f (T1 f k) x = (f k x, f 'c' 'd')
-
- 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)
-</ProgramListing>
-
-</Para>
-
-<Para>
-In the function <Function>h</Function> we use the record selectors <Literal>return</Literal>
-and <Literal>bind</Literal> to extract the polymorphic bind and return functions
-from the <Literal>MonadT</Literal> data structure, rather than using pattern
-matching.
-</Para>
-
-<Para>
-You cannot pattern-match against an argument that is polymorphic.
-For example:
-
-<ProgramListing>
- newtype TIM s a = TIM (ST s (Maybe a))
-
- runTIM :: (forall s. TIM s a) -> Maybe a
- runTIM (TIM m) = runST m
-</ProgramListing>
-
-</Para>
-
-<Para>
-Here the pattern-match fails, because you can't pattern-match against
-an argument of type <Literal>(forall s. TIM s a)</Literal>. Instead you
-must bind the variable and pattern match in the right hand side:
-
-<ProgramListing>
- runTIM :: (forall s. TIM s a) -> Maybe a
- runTIM tm = case tm of { TIM m -> runST m }
-</ProgramListing>
-
-The <Literal>tm</Literal> on the right hand side is (invisibly) instantiated, like
-any polymorphic value at its occurrence site, and now you can pattern-match
-against it.
-</Para>
-
-</Sect2>
-
-<Sect2>
-<Title>The partial-application restriction</Title>
-
-<Para>
-There is really only one way in which data structures with polymorphic
-components might surprise you: you must not partially apply them.
-For example, this is illegal:
-</Para>
-
-<Para>
-
-<ProgramListing>
- map MkSwizzle [sort, reverse]
-</ProgramListing>
-
-</Para>
-
-<Para>
-The restriction is this: <Emphasis>every subexpression of the program must
-have a type that has no for-alls, except that in a function
-application (f e1…en) the partial applications are not subject to
-this rule</Emphasis>. The restriction makes type inference feasible.
-</Para>
-
-<Para>
-In the illegal example, the sub-expression <Literal>MkSwizzle</Literal> has the
-polymorphic type <Literal>(Ord b => [b] -> [b]) -> Swizzle</Literal> and is not
-a sub-expression of an enclosing application. On the other hand, this
-expression is OK:
-</Para>
-
-<Para>
-
-<ProgramListing>
- map (T1 (\a b -> a)) [1,2,3]
-</ProgramListing>
-
-</Para>
-
-<Para>
-even though it involves a partial application of <Function>T1</Function>, because
-the sub-expression <Literal>T1 (\a b -> a)</Literal> has type <Literal>Int -> T
-Int</Literal>.
-</Para>
-
-</Sect2>
-
-<Sect2 id="sigs">
-<Title>Type signatures
-</Title>
-
-<Para>
-Once you have data constructors with universally-quantified fields, or
-constants such as <Constant>runST</Constant> that have rank-2 types, it isn't long
-before you discover that you need more! Consider:
-</Para>
-
-<Para>
-
-<ProgramListing>
- mkTs f x y = [T1 f x, T1 f y]
-</ProgramListing>
-
-</Para>
-
-<Para>
-<Function>mkTs</Function> is a fuction that constructs some values of type
-<Literal>T</Literal>, using some pieces passed to it. The trouble is that since
-<Literal>f</Literal> is a function argument, Haskell assumes that it is
-monomorphic, so we'll get a type error when applying <Function>T1</Function> to
-it. This is a rather silly example, but the problem really bites in
-practice. Lots of people trip over the fact that you can't make
-"wrappers functions" for <Constant>runST</Constant> for exactly the same reason.
-In short, it is impossible to build abstractions around functions with
-rank-2 types.
-</Para>
-
-<Para>
-The solution is fairly clear. We provide the ability to give a rank-2
-type signature for <Emphasis>ordinary</Emphasis> functions (not only data
-constructors), thus:
-</Para>
-
-<Para>
-
-<ProgramListing>
- mkTs :: (forall b. b -> b -> b) -> a -> [T a]
- mkTs f x y = [T1 f x, T1 f y]
-</ProgramListing>
-
-</Para>
-
-<Para>
-This type signature tells the compiler to attribute <Literal>f</Literal> with
-the polymorphic type <Literal>(forall b. b -> b -> b)</Literal> when type
-checking the body of <Function>mkTs</Function>, so now the application of
-<Function>T1</Function> is fine.
-</Para>
-
-<Para>
-There are two restrictions:
-</Para>
-
-<Para>
-
-<ItemizedList>
-<ListItem>
-
-<Para>
- You can only define a rank 2 type, specified by the following
-grammar:
-
-
-<ProgramListing>
-rank2type ::= [forall tyvars .] [context =>] funty
-funty ::= ([forall tyvars .] [context =>] ty) -> funty
- | ty
-ty ::= ...current Haskell monotype syntax...
-</ProgramListing>
-
-
-Informally, the universal quantification must all be right at the beginning,
-or at the top level of a function argument.
-
-</Para>
-</ListItem>
-<ListItem>
-
-<Para>
- There is a restriction on the definition of a function whose
-type signature is a rank-2 type: the polymorphic arguments must be
-matched on the left hand side of the "<Literal>=</Literal>" sign. You can't
-define <Function>mkTs</Function> like this:
-
-
-<ProgramListing>
-mkTs :: (forall b. b -> b -> b) -> a -> [T a]
-mkTs = \ f x y -> [T1 f x, T1 f y]
-</ProgramListing>
-
-
-
-The same partial-application rule applies to ordinary functions with
-rank-2 types as applied to data constructors.
-
-</Para>
-</ListItem>
-
-</ItemizedList>
-
-</Para>
-
-</Sect2>
-
-
-<Sect2 id="hoist">
-<Title>Type synonyms and hoisting
-</Title>
-
-<Para>
-GHC also allows you to write a <Literal>forall</Literal> in a type synonym, thus:
-<ProgramListing>
- type Discard a = forall b. a -> b -> a
-
- f :: Discard a
- f x y = x
-</ProgramListing>
-However, it is often convenient to use these sort of synonyms at the right hand
-end of an arrow, thus:
-<ProgramListing>
- type Discard a = forall b. a -> b -> a
-
- g :: Int -> Discard Int
- g x y z = x+y
-</ProgramListing>
-Simply expanding the type synonym would give
-<ProgramListing>
- g :: Int -> (forall b. Int -> b -> Int)
-</ProgramListing>
-but GHC "hoists" the <Literal>forall</Literal> to give the isomorphic type
-<ProgramListing>
- g :: forall b. Int -> Int -> b -> Int
-</ProgramListing>
-In general, the rule is this: <Emphasis>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:</Emphasis>
-<ProgramListing>
- <Emphasis>type1</Emphasis> -> forall a. <Emphasis>type2</Emphasis>
-==>
- forall a. <Emphasis>type1</Emphasis> -> <Emphasis>type2</Emphasis>
-</ProgramListing>
-(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 <Literal>forall</Literal> comes from a synonym. For example, here is another
-valid way to write <Literal>g</Literal>'s type signature:
-<ProgramListing>
- g :: Int -> Int -> forall b. b -> Int
-</ProgramListing>
-</Para>
-</Sect2>
-
-</Sect1>
-
-<Sect1 id="existential-quantification">
-<Title>Existentially quantified data constructors
-</Title>
-
-<Para>
-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 <Command>hbc</Command> Haskell compiler for several years, and
-proved very useful. Here's the idea. Consider the declaration:
-</Para>
-
-<Para>
-
-<ProgramListing>
- data Foo = forall a. MkFoo a (a -> Bool)
- | Nil
-</ProgramListing>
-
-</Para>
-
-<Para>
-The data type <Literal>Foo</Literal> has two constructors with types:
-</Para>
-
-<Para>
-
-<ProgramListing>
- MkFoo :: forall a. a -> (a -> Bool) -> Foo
- Nil :: Foo
-</ProgramListing>
-
-</Para>
-
-<Para>
-Notice that the type variable <Literal>a</Literal> in the type of <Function>MkFoo</Function>
-does not appear in the data type itself, which is plain <Literal>Foo</Literal>.
-For example, the following expression is fine:
-</Para>
-
-<Para>
-
-<ProgramListing>
- [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
-</ProgramListing>
-
-</Para>
-
-<Para>
-Here, <Literal>(MkFoo 3 even)</Literal> packages an integer with a function
-<Function>even</Function> that maps an integer to <Literal>Bool</Literal>; and <Function>MkFoo 'c'
-isUpper</Function> packages a character with a compatible function. These
-two things are each of type <Literal>Foo</Literal> and can be put in a list.
-</Para>
-
-<Para>
-What can we do with a value of type <Literal>Foo</Literal>?. In particular,
-what happens when we pattern-match on <Function>MkFoo</Function>?
-</Para>
-
-<Para>
-
-<ProgramListing>
- f (MkFoo val fn) = ???
-</ProgramListing>
-
-</Para>
-
-<Para>
-Since all we know about <Literal>val</Literal> and <Function>fn</Function> is that they
-are compatible, the only (useful) thing we can do with them is to
-apply <Function>fn</Function> to <Literal>val</Literal> to get a boolean. For example:
-</Para>
-
-<Para>
-
-<ProgramListing>
- f :: Foo -> Bool
- f (MkFoo val fn) = fn val
-</ProgramListing>
-
-</Para>
-
-<Para>
-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.
-</Para>
-
-<Sect2 id="existential">
-<Title>Why existential?
-</Title>
-
-<Para>
-What has this to do with <Emphasis>existential</Emphasis> quantification?
-Simply that <Function>MkFoo</Function> has the (nearly) isomorphic type
-</Para>
-
-<Para>
-
-<ProgramListing>
- MkFoo :: (exists a . (a, a -> Bool)) -> Foo
-</ProgramListing>
-
-</Para>
-
-<Para>
-But Haskell programmers can safely think of the ordinary
-<Emphasis>universally</Emphasis> quantified type given above, thereby avoiding
-adding a new existential quantification construct.
-</Para>
-
-</Sect2>
-
-<Sect2>
-<Title>Type classes</Title>
-
-<Para>
-An easy extension (implemented in <Command>hbc</Command>) is to allow
-arbitrary contexts before the constructor. For example:
-</Para>
-
-<Para>
-
-<ProgramListing>
-data Baz = forall a. Eq a => Baz1 a a
- | forall b. Show b => Baz2 b (b -> b)
-</ProgramListing>
-
-</Para>
-
-<Para>
-The two constructors have the types you'd expect:
-</Para>
-
-<Para>
-
-<ProgramListing>
-Baz1 :: forall a. Eq a => a -> a -> Baz
-Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
-</ProgramListing>
-
-</Para>
-
-<Para>
-But when pattern matching on <Function>Baz1</Function> the matched values can be compared
-for equality, and when pattern matching on <Function>Baz2</Function> the first matched
-value can be converted to a string (as well as applying the function to it).
-So this program is legal:
-</Para>
-
-<Para>
-
-<ProgramListing>
- f :: Baz -> String
- f (Baz1 p q) | p == q = "Yes"
- | otherwise = "No"
- f (Baz1 v fn) = show (fn v)
-</ProgramListing>
-
-</Para>
-
-<Para>
-Operationally, in a dictionary-passing implementation, the
-constructors <Function>Baz1</Function> and <Function>Baz2</Function> must store the
-dictionaries for <Literal>Eq</Literal> and <Literal>Show</Literal> respectively, and
-extract it on pattern matching.
-</Para>
-
-<Para>
-Notice the way that the syntax fits smoothly with that used for
-universal quantification earlier.
-</Para>
-
-</Sect2>
-
-<Sect2>
-<Title>Restrictions</Title>
-
-<Para>
-There are several restrictions on the ways in which existentially-quantified
-constructors can be use.
-</Para>
-
-<Para>
-
-<ItemizedList>
-<ListItem>
-
-<Para>
- 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:
-
-
-<ProgramListing>
-f1 (MkFoo a f) = a
-</ProgramListing>
-
-
-Here, the type bound by <Function>MkFoo</Function> "escapes", because <Literal>a</Literal>
-is the result of <Function>f1</Function>. One way to see why this is wrong is to
-ask what type <Function>f1</Function> has:
-
-
-<ProgramListing>
- f1 :: Foo -> a -- Weird!
-</ProgramListing>
-
-
-What is this "<Literal>a</Literal>" in the result type? Clearly we don't mean
-this:
-
-
-<ProgramListing>
- f1 :: forall a. Foo -> a -- Wrong!
-</ProgramListing>
-
-
-The original program is just plain wrong. Here's another sort of error
-
-
-<ProgramListing>
- f2 (Baz1 a b) (Baz1 p q) = a==q
-</ProgramListing>
-
-
-It's ok to say <Literal>a==b</Literal> or <Literal>p==q</Literal>, but
-<Literal>a==q</Literal> is wrong because it equates the two distinct types arising
-from the two <Function>Baz1</Function> constructors.
-
-
-</Para>
-</ListItem>
-<ListItem>
-
-<Para>
-You can't pattern-match on an existentially quantified
-constructor in a <Literal>let</Literal> or <Literal>where</Literal> group of
-bindings. So this is illegal:
-
-
-<ProgramListing>
- f3 x = a==b where { Baz1 a b = x }
-</ProgramListing>
-
-
-You can only pattern-match
-on an existentially-quantified constructor in a <Literal>case</Literal> 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.
-
-</Para>
-</ListItem>
-<ListItem>
-
-<Para>
-You can't use existential quantification for <Literal>newtype</Literal>
-declarations. So this is illegal:
-
-
-<ProgramListing>
- newtype T = forall a. Ord a => MkT a
-</ProgramListing>
-
-
-Reason: a value of type <Literal>T</Literal> must be represented as a pair
-of a dictionary for <Literal>Ord t</Literal> and a value of type <Literal>t</Literal>.
-That contradicts the idea that <Literal>newtype</Literal> should have no
-concrete representation. You can get just the same efficiency and effect
-by using <Literal>data</Literal> instead of <Literal>newtype</Literal>. If there is no
-overloading involved, then there is more of a case for allowing
-an existentially-quantified <Literal>newtype</Literal>, because the <Literal>data</Literal>
-because the <Literal>data</Literal> version does carry an implementation cost,
-but single-field existentially quantified constructors aren't much
-use. So the simple restriction (no existential stuff on <Literal>newtype</Literal>)
-stands, unless there are convincing reasons to change it.
-
-
-</Para>
-</ListItem>
-<ListItem>
-
-<Para>
- You can't use <Literal>deriving</Literal> to define instances of a
-data type with existentially quantified data constructors.
-
-Reason: in most cases it would not make sense. For example:#
-
-<ProgramListing>
-data T = forall a. MkT [a] deriving( Eq )
-</ProgramListing>
-
-To derive <Literal>Eq</Literal> in the standard way we would need to have equality
-between the single component of two <Function>MkT</Function> constructors:
-
-<ProgramListing>
-instance Eq T where
- (MkT a) == (MkT b) = ???
-</ProgramListing>
-
-But <VarName>a</VarName> and <VarName>b</VarName> 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!
-</Para>
-</ListItem>