Instructions: Please solve the questions using pen and paper and scan the images. Every image should contain your roll number and name.
1. Derive the type of each lambda expression. Show all derivation steps.
[3 * 5 = 15]
(a) Given E0 ∪ y : bool :
y := true
(b) Given type constants func1 : A → B and func2 : (C → B) :
λ(x : A).(func1 x);λ(q : C).(func2 q)
(c) Given | be a constant of type Bool → Bool → Bool and type of true is Bool λ(ω : Bool → π). λ(x : Bool). (ω (x | true))
(d) Given + is type constant with the type S → S.
λ(f : S → C). λ(x : S). f(+x)
(e) Given E0 = {x : Ref Bool, y : Bool} and the constants succ : Int → Int, true : Bool, 4 : Int :
succ 4; x := true
2. Derive the type of each of the following expression. Any assumptions are welcome. [5 * 2 = 10]
(a) Given the type of φ is Float → Integer
(λ(p : Float → Integer). λ(f : Float → Float). λ(y : Float). p (f (f y))) φ
(b) Given φ be the constant with the type Bool → Bool → Bool and true with the type Bool λ(func1 : Bool → Char). λ(τ : Bool). func1 (τ φ true)
1
