l'ITI Recherche Nouvelles HREF= Rpertoires Ressources Gnie/Engineering Ud'O/UofO SITE Search News Directories Resources SITE

System F

An 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 x has to have type [SomethingAnything] . And that's something else than [Something] right?

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.

As it turns out, in logic, if you have a proposition H→C and another proposition H, then you can deduce C. It's what you call modus ponens when you want to impress someone with your latin.

System F

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.

Some conventions

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.

Rules for Types (formal notation)

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:

Rules for Terms (formal notation)

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

Reduction(formal notation)

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