PFPL Chapter 4 Statics

Posted on In Disqus:

Please refer this link from page 35 to 40.

PL Phase Distinction

There are 2 phases defined in PLs:

  • Static
    • Parsing and Type Checking to ensure the program is well-formed.
  • Dynamic
    • Well-Behaved Execution of well-formed programs.

A language is said to be safe when well-formed and well-behaved execution are both achieved.

What about Static Phase

Static phase is specified by a statics comprising a set of rules for deriving type judgments stating that an expression is well-formed of a certain type.

Type safety tells us that the predictions about “some aspects of run-time safety by seeing that the types fit well in the program” is correct.

This note will use PFPL expression language E as example.

Syntax

In chapter 1 we realized about the concrete and abstract part of syntax. When defining a language we should primarily concerned with its abstract syntax specified by a collection of operators and their arities.

We might need a smallest set of concrete syntax for the sake of clarity, with syntax table
$$
\begin{aligned}
\text{Typ}&&\tau&&::=&&\text{num}&&\text{num}&&\text{numbers}\newline
&&&&&&\text{str}&&\text{str}&&\text{strings}\newline
\text{Exp}&&e&&::=&&x&&x&&\text{variables}\newline
&&&&&&\text{num}[n]&&n&&\text{numeral}\newline
&&&&&&\text{str}[s]&&\text{“s”}&&\text{literlal}\newline
&&&&&&\text{plus}(e_1;e_2)&&e_1 + e_2&&\text{addition}\newline
&&&&&&\text{times}(e_1;e_2)&&e_1 * e_2&&\text{multiplication}\newline
&&&&&&\text{cat}(e_1;e_2)&&e_1 \wedge e_2&&\text{concatenation}\newline
&&&&&&\text{len}(e)&&|e|&&\text{length}\newline
&&&&&&\text{let}(e_1;x.e_2)&&\text{let } x \text{ be }e_1\text{ in }e_2 &&\text{definition}
\end{aligned}
$$

Type System

Type system impose constraint on formations of phrases that are sensitive to the context where they occur.

The only information we require from context of an expression is the type of variables within whose scope the expression lies.

In this way the statics of E consists of an inductive definition of generic judgment with form like $\mathcal X | \Gamma \vdash e : \tau$ where

  • $\mathcal X$ is a finite set of variables
  • $\Gamma$ is typing context consisting of hypotheses of form $x : \tau$ with $x \in \mathcal X$

We write $x \notin dom(\Gamma)$ for there’s no assumption in $\Gamma$ of form $x : \tau$ for any type of $\tau$. So $x$ is fresh for $\Gamma$.

The type system for E has form
$$
\dfrac{}{\Gamma, x:\tau \vdash x:\tau}
$$

$$
\dfrac{}{\Gamma \vdash \text{str}[s]:\text{str}}
$$

$$
\dfrac{}{\Gamma \vdash \text{num}[n]:\text{num}}
$$

$$
\dfrac{\Gamma\vdash e_1:\text{num}\phantom{“”}\Gamma\vdash e_2:\text{num}}{\Gamma\vdash \text{plus}(e_1;e_2):\text{num}}
$$

$$
\dfrac{\Gamma\vdash e_1:\text{num}\phantom{“”}\Gamma\vdash e_2:\text{num}}{\Gamma\vdash \text{times}(e_1;e_2):\text{num}}
$$

$$
\dfrac{\Gamma\vdash e_1:\text{num}\phantom{“”}\Gamma\vdash e_2:\text{num}}{\Gamma\vdash \text{cat}(e_1;e_2):\text{num}}
$$

$$
\dfrac{\Gamma\vdash e:\text{str}}{\Gamma\vdash \text{len}(e):\text{num}}
$$

$$
\dfrac{\Gamma\vdash e_1:\tau_1\phantom{“”}\Gamma, x:\tau_1\vdash e_2:\tau_2}{\Gamma\vdash \text{let}(e_1;x.e_2):\tau_2}
$$

In the last rule, we tacitly assume that $x$ is not already declared in $\Gamma$.

This may always be true for $\alpha$-equivalence of let expression.

Lemma: Unicity of Typing

For every typing context $\Gamma$ and expression $e$, there exists at most one $\tau$ such that $\Gamma \vdash e : \tau$.

Lemma: Inversion of Typing

Suppose $\Gamma \vdash e:\tau$. If $e = \text{plus}(e_1;e_2)$, then $\tau = \text{num}$, $\Gamma \vdash e_1 : \text{num}$ and $\Gamma \vdash e_2: \text{num}$. It similarly applies to other constructs of the language.

Structural Properties

Lemma: Weakening

If $\Gamma \vdash e’: \tau’$, then $\Gamma, x:\tau \vdash e’ : \tau’$ for any $x \notin dom(\Gamma)$ and any type $\tau$.

Lemma: Substitution

If $\Gamma, x : \tau \vdash e’ : \tau’$ and $\Gamma \vdash e : \tau$, then $\Gamma \vdash [e/x]e’ : \tau’$.

Lemma: Decomposition

If $\Gamma \vdash [e/x]e’ : \tau’$, then for every type $\tau$ such that $\Gamma \vdash e : \tau$, we have $\Gamma, x : \tau \vdash e’: \tau’$.

Classification of Forms

  • Introduction: Determines the values or canonical forms of that type.
  • Elimination: How to manipulate the values of a type to form a computation of another type.

Exercises

4.1 and 4.2

According 4.1(a) and 4.2(a)
$$
\dfrac{}{\Gamma, e\uparrow\tau \vdash e\uparrow \tau}
$$

$$
\dfrac{}{\Gamma \vdash \text{num}[n] \downarrow \text{num}}
$$

$$
\dfrac{}{\Gamma \vdash \text{str}[n] \downarrow \text{str}}
$$
According to 4.1(b)
$$
\dfrac{\Gamma \vdash e \uparrow \tau}{\Gamma \vdash e \downarrow \tau}
$$
According to 4.2(b)
$$
\dfrac{\Gamma \vdash e_1 \downarrow \text{num}\phantom{“”}\Gamma \vdash e_2 \downarrow \text{num}}{\Gamma \vdash \text{plus}(e_1;e_2) \uparrow \text{num}}
$$

$$
\dfrac{\Gamma \vdash e_1 \downarrow \text{num}\phantom{“”}\Gamma \vdash e_2 \downarrow \text{num}}{\Gamma \vdash \text{times}(e_1;e_2) \uparrow \text{num}}
$$

$$
\dfrac{\Gamma \vdash e_1 \downarrow \text{str}\phantom{“”}\Gamma \vdash e_2 \downarrow \text{str}}{\Gamma \vdash \text{cat}(e_1;e_2) \uparrow \text{str}}
$$

$$
\dfrac{\Gamma \vdash e \downarrow \text{str}}{\Gamma \vdash \text{len}(e) \uparrow \text{num}}
$$
According to 4.2(c)
$$
\dfrac{\Gamma \vdash e \downarrow \tau}{\Gamma \vdash \text{cast}\{\tau\}(e) \uparrow \tau}
$$
According to 4.2(d)
$$
\dfrac{\Gamma \vdash e_0 \uparrow \tau_0 \phantom{“”} \Gamma, x \uparrow \tau_0 \vdash e_1 \downarrow \tau}{\Gamma \vdash \text{let}(e_0;x.e_1)\downarrow \tau}
$$