COMPSCI 3MI3 – Principles of Programming Languages
J. Carette
McMaster University
Adapted from “Types and Programming Languages” by Benjamin C. Pierce
J. Carette (McMaster University) Data-Structures Fall 2023 1 / 9
Data-Structures
Adding data-structures: pairs
⟨t⟩ ::= …
| {t, t}.1
| {t, t}.2
⟨v⟩ ::= … | {v, v}
(E-Proj1) (E-Proj2) (E-Pair1)
t . 1 → t . 1 t → t′
t 2 → t 2′
{v1, t2} → {v1, t2′ }
t.2 → t′.2 t 1 → t 1′
{t1, t2} → {t1′ , t2} J. Carette (McMaster University)
{v1, v2}.1 → v1 {v1, v2}.2 → v2
(E-PairBeta1) (E-PairBeta2)
Data-Structures
Typing Pairs
⟨T⟩ ::= …
This is known as the product or the Cartesian Product type constructor.
Γ⊢t1 :T1 Γ⊢t2 :T2 Γ ⊢ {t1, t2} : T1 × T2
Γ ⊢ t : T1 × T2 Γ ⊢ t.1 : T1
Γ ⊢ t : T1 × T2 Γ ⊢ t.2 : T2
J. Carette
(McMaster University)
Data-Structures
程序代写 CS代考 加QQ: 749389476
Tuples: from 2 to n
⟨t⟩ ::= …
| {⟨t⟩, ⟨t⟩, …, ⟨t⟩} | t.i
where there are n terms in the first case, and 1 ≤ i ≤ n in the second. ⟨v⟩ ::= …
| {⟨v⟩,⟨v⟩,…,⟨v⟩} ⟨T⟩ ::= …
| {⟨T⟩×⟨T⟩×…×⟨T⟩ }
As this . . . notation can get tiresome, we use ⃗t, ⃗v and T⃗ .
J. Carette (McMaster University) Data-Structures Fall 2023 4 / 9
Evaluation Rules
j ∈ 1..n { ⃗v } . j → v j
t → t′ t.i → t′.i
tj → tj′ {v1,v2,…,vj−1,tj,…tn} → {v1,v2,…,vj−1,tj′,…tn}
(E-ProjTuple)
J. Carette (McMaster University) Data-Structures Fall 2023 5 / 9
Computer Science Tutoring
Tuping Typles
Γ⊢t2 :T2 …Γ⊢tn :Tn Γ ⊢ { ⃗t } : { T⃗ }
j ∈ 1..n Γ ⊢ t : {T⃗ } Γ ⊢ t.j : Tj
J. Carette
(McMaster University)
Data-Structures
Numbers are silly labels, let’s use names as labels. l ∈ L. ⟨t⟩ ::= …
| {⟨l⟩=⟨t⟩,⟨l⟩=⟨t⟩,…,⟨l⟩=⟨t⟩} | ⟨t ⟩.⟨l ⟩
⟨v⟩ ::= …
| {⟨l⟩=⟨v⟩,⟨l⟩=⟨v⟩,…,⟨l⟩=⟨v⟩}
⟨T⟩ ::= …
| {⟨l⟩: ⟨T⟩,⟨l⟩: ⟨T⟩,…,⟨l⟩: ⟨T⟩}
structs in C, object with only fields in Java, dictionaries (sort of) in Python
J. Carette (McMaster University) Data-Structures Fall 2023 7 / 9
Evaluation Rules
j ∈ 1..n −−→
(E-ProjRcd)
{l = v}.lj → vj t → t′
t.li → t′.li tj → tj′
{l1 = v1,…,lj−1 = vj−1,lj = tj,…ln = tn} → {l1 = v1,…,lj−1 = vj−1,lj = tj′,…ln = tn}
Note: order of labels is induced by the language somehow. Usually at type declaration time.
J. Carette (McMaster University) Data-Structures Fall 2023 8 / 9
Γ⊢t1 :T1 Γ⊢t2 :T2 …Γ⊢tn :Tn −−→ −−→
Γ⊢{f =t}:{f :T}
j ∈ 1..n Γ ⊢ t : {T }
→− Γ ⊢ t.j : Tj
J. Carette
(McMaster University)
Data-Structures
Code Help, Add WeChat: cstutorcs