PFPL Chapter 6 Type Safety

Posted on In Disqus:

Please refer this link from page 49 to 54.

Intros

Type safety expresses the coherence between the statics and the dynamics. Statics may be seen as predicting that the value of an expression will have a certain form so that the dynamics of the expression will be well-defined. Thus, evaluation will not get stuck.

The theorem of type safety for E is defined as:

  • (Preservation) If $e : \tau$ and $e \longmapsto e’$, then $e’: \tau$.
  • (Progress) If $e : \tau$ and either $e \text{ val}$ or $\exists e’$ such that $e \longmapsto e’$.

Safety is the conjunction of preservation and progress.

$e \text{ stuck}$ iff $\neg e \text{ val}$ and $\not\exists e’$ such that $e \longmapsto e’$. Based on safety theorem, stuck state is necessarily ill-typed.

Preservation

Theorem

The preservation theorem of E is defined as: If $e : \tau$ and $e \longmapsto e’$, then $e’: \tau$.

For plus, times, cat, len, the proof can be constructed as:

$$
\dfrac{e_0 \longmapsto e_0’}{op(e_0;e_1) \longmapsto op(e_0’;e_1)}\phantom{“”} \dfrac{e_0 \longmapsto e_0’}{op(e_0) \longmapsto op(e_0’)}
$$

With such forms of rules, we assume that $e_0 : \tau$ and $e_1 : \tau$, then $op(e_0;e_1) :\tau$, by induction $e_0’:\tau$.

For let, the proof is constructed as:

$$
\dfrac{}{\text{let}(e; x.e_1)\longmapsto[e/x]e_1}
$$

Assume that $\text{let}(e;x.e_1):\tau$, by inversion of typing lemma in chapter 4, $\Gamma, x:\tau_0 \vdash e_1 : \tau$ and $\Gamma \vdash e : \tau_0$.

By substitution lemma in chapter 4, $[e/x]e_1 : \tau$.

Progress

Progress theorem captures the idea that well-typed programs do not get stuck.

Lemma

Canonical Forms: If $e\text{ val}$ and $e :\tau$, then

  • If $\tau = \text{num}$, then $e = \text{num}[n]$ for some $n$.
  • If $\tau = \text{str}$, then $e = \text{str}[s]$ for some $s$.

Theorem

If $e : \tau$ and either $e \text{ val}$ or $\exists e’$ such that $e \longmapsto e’$.

For plus, times, cat, len, the proof can be constructed as:

$$
\dfrac{e_0 \longmapsto e_0’}{op(e_0;e_1) \longmapsto op(e_0’;e_1)}\phantom{“”} \dfrac{e_0 \longmapsto e_0’}{op(e_0) \longmapsto op(e_0’)}
$$

WLOG we consider binary operator situation:

  • $\exists e_0’​$ that $e_0 \longmapsto e_0’​$, $e_1 \text{ val}​$, then $op(e_0;e_1) \longmapsto op(e_0’;e_1)​$
  • $\exists e_1’$ that $e_1 \longmapsto e_1’$, $e_0 \text{ val}$, then $op(e_0;e_1) \longmapsto op(e_0;e_1’)$
  • $e_0 \text{ val}$ and $e_1 \text{ val}$, then follow instruction rules to become value.
  • $\exists e_0’$ that $e_0 \longmapsto e_0’$, $\exists e_1’$ that $e_1 \longmapsto e_1’$, then $op(e_0;e_1) \longmapsto op(e_0’;e_1’)$

For let, the proof has form

$$
\dfrac{}{\text{let}(e; x.e_1)\longmapsto[e/x]e_1}
$$

  • If $e \longmapsto e’$, then $\text{let}(e;x.e_1) \longmapsto \text{let}(e’;x.e_1)$
  • If $\Gamma , x :\tau \vdash e_1 \longmapsto e_1’$, then $\text{let}(e;x.e_1) \longmapsto \text{let}(e;x.e_1’)$
  • $\text{let}(e;x.e_1) \longmapsto [e/x]e_1$

RTE

Consider the rule
$$
\dfrac{e_1 \text{ : num} \phantom{“”}e_2\text{ : num}}{\text{div}(e_1;e_2)\text{ : num}}
$$
The expression $\text{div}(\text{num[114514]}; \text{num[0]})$ is well-typed but it stuck.

Two (not so practical) options:

  • Enhance the type system to eliminate such error
  • Add dynamic checks so division by zero signals an error

The main idea was to distinguish checked and unchecked errors.

Unchecked errors are errors can be ruled out by type system.

A method for modeling checked errors is inductively define the judgment $e \text{ err}$ stating that $e$ incurs a checked RTE.
$$
\dfrac{e \text { val}}{\text{div}(e;\text{num[0]}) \text{ err}}\\
\dfrac{e_1 \text{ err}}{\text{div}(e_1;e_2)\text{ err}}\\
\dfrac{e_1 \text{ val}\phantom{“”}e_2\text{ err}}{\text{div}(e_1;e_2)\text{ err}}
$$
We can also consider adding an expression error which forcibly induce an error with static
$$
\dfrac{}{\Gamma \vdash \text{error}: \tau}
$$
and dynamics
$$
\dfrac{}{\text{error} \text{ err}}
$$

Improved Type Safety Theorem

Preservative part is not affected.

Progress part is affected since we have to consider err.

If $e : \tau$ and either $e \text{ val}$, $e\text{ err}$ or $\exists e’$ such that $e \longmapsto e’$.