1 Types
Some more notes on Types G6021 Comparative Programming
You should know how to type Haskell expressions (see lab exercises for some examples). When the λ-calculus is used in Haskell expressions, you may find it useful to build a derivation or use the type reconstruction algorithm. However, informal reasoning is sufficient for Haskell expressions.
Example: what is the type of \x -> \y -> x y?
Solution: So that xy can have a type, x must be a function, say C → D, and y must have type C so that xy : D. Putting this together, we have the overall type: (C →D)→C →D.
Try to find the types of the following, using the same ideas: 1.\x->\y-> yx
2. \x -> \y -> x(x y) 3. \x -> \y -> x (y 3)
You should know how to unify types (by first finding the disagreement pair). Try the following. What is the result of each of the following?
2
1. U(a,b→c)
Solution: a = b → c
2. U(a→b,c→d)
Solution: a=c,b=d
3. U(a→b,c→d→e)
Solution: a=c,b=d→e
Types: More derivations
1. Build a type derivation to find the type of λx.(λy.y)x
x : A, y : A ⊢ y : A
x : A ⊢ λy.y : A → A x : A ⊢ x : A
x : A ⊢ (λy.y)x : A ⊢ λx.(λy.y)x : A → A
1
2. Build a type derivation to find the type of λx.x(λy.y)
x : (A → A) → B, y : A ⊢ y : A x : (A → A) → B ⊢ x : (A → A) → B x : (A → A) → B ⊢ λy.y : A → A
x : (A → A) → B ⊢ x(λy.y) : B
⊢ λx.x(λy.y) : ((A → A) → B) → B
3. Build a type derivation to find the type of W = λxy.xyy
x:A→A→B,y:A⊢x:A→A→B x:A→A→B,y:A⊢y:A
x : A → A → B, y : A ⊢ xy : A → B x : A → A → B, y : A ⊢ y : A
x : A → A → B, y : A ⊢ xyy : B
x : A → A → B ⊢ λy.xyy : A → B ⊢ λxy.xyy : (A → A → B) → A → B
4. Showing that a term does not have a type can be done in a number of different ways. For example, if we try to type: D = λxy.xxy, then we can start with:
x :?, y 😕 ⊢ xx 😕 x :?, y 😕 ⊢ y 😕 x :?, y 😕 ⊢ xxy 😕
x 😕 ⊢ λy.xxy 😕
⊢ λxy.xxy 😕
We cannot make any progress here, because xx cannot be typed. To see this, x must be a function say, x : A → B, and also the argument of this function, so must be x : A. Now, the problem is that we cannot make A → B and A equal (they do not unify).
2