Some more worked examples for G6021 Comparative Programming
1 Types: building derivations
We can find the type of a term by building a derivation. We need these three rules:
(VAR) Γ, x : A ⊢ x : A
Γ, x : A ⊢ M : B
(ABS)
Γ⊢λx.M :A→B
Γ⊢M:A→B Γ⊢N:A
(APP)
Γ ⊢ MN : B
ThenotationΓ⊢t:Ameansthattheλ-termthastypeAinthecontextΓ. Γisalistof typedvariables,forexamplex:A,y:B→C,z:A→B,etc. Eachruletellsushowtotypea λ-term, depending on the structure of the term.
• If it is a variable, x, then the type will be found in the context.
• If it is an abstraction λx.M then we add x : A to the context (A is a new type variable),
and we use the rules to type M. If M : B, then the type of the abstraction is A → B.
• If it is an application MN, then we find the type of M, which must be a function type, say A → B. We find the type of N which must be the same type as the function expects: A. We then deduce that the type of the application is B. Unification is used when we need to make two types equal.
We name the rules VAR, ABS and APP respectively. We can use these derivations in a number of different ways. The most useful for us is to build the type of a λ-term. Here are some worked examples.
1. Buildaderivationendingin⊢λxy.xy:(A→B)→A→B.
Note that you have been given the type in this example. We just need to build the derivation:
x : A → B, y : A ⊢ x : A → B x : A → B, y : A ⊢ y : A x : A → B, y : A ⊢ xy : B
x : A → B ⊢ λy.xy : A → B
⊢ λx.λy.xy : (A → B) → A → B
To help check your understanding, identify which rule was used in each case.
2. By building a derivation, find the type of λx.x.
To answer this question, we need to build a derivation ending in ⊢ λx.x : T where T is the type. We now look to see which typing rule was the last one used (i.e. which of the above
1
three rules must be used to give the final result). There is only one that fits: ABS. Therefore
the derivation must end in:
x : A ⊢ x 😕
(ABS) ⊢ λx.x 😕
In using the rule, we put the variable x in the context with a new type A. Now, there is only one rule that we can use to complete the derivation: VAR:
x:A⊢x:A ⊢ λx.x 😕
It is now possible to see that ? must be A → A from the rule ABS.
3. By building a derivation, find the type of λx.λy.x
x : A, y : B ⊢ x : A
x : A ⊢ λy.x : B → A ⊢ λx.λy.x : A → B → A
4. By building a derivation, find the type of λxy.yx
x : A, y : A → B ⊢ y : A → B x : A, y : A → B ⊢ x : A x : A, y : A → B ⊢ yx : B
x : A ⊢ λy.yx : (A → B) → B
⊢ λx.λy.yx : A → (A → B) → B
Remember that arrow associates to the right: A → ((A → B) → B)
5. By building a derivation, find the type of λfx.f(fx)
f : A → A, x : A ⊢ f : A → A f : A → A, x : A ⊢ x : A f : A → A,x : A ⊢ f : A → A f : A → A,x : A ⊢ fx : A
f :A→A,x:A⊢f(fx):A
f :A→A⊢λx.f(fx):A→A
⊢ λf.λx.f(fx) : (A → A) → A → A
6. Try to finish this one: λxyz.xz(yz) (See over page for solution).
⊢ λxyz.xz(yz) : (A → B → C) → (A → B) → A → C
In all the above examples, try to identify each rule that was used at each step (VAR, ABS or APP).
2
Details for the final question:
Γ⊢x:A→B→C Γ⊢z:A Γ⊢y:A→B Γ⊢z:A Γ ⊢ xz : B → C Γ ⊢ yz : B
Γ = x : A → B → C, y : A → B, z : A ⊢ xz(yz) : C
x : A → B → C, y : A → B ⊢ λz.xz(yz) : A → C
x : A → B → C ⊢ λyz.xz(yz) : (A → B) → A → C
⊢ λxyz.xz(yz) : (A → B → C) → (A → B) → A → C
3