A Short Introduction to Systems F and F
ω
Pablo Nogueira
22nd February 2006
Contents
1 Introduction 2
2 Preliminaries 2
3 Pure Simply Typed Lambda Calculus 3
4 Adding primitive types and values. 6
5 Adding parametric polymorphism: System F 8
6 Adding type operators: System F
ω
9
7 Adding general recursion 12
Bibliography 15
1
1 Introduction
These notes contain a short introduction to the syntactic, context-dependent, and operational
aspects of System F and System F
ω
. The former extends the Simply (and explicitly) Typed
Lambda Calculus with (universal) parametric polymorphism. The latter extends it with type
operators. The following references contain detailed presentations of the systems and of typed
lambda calculi in general: [Car97, CW85, Pie02, Mit96].
2 Preliminaries
What is the Lambda Calculus? We can describe the Lambda Calculus [Chu41, Mit96, Bar84]
as a tiny programming language of unnamed, first-class functions. It was originally conceived
as a formal (i.e., symbolic) language of untyped functions that was part of a proof system of
functional equality. The logical part of the system was proved inconsistent but the language of
functions was deem useful and gave rise to different families of languages that model different
aspects of computation. Typed extensions with polymorphism, recursion, built-in primitives, plus
naming and definitional facilities at value and type level make up the core languages of functional
languages [Lan66, Pie02, Rea89]. Improvements to the core language’s operational aspects form
the basis of functional language implementations.
Object and meta language. We assume familiarity with the distinction between object lan-
guage , a particular formal language under study, and meta-language , the notation used when
talking about the object language.
Definitions and equality. It is common practice in mathematics to use equality as a definitional
device. Since equality is also used as a relation on already defined entities, we distinguish equality
from definitional equality and use the symbol
def
= for the latter. A definition induces an equality
in the sense that if X
def
= Y then X = Y ; the converse need not be true.
Format of typing rules. Type rules are written inductively in natural deduction style:
antecedent1 . . . antecedentn
consequent
1
. . . consequent
n
where n ≥ 0. Rules can be read forwards (when all antecedents are the case then all the consequents
are the case) or backwards (all the consequents are the case if all the antecedents are the case).
Variables appearing in antecedents and consequents are assumed universally quantified unless
indicated otherwise.
Grammatical conventions. We use EBNF notation to define syntax. Non-terminals are writ-
ten in capitalised slanted. Any other symbol stands for a terminal with the exception of the
postfix meta-operators ?, +, and ∗. Their meaning is as follows: X?, X∗, and X+ denote, respect-
ively, zero or one X, zero or more X, and one or more X, where X can be a terminal or non-terminal.
2
Parentheses are also used as meta-notation for grouping, e.g., (X Y)∗.
The following EBNF example is a snippet of C++’s grammar [Str92]:
CondOp ::= if Cond Block (else Block)?
Cond ::= ( Expression )
Block ::= Stmt | { Stmt+ }
In the first production parentheses are meta-notation. In the second they are object-level symbols,
for they are not followed by a postfix meta-operator.
Quantification. We follow the widely used and well-known “quantifier-dot” convention when
denoting quantification. For example, in ∀x.P the scope of bound variable x starts from the dot
to the end of the expression P . Also,
∀x ∈ S. P abbreviates ∀x. x ∈ S ⇒ P
3 Pure Simply Typed Lambda Calculus
Type ::= ∗ −− base type
| Type → Type −− function type
| (Type) −− grouping
Term ::= TermVar −− term variable
| Term Term −− term application
| λ TermVar : Type . Term −− term abstraction
| (Term) −− grouping
Γ(x) = τ
Γ ` x : τ
Γ ` t1 : σ → τ Γ ` t2 : σ
Γ ` (t1 t2) : τ
Γ, x : σ ` t : τ
Γ ` (λx :σ . t) : σ → τ
(λx :τ . t) t′ B t[t′/x]
β
t1 B t
′
1
t1 t2 B t
′
1
t2
li1
t2 B t
′
2
x t2 B x t
′
2
li2
t B t
ref
t1 B t2 t2 B t3
t1 B t3
trs
Figure 1: The Pure Simply Typed Lambda Calculus.
Figure 1 shows the syntax, type rules, and operational semantics of the Pure Simply Typed
Lambda Calculus (PSTLC). There are terms carrying type annotations and for that reason it is
dubbed ‘explicitly typed’—or á la Church, who first proposed it [HS86]. The following paragraphs
elaborate.
Terms and types. The PSTLC has a language of types (non terminal Type) for expressing
the types of functions inductively from a unique base or ground type ∗, and a language of terms
3
(non-terminal Term) which consists of variables, lambda abstractions (unnamed functions), and
applications of terms to other terms.1 Variables stand for formal parameters or yet-to-be-defined
primitive values when not bound by any λ. In a lambda abstraction λx :τ.t, the λ symbol indicates
that x is a bound variable—i.e., a formal parameter—, τ is the type of x, and t abbreviates an
expression where x may occur free. Table 2 contains the list of meta-variable conventions followed
throughout these notes.
σ, τ , . . . range over types.
x, y, . . . range over term variables.
t, t′, . . . range over terms.
Γ ranges over type-assignments.
α, β, . . . range over type variables (Section 5).
κ, ν range over kinds (Section 5).
Figure 2: Meta-variable conventions for Lambda Calculi.
Types and terms are separated with the only exception that types can appear as annotations in
lambda abstractions. The type of a function is also called its type signature . It describes the
function’s arity, order, and the type of its arguments. The arity is the number of arguments it
takes. The order is determined from its type signature as follows:
order(∗)
def
= 0
order(σ → τ)
def
= max ( 1 + order(σ), order(τ) )
Let τ be the type of a lambda abstraction and suppose order(τ) = n. If n = 1 then the lambda
abstraction may either return a manifest (non-function) value of type ∗ or another lambda ab-
straction of order 1 as result. If n > 1, then it is a higher-order abstraction that either takes or
returns a lambda abstraction of order n.
It is typical to blur the conceptual distinction between manifest values and function values by
considering the former as nullary functions and the latter as proper functions .2
The fixity of a function is an independent concept. It determines the syntactical denotation of the
application of the function to its arguments. In some functional languages, functions can be infix,
prefix, postfix, mixfix, and have their precedence and associativity defined by programmers. In the
PSTLC, lambda abstractions are prefix, application associates to the left—for example, t1 t2 t3
is parsed as (t1 t2) t3—and consequently arrows in type signatures associate to the right—for
example, ∗ → ∗ → ∗ is parsed as ∗ → (∗ → ∗).
Multiple-argument functions are represented as curried higher-order functions that take one
argument but return another function as result. For example, the term:
λx :∗ . λy :∗ → ∗ . y x
is a higher-order function that takes a manifest value x and returns a function that takes a function
1That application is denoted by whitespace is not quite deducible from the grammar alone. In order for the two
terms to be distinguished there must be some separator token between them which is assumed to be whitespace.
2In the PSTLC not every term is a function: there is a ground type. In the untyped lambda calculus, every
term is a function.
4
y as argument and applies it to x.
Related terminology. An operator is a term whose value is a function (a precise definition
of ‘value’ is given on page 5). An operand is a term that plays the role of a parameter or argu-
ment . A formal parameter or argument appears in a definition whereas an actual parameter
or argument appears in an application. A call site is another name for an application of an
operator to an operand.
In common parlance, the word ‘type’ is not only used in reference to type-terms but also in
reference to data types , i.e., a concrete realisation of the type in an implementation design or
actual code.
Type rules. The type rules listed in Figure 1 can be employed to check the type of a term
compositionally from the type of its subterms. The type of a term depends on the type of its
free variables. This context-dependent information is captured by a type-assignment function
Γ : TypeVar → Type which acts as a symbol table of sorts that stores the types of free variables
in scope. The operation Γ, x : τ denotes the construction of a new type-assignment and has the
following definition:
(Γ, x : τ)(y)
def
= if x = y then τ else Γ(y)
The type rules are rather intuitive. Notice only that Γ is enlarged in the last rule because x may
occur free in t.
Operational semantics. The call-by-name operational semantics is shown in the last box of
Figure 1. A reduction relation B is defined between terms. Briefly, Rule β captures the reduction
of an application of a lambda abstraction to an argument. The free occurrences of the parameter
variable are substituted (avoiding variable capture) by the argument in the lambda abstraction’s
body. This is what the operation t[t′/x] means, which reads “t where t′ is substituted for free
x” [Bar84]. Rule li1 specifies that an application t1 t2 can be reduced to the term t
′
1
t2 when t1 can
be reduced to t′
1
. Rule li2 specifies that reduction must proceed to the argument of an application
when the term being applied is a free variable. Together, these rules specify a leftmost-outermost
reduction order. Rules ref and trs specify that B is a reflexive and transitive relation.
A value is a program term of central importance. Operationally, the set of values V is a subset
of the set of normal forms N , which is in turn a subset of the set of terms T , that is, V ⊆ N ⊆ T .
These sets are to be fixed by definition. A term is in normal form if no reduction rule, other than
reflexivity, is applicable to it. In the PSTLC, all normal forms are values and they are defined by
the following grammar:
NF ::= TermVar | λ TermVar : Type . Term
That is: variables and lambda abstractions are normal forms, which means that function bodies
are evaluated only after the function is applied to an argument. This is reflected in the operational
5
semantics by the deliberate omission of the following rule:
t B t′
λx :τ . t B λx :τ . t′
It can be the case in other languages that there are normal forms that are not values. Examples
are stuck terms which denote run-time errors.
Example. The following derivation proves a reduction:
(λx :∗ → ∗ . x) (λx :∗ . x) B (λx :∗ . x)
β
(λx :∗ → ∗ . x) (λx :∗ . x) y B (λx :∗ . x) y
li1
(λx :∗ . x) y B y
β
(λx :∗ → ∗ . x) (λx :∗ . x) y B y
trs
The following is an example reduction of a well-typed PSTLC term to its normal form. The
subterm being reduced at each reduction step is shown underlined.
(λy :∗ → ∗ . y z) ((λy :∗ → ∗ . y) (λx :∗ . x))
B ((λy :∗ → ∗ . y) (λx :∗ . x)) z
B (λx :∗ . x) z
B z
4 Adding primitive types and values.
The PSTLC is impractical as a programming language. Given a term t, its free variables have
no meanings. The PSTLC extended with various primitives has been given specific names. In
particular, the language PCF (Programming Computable Functions) is a PSTLC extended with
natural numbers, booleans, cartesian products, and fixed points [Sto77, Mit96].
In Figure 3 we extend the grammar of terms and types of Figure 1 to include some primitive types.
The base type ∗ is now removed from the language of types. Of particular interest are cartesian
product and disjoint sum types that endow the Extended STLC (referred to as STLC from now
on) with algebraic types roughly similar to those supported by functional languages.
We only show a tiny sample of type and reduction rules for primitives, the latter called δ-rules
in the jargon, to illustrate how the extension goes. Primitive types are all manifest and therefore
their order is 0.
6
Type ::= Nat −− naturals
| Bool −− booleans
| Type × Type −− products
| Type + Type −− disjoint sums
| 1 −− unit type
Term ::= Num −− natural literals
| true −− boolean literals
| false
| + | − | … −− arithmetic functions
| not Term −− boolean functions
| if Term then Term else Term
| …
| (Term , Term) −− pairs
| fst Term
| snd Term
| Inl Term −− sums
| Inr Term
| case Term of Inl TermVar then Term ; Inr TermVar then Term
| unit −− unit value
Γ ` true : Bool Γ ` unit : 1
Γ ` t : Bool Γ ` t1 : τ Γ ` t2 : τ
Γ ` (if t then t1 else t2) : τ
(if true then t1 else t2) B t1 (if false then t1 else t2) B t2
t B t′
(if t then t1 else t2) B (if t
′ then t1 else t2)
Figure 3: The (Extended) Simply Typed Lambda Calculus. The base type ∗ is removed from the
language of types and new productions are added for terms and type-terms to those in Figure 1.
Only a small sample of type and reduction rules are shown.
7
Example. The following is an example reduction of a well-typed STLC term:
(λx :Nat . if x > 0 then 1 else x + 1) ((λy :Nat . y + y) 4)
B if ((λy :Nat . y + y) 4) > 0 then 1 else ((λy :Nat . y + y) 4) + 1
B if (4 + 4) > 0 then 1 else ((λy :Nat . y + y) 4) + 1
B if 8 > 0 then 1 else ((λy :Nat . y + y) 4) + 1
B if true then 1 else ((λy :Nat . y + y) 4) + 1
B 1
5 Adding parametric polymorphism: System F
The STLC is not polymorphic. For example, the identity function for booleans and naturals is
expressed by two syntactically different lambda abstractions:
(λx :Nat . x) : Nat → Nat
(λx :Bool . x) : Bool → Bool
However, they only differ in type annotations. System F [Gir72, Rey74] extends the STLC
with universal parametric polymorphism. It adds new forms of abstraction and application where
types appear as terms, not just annotations. The new syntax can be motivated using the above
identity functions. A parametrically polymorphic identity is obtained by abstracting over types
(universal abstraction), e.g.:
Λα :∗ . λx :α . x
This term has type:
∀α :∗ . α → α
(We explain the role of ∗ in a moment.) A capitalised lambda ‘Λ’ is introduced to distinguish
universal abstraction over types from term abstraction. Dually, there is universal application ,
e.g.:
(Λα :∗ . λx :α . x) Nat B (λx :Nat . x)
A universal application is evaluated by substituting the type-term argument for the free occur-
rences of the bound type-variable in the body of the universal abstraction. Here is another example;
notice that type-variable β appears in a type-application:
(Λβ :∗ . (Λα :∗ . λx :α . x) β) Nat B (Λα :∗ . λx :α . x) Nat
Figure 4 shows the additions to the grammar, to the type rules, and to the operational semantics.
Because of the introduction of type variables, rules for type-term well-formedness are provided (a
few are shown in the first row of the second box).
We reintroduce ∗ at a new level and call it a base or ground kind . Kinds classify types and are
explained in detail in Section 6; for the moment, type variables in universal abstractions always
8
Kind ::= ∗
Type ::= TypeVar
| ∀ TypeVar : Kind . Type → Type
Term ::= Λ TypeVar : Kind . Term −− universal abstraction
| Term Type −− universal application
Γ(α) = κ
Γ ` α : κ
Γ ` σ Γ ` τ
Γ ` σ → τ
Γ, α : κ ` σ
Γ ` ∀α :κ . σ
. . .
Γ, α : κ ` t : τ
Γ ` (Λα :κ . t) : (∀α :κ . τ)
Γ ` t : (∀α :κ . τ) Γ ` σ
Γ ` t σ : τ [σ/α]
(Λα :κ . t) σ B t[σ/α]
Figure 4: System F extensions.
have kind ∗, for they can only be substituted for base types which are all manifest, but we use
in advance the kind meta-variable κ because the language of kinds is extended in Section 6.
Type-assignments now also store the kinds of type variables.
The type rules for universal abstraction and application are shown in the second row of the second
box. Notice that a type-level, capture-avoiding substitution operation is assumed which replaces
type variables for types in terms. The last box in Figure 4 enlarges the reduction relation to
account for universal applications. Universal abstractions are normal forms like regular term
abstractions.
6 Adding type operators: System Fω
System F
ω
extends System F with type operators , i.e., functions at the type level. They are
also called type constructors , but we prefer to use ‘constructor’ at the value level when referring
to the terms associated with type operators, called value constructors . An example of type
operator is List which when applied to a manifest type τ returns the type of lists of type τ . Its
associated value constructors are:
Nil :: ∀ a:∗. List a
Cons :: ∀ a:∗. a → List a → List a
which are names for primitive constants without δ-rules—e.g., a term like Cons t Nil is in normal
form, whatever the t. Manifest types such as Nat or Bool are ‘values’ at the type level. A fully
applied (i.e., closed) type operator also constitutes a manifest type, e.g.: List Nat. Occasionally,
9
we blur the distinction between manifest types and type operators by considering the former as
nullary type operators and the latter as proper type operators .
To model type-level functions, the PSTLC of Figure 1 is lifted to the type level as shown in the first
box of Figure 5, so that terms such as α, λα :κ . τ , and τ σ (that is, type variables , type-level
abstractions , and type-level applications) are defined as legal type-terms.
The kind of a type-term is somewhat inaccurately described as the ‘type’ of a type-term. But
kinds only describe the arity and order of type operators. The kind of a nullary type operator (a
manifest type) is ∗. The kind of a proper type operator is denoted as κ → ν, where κ is the kind
of its argument and ν the kind of its result. The order of a type operator is determined from its
kind signature as follows:
order(∗)
def
= 0
order(κ → ν)
def
= max ( 1 + order(κ), order(ν) )
Kinds do not have a status as the ‘types’ of types when there are orthogonal features in the type
language, like type classes [Blo91, WB89, Jon92], which render them inaccurate as such. For
instance, the following two Haskell definitions of the type operator List have the same kind, but
the second is constrained on the range of type arguments:
data List a = Nil | Cons a (List a)
data Ord a ⇒ List a = Nil | Cons a (List a)
Type checkers kind-check applications of type operators to arguments to make sure the latter
have the right expected kind. Kind-checking rules are shown in the second box of Figure 5. The
first three lines establish the kinds of manifest types and also depict the kind-checking rules for
primitive type operators such as + and ×, etc. The last line contains the type rules of the PSTLC
but lifted as kind rules (compare with Figure 1).
The third box in Figure 5 shows a type-level reduction relation I between type-terms that is
reflexive, transitive, and compatible with all ways of constructing type-terms. The symbol P
stands for a primitive type, i.e., Bool, Nat, or 1. The reduction relation is static: type-level
applications are reduced by the type-checker at compile time. (This relation is a simple example
of type-level computation.)
The last box in Figure 5 defines a relation of structural type equivalence which specifies that
two type-terms are equal when their structure is equal. The relation is reflexive, symmetric,
transitive, and compatible with all ways of constructing types.
Normal forms of type-terms are type variables, primitive types, type-level abstractions, and type-
terms of the form τ1 × τ2, ∀α :κ . τ1, τ1 + τ2, and τ1 → τ2, when τ1 and τ2 are themselves in normal
form.
Notice that there are three sorts of substitutions, all using the same notation. There are two
at the term level (term variables replaced for terms in term abstractions and type variables for
type-terms in universal abstractions) plus one at the type level (type variables for type-terms in
10
Kind ::= ∗
| Kind → Kind
Type ::= Type Type −− type application
| λ TypeVar : Kind . Type −− type abstraction
Γ ` Nat : ∗ Γ ` Bool : ∗
Γ ` τ1 : ∗ Γ ` τ2 : ∗
Γ ` (τ1 → τ2) : ∗
Γ ` τ1 : ∗ Γ ` τ2 : ∗
Γ ` (τ1 × τ2) : ∗
Γ ` τ1 : ∗ Γ ` τ2 : ∗
Γ ` (τ1 + τ2) : ∗
Γ, α : κ ` τ : ∗
Γ ` ∀α :κ . τ : ∗
Γ(α) = κ
Γ ` α : κ
Γ ` τ1 : κ → ν Γ ` τ2 : κ
Γ ` (τ1 τ2) : ν
Γ, α : κ ` τ : ν
Γ ` (λα :κ . τ) : κ → ν
(λα :κ . τ) τ ′ I τ [τ ′/α]
τ1 I τ
′
1
τ1 τ2 I τ
′
1
τ2
τ2 I τ
′
2
P τ2 I P τ
′
2
τ1 I τ
′
1
τ2 I τ
′
2
τ1 + τ2 I τ
′
1
+ τ ′
2
τ1 I τ
′
1
τ2 I τ
′
2
τ1 × τ2 I τ
′
1
× τ ′
2
τ1 I τ
′
1
τ2 I τ
′
2
τ1 → τ2 I τ
′
1
→ τ ′
2
τ I τ ′
∀α :κ . τ I ∀α :κ . τ ′ τ I τ
τ1 I τ2 τ2 I τ3
τ1 I τ3
τ ≡ τ
τ1 ≡ τ2
τ2 ≡ τ1
τ1 ≡ τ2 τ2 ≡ τ3
τ1 ≡ τ3
τ1 ≡ σ1 τ2 ≡ σ2
τ1 → τ2 ≡ σ1 → σ2
τ ≡ σ
∀x :κ . τ ≡ ∀x :κ . σ
τ ≡ σ
λα :κ . τ ≡ λα :κ . σ
τ1 ≡ σ1 τ2 ≡ σ2
τ1 τ2 ≡ σ1 σ2 (λα :κ . τ) τ
′
≡ τ [τ ′/α]
Figure 5: System F
ω
adds type operators, a reduction relation (I), and an equivalence relation
(≡) on type-terms.
11
type-level abstractions).
7 Adding general recursion
All the languages described so far are strongly normalising, i.e., terms and type-terms always
reduce to normal form [Pie02, Mit96]. However, in order to use System F
ω
for real programming
we need to introduce some form of recursion. In this section we extend the language of terms
and types to cater for general recursive functions and type operators. In functional languages,
functions (term-level or type-level) are recursive when the function name is applied to another
term within its own body. For instance, the recursive definition of the list type and the factorial
function can be written in Haskell as follows:
data List a = Nil | Cons a (List a)
factorial n = if n==0 then 1 else n ∗ factorial(n-1)
Which can be translated to the lambda notation of System F
ω
as follows:
List = λa:∗. 1 + (a × (List a))
factorial = λn:Nat. if n==0 then 1 else n ∗ factorial (n-1)
But term and type lambda abstractions are unnamed; the naming mechanism above is meta-
notation. Recursion must be achieved indirectly. Let us abstract in both cases over the name of
the function to remove the recursion:
List◦ = λf:∗ → ∗. λa:∗. 1 + (a × f a)
factorial◦ = λf:Nat→Nat. λn:Nat. if n==0 then 1 else n ∗ f (n-1)
It is typical at this point to resort to meta-level arguments or denotational semantics to explain
that the equations:
List = List◦ List
factorial = factorial◦ factorial
have a least solution in some semantic domain that gives meaning to System F
ω
syntax. Such
solution is the least fixed point of the equation. Fortunately, there is no need to resort to meta-
level arguments. Operationally, recursive functions are reduced by unfolding their body at each
recursive call. This unfolding can be carried out at the object level by two new primitive term
and type constants fix and Fix respectively. They are called fixed-point operators because,
semantically, they return the least fixed point of their argument.3 Their type- and kind-signatures
are respectively:
fix : ∀τ :κ. (τ → τ ) → τ
Fix : ∀κ. (κ → κ) → κ
Their type-checking and reduction rules are shown in Figure 6. The intuition is that at the
meta-level, the following equations must hold:
3Fixed-point operators are also denoted Y and µ in the literature.
12
Type ::= Fix Type
Term ::= fix Term
Γ ` τ : κ → κ
Γ ` Fix τ : κ
Γ ` t : τ → τ
Γ ` fix t : τ
Fix (λα :κ . τ) I τ [α/Fix (λα :κ . τ)] fix (λx :α . t) B t[x/fix (λx :α . t)]
Figure 6: Extension of System F
ω
with fixed-point operators.
(fix f◦) = f◦ (fix f◦)
(Fix F◦) = F◦ (Fix F◦)
which turned into reduction rules give:
(fix f◦) B f◦ (fix f◦)
(Fix F◦) I F◦ (Fix F◦)
but since F◦ and f◦ abbreviate respectively type and term lambda abstractions, we have:
(fix (λx :α . t)) B (λx :α . t) (fix (λx :α . t))
B t[x/(fix (λx :α . t))]
(Fix (λα :κ . τ)) I (λα :κ . τ) (Fix (λα :κ . τ))
I τ[α/(Fix (λα :κ . τ))]
Figure 6 collects these steps in a single reduction rule. Call-by-name guarantees that recursive
calls are unfolded only when their value is required.
Going back to our examples, the terms:
Fix (λf:∗ → ∗. λa:∗. 1 + (a × f a))
fix (λf:Nat→Nat. λn:Nat. if n==0 then 1 else n ∗ f (n-1))
are both legal System F
ω
syntax that represent the recursive list type operator and the factorial
function. The following is an example reduction that demonstrates the unfolding (ellipsis abbre-
viate some subexpressions and reduction steps):
(fix (λf:Nat→Nat. λn:Nat. if n==0 then 1 else n ∗ f (n-1))) 2
B (λn:Nat. if n==0 then 1 else n ∗ (fix . . . ) (n-1)) 2
B if 2==0 then 1 else 2 ∗ (fix . . . ) (2-1)
B if false then 1 else 2 ∗ (fix . . . ) (2-1)
B 2 ∗ (fix . . . ) (2-1)
B 2 ∗ (λn:Nat. if n==0 then 1 else n ∗ (fix . . . )) (2-1)
B 2 ∗ if (2-1)==0 then 1 else (2-1) ∗ (fix . . . ) ((2-1)-1)
13
. . .
B 2 ∗ if false then 1 else (2-1) ∗ (fix . . . ) ((2-1)-1)
B 2 ∗ (2-1) ∗ (fix . . . ) ((2-1)-1)
. . .
B 2 ∗ (2-1) ∗ 1
. . .
B 2
Et Voilà.
14
References
[Bar84] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland,
Amsterdam, revised edition, 1984.
[Blo91] Stephen Blott. Type Classes. PhD thesis, Glasgow University, Glasgow, Scotland, UK,
1991.
[Car97] Luca Cardelli. Type systems. In Allen B. Tucker, editor, The Computer Science and
Engineering Handbook. CRC Press, Boca Raton, FL, 1997. Revised 2004.
[Chu41] Alonzo Church. The Calculi of Lambda Conversion. Princeton University Press, 1941.
[CW85] Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and poly-
morphism. Computer Surveys, 17(4):471–522, December 1985.
[Gir72] Girard, J.-Y. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique
d’Ordre Supérieur. Thèse de doctorat d’état, Université Paris VII, June 1972.
[HS86] J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and λ-Calculus.
London Mathematical Society, Student Texts 1. Cambridge University Press, 1986. Re-
print 1993.
[Jon92] Mark P. Jones. Qualified Types: Theory and Practice. PhD thesis, Oxford University,
July 1992.
[Lan66] Peter J. Landin. The next 700 programming languages. Communications of the ACM,
9(3):157–164, March 1966. Originally presented at the Proceedings of the ACM Program-
ming Language and Pragmatics Conference, August 8–12, 1965.
[Mit96] John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
[Pie02] Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
[Rea89] Chris Reade. Elements of Functional Programming. International Series in Computer
Science. Addison-Wesley, 1989.
[Rey74] John C. Reynolds. Towards a theory of type structure. In Programming Symposium,
Proceedings Colloque sur la Programmation, pages 408–423. Springer-Verlag, 1974.
[Sto77] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming
Language Semantics. MIT Press, Cambridge, Massachusetts, 1977.
[Str92] Bjarne Stroustrup. The C++ Programming Language. Addison Wesley, 2nd edition, 1992.
[WB89] Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In 16th
ACM Symposium on Principles of Programming Languages, pages 60–76, 1989.
15