1 Records  25 Points

In this question we investigate records: they are tuples whose components, called fields, have labels. Actually tuples can be seen as records with numeric fields 1, 2 …; given a record we can access one of its component via its labels. For

example type id ={name:string,born:int}; if someid is of type id, you can

access the value corresponding to the name field with someid.name. This yields the following language, where we assume we are given a denumerable set of labels. The ordering on labels is immaterial.

Types τ ::= … | {l_{1} : τ_{1}, …, l_{n} : τ_{n}}
Expressions e ::= … | {l_{1} = e_{1}, …, l_{n} = e_{n}} | e.l
Values v ::= … | {l_{1} = v_{1}, …, l_{n} = v_{n}}

Note that n ≥ 0, which accounts for the empty record.

1. Part 1 (5 points). Give typing and SOS evaluation rules for this language.

2. Part 2 (10 points) We now want to add the following operations on records: record extension +, overriding ⊕ and subtraction \, with the following semantics

• r + {l = e} is defined as the addition of {l = e} to r provided that l is a new label.

• r ⊕ {l = e} is defined as the overwriting of r with {l = e} provided that l is one of the labels in r and its type is consistent.

• r \ {l = e} is defined as r minus {l = e} provided that l is one of the labels in r and its type is consistent.

Give typing and SOS evaluation rules for those operations. 2 3. Part 3 (10 points) We now want to add record concatenation, say r@r′.

How shall it behave on common labels? Give typing and SOS rules for your operator. Consider the typing rule T ype@; under the right formulation it is redundant, that is anything which can be derived with it can be derived without it. Prove that {l_{1} = v_{1}, …, l_{n} = v_{m}}@{l′_{1} = v′_{1}, …, l′_{n} = v′_{n}} can be typed without rule T ype@.

1. Answer 1.

\begin{matrix}\frac{Γ⊢e_{i}:τ_{i} ∀i.1≤i≤n}{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}:\{l_{1}:τ_{1},...,l_{n}:τ_{n}\}} & T ype\{\} \\ \frac{Γ⊢e:\{l_{1}:τ_{1},...,l_{n}:τ_{n}\} ∃i.1≤i≤n}{Γ⊢e.l_{i}:τ_{i}} & T ype. \\ \frac{∃i.1≤i≤n}{\{l_{1}=v_{1},...,l_{n}=v_{n}\}.l_{i}↦v_{i}} & [EvalF ield] \\ \frac{e↦e′}{\{...l=e...\}↦\{...l=e′...\}} & [SearchF ield] \end{matrix}

2. Answer 2. Let ∗ vary on +, ⊕, \

\frac{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}:\{l_{1}:τ_{1},...,l_{n}:τ_{n}\} ∀i.l≠l_{i} Γ⊢e:τ}{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}+\{l=e\}:\{l_{1}:τ_{1},...,l_{n}:τ_{n},l=e\}} T ype+
\frac{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}:\{l_{1}:τ_{1},...,l_{n}:τ_{n}\} ∃i.l=l_{i} Γ⊢e:τ τ=τ_{i}}{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}⊕\{l=e\}:\{l_{1}:τ_{1},...,l_{n}:τ_{n}\}} T ype⊕
\frac{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}:\{l_{1}:τ_{1},...,l_{n}:τ_{n}\} ∃i.l=l_{i} Γ⊢e:τ τ=τ_{i}}{Γ⊢\{l_{1}=e_{1},...,l_{n}=e_{n}\}\\{l=e\}:\{l_{1}:τ_{1},...,l_{i−1}:τ_{i−1},l_{i+1}:τ_{i+1},...,l_{n}:τ_{n}\}}T ype\

\frac{e↦e′}{\{l_{1}=v_{1},...,l_{n}=v_{n}\}∗\{l=e\}↦\{l_{1}=v_{1},...,l_{n}=v_{n}\}∗\{l=e′\}}SearchRHS
\frac{e_{i}↦e′_{i}}{\{l_{1}=e_{1},...,l_{n}=e_{n}\}∗\{l=e\}↦\{...l_{i}=e′_{i}...\}∗\{l=e\}}SearchLHS
\overline{\{l_{1}=v_{1},...,l_{n}=v_{n}\}+\{l=v\}↦\{l_{1}=v_{1},...,l_{n}=v_{n},l=v\}}Eval+
\frac{∃i.1≤i≤n}{\{l_{1}=v_{1},...,l_{n}=v_{n}\}⊕\{l=v\}↦\{l_{1}=v_{1},...,l_{i}=v,...,l_{n}=v_{n},l=v\}}Eval⊕
\frac{∃i.1≤i≤n}{\{l_{1}=v_{1},...,l_{n}=v_{n}\}\\{l=v\}↦\{l_{1}=v_{1},...,l_{i−1}=v_{i−1},l_{i=1}=v_{i=1},...,l_{n}=v_{n},l=v\}}Eval\

3. Answer 3. There are two ways, one following the semantics of +, the other ⊕. In the first case concatenation is defined only when the labels intersection is empty; in the second case we overwrite the common labels in the first record with the new values in the second one. For example, if we call dom(r) the set of labels occurring in a record r:

\begin{matrix}\frac{dom(r1)∩dom(r2)=∅ Γ⊢r1:τ_{1} Γ⊢r1:τ_{2}}{Γ⊢r1@r2:\{τ1,τ2\}} & T ype@ \\ \overline{\{l_{1}=v_{1},...,l_{n}=v_{m}\}@\{l′_{1}=v′_{1},...,l′_{n}=v′_{n}\}↦^{∗}\{l_{1}=v_{1},...,l_{m}=v_{m},l′_{1}=v_{1},...,l′_{n}=v′_{n}\}} & Eval@ \end{matrix}

If we define this version of @ in terms of +:

{l_{1} = e_{1}, …, l_{n} = e_{m}}@{l′_{1} = e′_{1}, …, l′_{n} = e′_{n}} =_{def} {l_{1} = e_{1}, …, l_{m} = e_{m}}+{l′_{1} = e_{1}}+, …, +{l′_{n} = e′_{n}}

The rules are derivable as it can be proven by induction on the length of the second record. Consider T ype@; if n = 1, the premises match T ype+, thus apply the latter. Assume that the result hold for n − 1 and again apply T ype+ as a last step.