Keith Wansbrough writes:
>
> 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.
>
Now I have some difficulty to follow. If I write
id :: a -> a
then I thought it meant " id is a "function" from type a to type a " ; in
logic this is completely equivalent with (since a is a variable ):
" forall a ( id is a function from type a to type a) "
But then I immediately get a problem, indeed since id is a function from set
a into set a then I have
id is a subset from set aXa (the product of a with a)
Choose a set b such that "a intersection b = empty" then
id is subset of aXa and subset of bXb
which is a contradiction. So id is not a function but one can define it as
id = \x -> x that is an untypable lambda-function.
A way out of it is to write id(a) :: a -> a ; then I can really say that
forall a ( id(a) is a function from type (or set) a into (or to) type a).
And forall x forall a (id(a) x = x) which is completely equivalent with
forall x forall a (id(a) x = x).
I am very confident that you cannot go around the rule:
forall a forall b ( T(a,b)) equivalent with forall b forall a (T(a,b)).
So I think, before I can proceed any further in learning I invite you to
phrase exactly what one means with
id :: a -> a ?
> 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.
>
>
What do you mean by " in some sense equivalent and yet clearly different" ?
> > Doesn't haskell 98 allow in place updating e.g; for records?
>
> [see next message]
>
I have read this message and now I have the following question:
Does this mean that a compiled program written in a strict functional
language will be faster than the "same" program compiled with thelazy
functional language Haskell 98
Thanks
>
> You're welcome!
>
Thanks again
Jan
> > 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] :
> :---------------------------------------------------------------------:
>
>
>
