Eq :: ∗ ⇒ ∗ ⇒ ∗
= λα::∗.λβ::∗.∀φ::∗⇒∗.φα→φβ
refl : ∀α::∗.Eqαα
= Λα::∗.Λφ::∗⇒∗.λx:φα.x
symm : ∀α::∗.∀β::∗.Eqαβ → Eqβα
= Λα::∗.Λβ::∗.λe:(∀φ::∗⇒∗.φα → φβ).e [λγ::∗.Eqγα] (refl [α])
trans : ∀α::∗.∀β::∗.∀γ::∗.Eqαβ → Eqβγ → Eqαγ
= Λα::∗.Λβ::∗.Λγ::∗.λab:Eqαβ.λbc:Eqβγ.bc [Eqα] ab
Zero :: ∗ =∀α::∗.α
Unit :: ∗ =∀α.α → α
unit : Unit =λα.λx:α.x
Z::∗
= Zero
S::∗⇒∗
= λX . X + U n i t
Neq : : ∗ ⇒ ∗ ⇒ ∗ =λα.λβ.Eqαβ →Zero
sz distinct : ∀N.Neq (S N) Z
=λN.λeq:Eq (S N) Z. eq [λX.X] (inr [N] unit)
eq pred : ∀M.∀N.Eq (S M) (S N) → Eq M N
Figure 1: Definitions in System Fω
2
1 Types and type inference
(a) For each of the following System Fω terms either give a typing derivation or explain why there is no such derivation
(i) Λα::*.λf:α → α.f f
(ii) λf:(∀α::*.α).f [∀α.α → α] [∀α.α] f
(iii) λf:(∀φ::* ⇒ *.∀α.φ α → φ α).Λα.f [α] [α]
(6 marks) (b) Algorithm J is defined recursively over the structure of terms. The case for
function application (M N) is as follows:
J (Γ, M N) = β
where A = J (Γ, M)
and B = J (Γ, N)
and unify’ ({A = B → β}) succeeds and β is fresh
Give similar cases to handle the following constructs: (i) Constructing a value of sum type using inl: inl M
(ii) Scrutinising a value of sum type: case L of x.M | y.N
(c) Both the case for let in Algorithm J and the corresponding typing rule only generalize (quantify) type variables that are not already in the context. Explain by means of an example what problems would arise if type variables in the context were also generalized.
(3 marks)
3
(4 marks)
2 De Morgan’s laws in Fω
In lecture 2 we saw System Fω encodings of a number of types, including the type with one inhabitant (equivalent to OCaml’s unit type), and the type with two inhabitants (equivalent to bool). We can also encode the type with no inhabitants, following the same pattern:
Zero :: ∗
Zero = ∀α::*.α
Under the Curry-Howard correspondence, Zero represents the false proposition, and the fact that it has no inhabitants corresponds to the fact that the false proposition has no proof. The fold for Zero corresponds to the logical principle ex falso quodlibet (“from falsehood anything follows”):
foldZero : Zero → ∀α::*.α foldZero = λe:Zero.e
Using Zero, we can represent logical negation as a type operator :
Not :: * ⇒ *
Not = λA.A → Zero
and using Not we can build System Fω types corresponding to De Morgan’s laws: DM1 = ∀α.∀β.Not(α × β) → (Notα + Notβ)
DM2 = ∀α.∀β.(Notα + Notβ) → Not(α × β)
DM3 = ∀α.∀β.Not(α + β) → (Notα × Notβ)
DM4 = ∀α.∀β.(Notα × Notβ) → Not(α + β)
- (a) Three of De Morgan’s laws have proofs in System Fω — that is, it is possible
to write System Fω terms that have the corresponding types. (i) Add a term to exercise1.f for each of those three types.
(ii) Identify the type for which it is not possible to define a term, and explain (in a sentence or two) why it is not possible.
- (b) De Morgan’s laws can be extended from binary connectives to quantified propositions, treating universal quantification as a generalized product and existential quantification as a generalized sum. For example, the following definition may be viewed as a generalized version of DM1:
DM5 = ∀φ::* ⇒ *.Not (∀α.φ α) → (∃α.Not (φ α))
(i) Add types DM6, DM7 and DM8 representing similarly extended versions of DM2,DM3 and DM4 to exercise1.f.
4
(ii) For each of the types DM5, DM6, DM7 and DM8, either give a term of that type, or explain why it is not possible to define such a term.
(11 marks)
5
3 Vectors in Fω
System Fω is a total language—i.e. the evaluation of every System Fω expression completes without error, producing a value. For this reason a number of OCaml functions cannot be defined using the System Fω encoding of datatypes seen in the lectures. For example, here is the definition of a function hd that returns the first element of a list or fails if the list is empty:
val hd : ‘a list -> ‘a let hd = function
[] -> failwith “hd” | a::_ -> a
Since evaluating hd v may fail, there is no equivalent of this function in System Fω.
However, it is possible to define a richer sequence type that distinguishes between empty and non-empty lists, and for which hd can be defined. Here is a definition of a List-like type function Vec, whose two arguments respectively represent the type of the elements in the sequence and the length of the sequence:
Vec :: * ⇒ * ⇒ *
Vec = λα.λM.∀φ::*⇒*.φ Z → (∀N.α → φ N → φ (S N)) → φ M
For example, a value of type Vec Nat (S (S Z)) represents a sequence of two Nat values. We assume that we have available type operators Z (zero) and S (successor) for
constructing a representation of numbers:
Z :: *
S :: * ⇒ *
Furthermore, it will be useful to have representations of some basic facts about numbers. Making use of Eq from the lectures and Not from Question 2, we can define a type rerepsenting the proposition that one number is the predecessor of another:
Pred :: * ⇒ * ⇒ * = λM.λN.Eq (S M) N
and a term representing the fact that zero is not the successor of any number:
sz_distinct : ∀N.Not (Eql (S N) Z)
and a term representing the fact that successor is injective (i.e. that if S M is equal
toS NthenMisequaltoN):
eq_pred : ∀M.∀N.Eq (S M) (S N) → Eq M N
(a) Define Vec constructors nil and cons analogous to the constructors for lists, and with the following types:
nil : ∀α.Vec α Z
cons : ∀α.∀μ.α → Vec α μ → Vec α (S μ)
6
(Hint: this is relatively straightforward, and you should not need to make use of any of the facts about numbers.)
- (b) Define a function head that extracts the first element of a non-empty vector. Your function should have the following type:
head : ∀α.∀μ.Vec α (S μ) → α
(Hint: this is harder. The key is to find an appropriate instantiation for φ in thedefinition of Vec. Remember that the result type of φ may be a function type.)
- (c) Define tail a function tail that removes the first element of a non-empty vector.
Your function should have the following type:
tail : ∀α.∀μ.Vec α (S μ) → Vec α μ
(Hint: this is really quite tricky! You may find it helpful to start by defining an auxiliary function that returns a pair corresponding to the list itself together with its tail.)
- (d) The map function for Vec behaves similarly to map for lists: it changes the type of each element, but preserves the length. Give a definition of map with the following type:
map : ∀α.∀β.∀μ.(α → β) → Vec α μ → Vec β μ
7
(6 marks)