You will need a unicode font to view this homework.
The compiler will generate more code for the C++ Templates version because in order to allocate enough room to hold the data objects directly, it needs to create a different version of the function for each datatype.
The ML implementation, on the other hand, stores everything as references, which are all the same size regardless of type. Therefore it can use a single version to handle all types.
The C++ version will be more efficient at run time. It does not need to carry around and check tags, and it does not need to dereference the objects every time they are used.
Δ |&minus unit ok
t ∈ Δ
Δ |&minus t ok
Δ |&minus τ_{1} ok Δ |&minus τ_{2} ok
Δ |&minus τ_{1} → τ_{2} ok
Δ |&minus τ_{1} ok Δ |&minus τ_{2} ok
Δ |&minus (τ_{1} + τ_{2}) ok
Δ∪{t} |&minus τ ok (t ∉ &Delta)
Δ |&minus ∀(τ) ok
Δ∪{t} |&minus τ ok (t ∉ &Delta)
Δ |&minus ∃t(τ) ok
Δ |&minus Γ(x) ok ∀x∈dom(Γ)
Δ |&minus Γ ok
Γ |−_{Δ} ():unit
Δ |&minus τ_{1} ok Γ[x:τ_{1}] |−_{Δ} e:τ_{2} (x ∉ dom(Γ))
Γ |−_{Δ} fn(x:τ_{1}) ⇒ e:τ_{1}→τ_{2}
Γ |−_{Δ} e_{1}:τ_{2}→τ Γ |−_{Δ} e_{2}:τ_{2}
Γ |−_{Δ} apply(e_{1},e_{2}):τ
Γ |−_{Δ} e:τ_{1} Δ |&minus τ_{2} ok
Γ |−_{Δ} inl_{(τ1+τ2)}(e):(τ_{1}+τ_{2})
Γ |−_{Δ} e:τ_{2} Δ |&minus τ_{1} ok
Γ |−_{Δ} inr_{(τ1+τ2)}(e):(τ_{1}+τ_{2})
Γ |−_{Δ∪{t}} e:σ t ∉ Δ
Γ |−_{Δ} Fun t in e:∀t(σ)
Γ |−_{Δ} e:(τ_{1}+τ_{2}) Γ[x_{1}:τ_{1}] |−_{Δ} e_{1}:τ Γ[x_{2}:τ_{2}] |−_{Δ} e_{2}:τ (x_{1},x_{2} ∉ dom(Γ))
Γ |−_{Δ} case_{τ} e of inl(x_{1}:τ_{1})⇒e_{1} | inr(x_{2}:τ_{2})⇒e_{2} :τ
Γ |−_{Δ} e:∀t(σ) Δ |&minus τ ok
Γ |−_{Δ} inst(e,τ):{τ/t}σ
Δ |&minus τ ok Δ |&minus ∃t(σ) ok Γ |−_{Δ} e:{τ/t}σ
Γ |−_{Δ} pack τ with e as ∃t(σ):∃t(σ)
Δ |&minus τ_{c} ok Γ,x:σ |−_{Δ} e_{c}:τ_{c} Γ |−_{Δ} e_{i}:∃t(σ) t ∉ Δ
Γ |−_{Δ} open e_{i} as t with x:σ in e_{c}:τ_{c}
Prove If Δ |− Γ ok and Γ |−_{Δ} e:τ then Δ |&minus τ ok
IH(Δ |− Γ ok, Γ |−_{Δ} e:τ then Δ |&minus τ ok)
1. | Δ |− Γ ok and Γ |−_{Δ} ():unit | by assumption |
2. | Δ |− unit ok | by DU |
1. | Δ |− Γ ok and Γ |−_{Δ} fn(x:τ_{1})⇒e:τ_{1}→τ_{2} | by assumption |
2. | Δ |− τ_{1} ok and Γ[x:tau;_{1}] |−_{Δ}e:τ_{2} | by |
3. | Δ |− τ_{2} ok | by IH(Δ |− Γ ok, Γ[x:τ_{1}] |−_{Δ} e:τ_{2}), 1, and 2 |
4. | Δ |− τ_{1}→τ_{2} ok | by DF, 2, and 3 |
1. | Δ |− Γ ok and Γ |−_{Δ} apply(e_{1},e_{2}):τ) | by assumption |
2. | Γ |−_{Δ} e_{1}:τ_{2}→τ) | by invert TA |
3. | Δ |− τ_{2}→τ ok | by IH(Δ |− Γ ok, Γ |−_{Δ} e_{1}:τ_{2}→τ), 1, and 2 |
4. | Δ |− τ ok | by invert DF and 3 |
1. | Δ |− Γ ok and Γ |−_{Δ} inl_{(τ1+τ2)}(e):(τ_{1}+τ_{2}) | by assumption |
2. | Γ |−_{Δ} e:τ_{1} and Δ |− τ_{2} ok | by invert TL |
3. | Δ |− τ_{1} ok | by IH(Δ |− Γ ok, Γ |−_{Δ} e:τ_{1}), 1, and 2 |
4. | Δ |− τ_{1}+τ_{2} ok | by DS, 2, and 3 |
1. | Δ |− Γ ok and Γ |−_{Δ} Fun t in e:∀t(σ) | by assumption |
2. | Γ |−_{Δ∪{t}} e:σ and t ∉ Δ | by invert TN |
3. | Δ∪{t} |− σ ok | by IH(Δ |− Γ ok,Γ |−_{Δ∪{t}} e:σ) and 2 |
4. | Δ |− ∀t(σ) | by D∀, 1, 2, and 3 |
1. | Δ |− Γ ok and Γ |−_{Δ} case_{τ} e of inl(x_{1}:τ_{1})⇒e_{1} | inr(x_{2}:τ_{2})⇒e_{2} :τ | by assumption |
2. | Γ |−_{Δ} e_{1}:τ | by invert TC |
3. | Δ |− τ ok | by IH(Δ |− Γ,Γ |−_{Δ} e_{1}:τ), 1, and 2 |
1. | Δ |− Γ ok and Γ |−_{Δ} inst(e,τ):{τ/t}σ | by assumption |
2. | Δ |− τ ok and Γ |−_{Δ} e:∀t(σ) | by invert TI |
3. | Δ |− ∀t(σ) | by IH(Δ |− Γ ok, Γ |−_{Δ} e:∀t(σ)), 1, and 2 |
4. | Δ∪{t} |− σ ok | by invert D∃ |
5. | Δ |− {τ/t}σ ok | by some kind of substitution lemma |
1. | Δ |− Γ ok and Γ |−_{Δ} pack τ with e as ∃t(σ):∃t(σ) | by assumption |
2. | Δ |− ∃t(σ) ok | by invert TP |
1. | Δ |− Γ ok and Γ |−_{Δ} open e_{i} as t with x:σ in e_{c}:τ_{c} | by assumption |
2. | &Delta |− τ_{c} | by invert TO |