## System FAn introduction by Franck Binard |

While System F may be hard to understand at first, and while I've been told that there are other systems even more powerful out there, this one blows me away.

Maybe I'm being naive, but if you know and love the lambda calculus for being
willing to accept terms such as: *(λx.xx)*, you have to be a bit
disappointed when you find out that this ability is lost in the simply-typed version. (λx.xx) can't be typed!!

It is not possible to encode parametric polymorphic functions in the simple type system.
All that beautiful potential for abstraction is just gone. If *x* is of type
* [Something]*, any type that goes to the left of

Anyhow, remember how it was possible to say in a godlike manner: "λxy.x", that to my world will be true. And false. I'll call that "λxy.y". And because I feel like it , false will also be zero. And I'm so powerful that 2 will be λxy.xxy. And it will all work out. Ha Ha Ha. (godlike laughter)

Of course the simply-typed version does have its good sides. For one, it is isomorphic
to first-order logic. So if you have socrates of type human (lets write that *s*:**[H]**), and a function
*loudMouth*, the type of which takes a human and returns a comment (let's write *loudMouth*:**[H→C]**),
then applying *loudMouth* to s magically creates a first year philosophy class.

System F gets you the best of both worlds. Types and Curry mixed in with a whole lot of extra abstractions. System F, I mean second-order polymorphically typed-calculus is an extension of the simply-typed calculus. It provides a basis for polymorphic programming languages. It was independently invented by Girard and Reynolds over 20 years ago.

In this text, I will use two kind of notation (and indicate which I'm using in the title of the section).When casual, I will
write types bold, capitalized and enclosed in square brackets, like so: **[Toy]**. An object is written in italics.
So the expression *ball*:**[Toy]** refers to an object ball of type Toy.

When using formal math, I will use the standard notation found in Girard's Proofs and Types book.

Girard's System F adds the use of *type variables* to the simply-typed lambda-calculus. Type
variables are then used to define more complex types (Bool, Int, List) by
induction. These are the schemes for type formation:

- If U and V are types then U→V is a type
- If V is a type and X is a type variable then is a type

The rules for term formation are expanded to take into account the addition
of type variables: There are 5 schemes for forming *terms*:

*Variables:*

x^{T},y^{T},z^{T},are*variables*of type T*Application:*

tu is a term of type V where and t:U→V and u:U*λ-abstraction:*

is a term of type U→V where v:V*Universal abstraction:*

is a term of type where X is a type variable*Universal application:*

and U is a type then is a term of type V[U/X]

All the usual conversion rules apply from the simply-typed lambda-calculus apply. With the following added:

Next: Free structures and models

Franck J.L. Binard

School of Information Technology and Engineering (SITE)

University of Ottawa

800 King Edward Ave.

Ottawa, Ontario, Canada, K1N 6N5

Tel: (613) 562-5800 x6727, Fax: (613) 562-5664

Office: 4-035 SITE

Email: fbinard@site.uottawa.ca

Contactez: L'cole d'ingnierie et de technologie de l'information

Contact: School of Information Technology and Engineering

Copyright 2001 Universit d'Ottawa / University of Ottawa

Webmestre / Webmaster