Assignment 8

Elika Etemad, COS 441

You will need a unicode font to view this homework.

Problem 1

  1. 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.

  2. 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.

Problem 2

  1. Δ |&minus τ ok

    DU

     

    Δ |&minus unit ok

    Dt

    t ∈ Δ

    Δ |&minus t ok

    DF

    Δ |&minus τ1 ok Δ |&minus τ2 ok

    Δ |&minus τ1 → τ2 ok

    DS

    Δ |&minus τ1 ok Δ |&minus τ2 ok

    Δ |&minus (τ1 + τ2) ok

    D∀

    Δ∪{t} |&minus τ ok (t ∉ &Delta)

    Δ |&minus ∀(τ) ok

    D∃

    Δ∪{t} |&minus τ ok (t ∉ &Delta)

    Δ |&minus ∃t(τ) ok

    Δ |&minus Γ(x) ok ∀x∈dom(Γ)

    Δ |&minus Γ ok

  2. Γ |−Δ e:τ

    TU

     

    Γ |−Δ ():unit

    TF

    Δ |&minus τ1 ok Γ[x:τ1] |−Δ e:τ2 (x ∉ dom(Γ))

    Γ |−Δ fn(x:τ1) ⇒ e:τ1→τ2

    TA

    Γ |−Δ e12→τ Γ |−Δ e22

    Γ |−Δ apply(e1,e2):τ

    TL

    Γ |−Δ e:τ1 Δ |&minus τ2 ok

    Γ |−Δ inl12)(e):(τ12)

    TR

    Γ |−Δ e:τ2 Δ |&minus τ1 ok

    Γ |−Δ inr12)(e):(τ12)

    TN

    Γ |−Δ∪{t} e:σ t ∉ Δ

    Γ |−Δ Fun t in e:∀t(σ)

    TC

    Γ |−Δ e:(τ12) Γ[x11] |−Δ e1 Γ[x22] |−Δ e2 (x1,x2 ∉ dom(Γ))

    Γ |−Δ caseτ e of inl(x11)⇒e1 | inr(x22)⇒e2

    TI

    Γ |−Δ e:∀t(σ) Δ |&minus τ ok

    Γ |−Δ inst(e,τ):{τ/t}σ

    TP

    Δ |&minus τ ok Δ |&minus ∃t(σ) ok Γ |−Δ e:{τ/t}σ

    Γ |−Δ pack τ with e as ∃t(σ):∃t(σ)

    TO

    Δ |&minus τc ok Γ,x:σ |−Δ ecc Γ |−Δ ei:∃t(σ) t ∉ Δ

    Γ |−Δ open ei as t with x:σ in ecc

Problem 3

Prove If Δ |− Γ ok and Γ |−Δ e:τ then Δ |&minus τ ok

IH(Δ |− Γ ok, Γ |−Δ e:τ then Δ |&minus τ ok)

case TU: IH(Δ |− Γ ok, Γ |−Δ ():unit)
1. Δ |− Γ ok and Γ |−Δ ():unit by assumption
2. Δ |− unit ok by DU
case TF: IH(Δ |− Γ ok, Γ |−Δ fn(x:τ1)⇒e:τ1→τ2)
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
case TA: IH(Δ |− Γ ok, Γ |−Δ apply(e1,e2):τ)
1. Δ |− Γ ok and Γ |−Δ apply(e1,e2):τ) by assumption
2. Γ |−Δ e12→τ) by invert TA
3. Δ |− τ2→τ ok by IH(Δ |− Γ ok, Γ |−Δ e12→τ), 1, and 2
4. Δ |− τ ok by invert DF and 3
case TL: IH(Δ |− Γ ok, Γ |−Δ inl12)(e):(τ12))
1. Δ |− Γ ok and Γ |−Δ inl12)(e):(τ12) by assumption
2. Γ |−Δ e:τ1 and Δ |− τ2 ok by invert TL
3. Δ |− τ1 ok by IH(Δ |− Γ ok, Γ |−Δ e:τ1), 1, and 2
4. Δ |− τ12 ok by DS, 2, and 3
case TR: IH(Δ |− Γ ok, Γ |−Δ inr12)(e):(τ12))
as for TL, above
case TN: IH(Δ |− Γ ok, Γ |−Δ Fun t in e:∀t(σ))
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
case TC: IH(Δ |− Γ ok, Γ |−Δ caseτ e of inl(x11)⇒e1 | inr(x22)⇒e2 :τ)
1. Δ |− Γ ok and Γ |−Δ caseτ e of inl(x11)⇒e1 | inr(x22)⇒e2 by assumption
2. Γ |−Δ e1 by invert TC
3. Δ |− τ ok by IH(Δ |− Γ,Γ |−Δ e1:τ), 1, and 2
case TI: IH(Δ |− Γ ok, Γ |−Δ inst(e,τ):{τ/t}σ)
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
case TP: IH(Δ |− Γ ok, Γ |−Δ pack τ with e as ∃t(σ):∃t(σ))
1. Δ |− Γ ok and Γ |−Δ pack τ with e as ∃t(σ):∃t(σ) by assumption
2. Δ |− ∃t(σ) ok by invert TP
case TO: IH(Δ |− Γ ok, Γ |−Δ open ei as t with x:σ in ecc)
1. Δ |− Γ ok and Γ |−Δ open ei as t with x:σ in ecc by assumption
2. &Delta |− τc by invert TO

Problem 4

  1. (int * int* int)
  2. (shape * shape)
  3. shape
  4. shape