Jan Brosius writes:
> Is there anyone who can explain to me what is meant by second rank
> polymorphism.
The system of second-order lambda calculus, or System F, is the system
you are looking for. It features rank-2 polymorphism in the sense that
a polymorphic function may be used at a polymorphic type.
In other words, consider the identity function `id' (using a
not-quite-Haskell notation):
id :: forall (a :: T) . a -> a
id = /\ a :: T . \ x :: a . x
Here you can see that the function `id' has a polymorphic type: for any
type `a', it has the type `a->a'. The definition reflects this: the
`/\ a' is a type lambda -- the first argument of `id' is a type. Given
a type a, it then takes a term x of type a, and returns it. Thus a
valid application of id is as follows:
id Int 5 ==> 5
because
(/\a::T.\x::a.x) Int 5 --> (\x::Int.x) 5 --> 5
Now in ordinary Haskell (or ML), you don't see the type lambdas /\, or
the foralls. These are inferred automatically for you. However, they
are inferred in such a way that they all appear at the very beginning
of the types and terms respectively. There are good technical reasons
for this. One consequence is that a function like `id' will never need
to be applied at a polymorphic type; that is,
id (forall (a::T).a->a) id ==/==> id
but is in fact untypeable. This is OK because you must have been going
to use the result, and so in reality you have something like
id (Int->Int) (id Int) 5 ==> 5
as expected.
So a rank-1 polymorphic type system, or predicative polymorphism,
restricts `T' above to only monomorphic (non-polymorphic) types.
Rank-2 polymorphism relaxes this restriction. Now T is closed under
forall as well as under (->) and so on, and so polymorphic types may
appear as arguments. This also means, necessarily, that foralls may
appear anywhere in types, not just at the beginning. For example, in
System F,
id (forall (a::T).a->a)
has type
(forall (a::T).a->a) -> (forall (b::T).b->b)
Normally the `::T' is dropped, and `forall a::T' is simply written
`forall a'. Sometimes `*', aka `the kind of all types', is used:
`forall a::*'.
In the literature, an actual `forall' symbol, an upside-down A like
`\/', is usually used instead of `forall'.
References:
There's a discussion in Chapter 9 of:
@Book{
Mitchell96:Foundations,
author="John C. Mitchell",
title="Foundations for Programming Languages",
publisher="{MIT} {P}ress",
year="1996",
}
And also in any introduction to type systems or the typed lambda
calculus, such as the lecture notes originally by Andy Pitts at
http://www.cl.cam.ac.uk/Teaching/1998/Types/
The second-order lambda calculus was independently invented by
Jean-Yves Girard (c.1971) and John Reynolds (c.1974). I don't have the
references to hand.
Hope this helps!
> I have already read all available online documentation.
> In logic one has: forall x forall y = forall y forall x.
This is not the case in the second-order lambda calculus, because the
order of the type lambdas is clearly significant:
(.) :: \/a. \/b. \/c. (a->b) -> (b->c) -> (a->c)
is clearly different from
(.') :: \/c \/b. \/a. (a->b) -> (b->c) -> (a->c)
although the two are in some sense equivalent.
> Doesn't haskell 98 allow in place updating e.g; for records?
[see next message]
> Thanks
You're welcome!
> Jan
--KW 8-)
--
: Keith Wansbrough, MSc, BSc(Hons) (Auckland) ------------------------:
: PhD Student, Computer Laboratory, University of Cambridge, England. :
: (and recently of the University of Glasgow, Scotland. [><] ) :
: Native of Antipodean Auckland, New Zealand: 174d47' E, 36d55' S. :
: http://www.cl.cam.ac.uk/users/kw217/ mailto:[EMAIL PROTECTED] :
:---------------------------------------------------------------------:
