Type Systems Exercises
- Find the term of the following λ→ types:
- (α → β) → (α → α → β)'
- ((α → β) → δ) → β → δ
- Compute the principle type of λx.λy.y x(λz.x)
- Type λx.xxx in λ2-Curry.
- Prove that all normal forms are typeable in λ2.
- Define Sum: ListNat → Nat that sums the elements of a list.