O'Reilly logo

Practical Foundations for Programming Languages by Robert Harper

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

20 Girard’s System F

The languages we have considered so far are all monomorphic in that every expression has a unique type, given the types of its free variables, if it has a type at all. Yet it is often the case that essentially the same behavior is required, albeit at several different types. For example, in images{nat →} there is a distinct identity function for each type τ, namely λ (x : τ ) x, even though the behavior is the same for each choice of τ. Similarly, there is a distinct composition operator for each triple of types, namely

images

Each choice ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required