Gradual Typing in Adelfa
Introduction
Gradual Typing is a type system that marries static and dynamic typing. It was
developed in 2006 by Jeremy Siek and Walid Taha. Dynamic type systems offer
complete flexibility and agility; whereas static typing offers type-related
error detection earlier. Gradual typing allows us to declare types as dynamic
and also specify types. Moreover, we can coerce types to and from dynamic
throughout its execution.
I won't be going over Gradual Typing too closely, because Professor Siek has his own blog you should give a read if you're interested. This blog post will focus more on mechanizing some properties of gradual typing in Adelfa, a system I'm currently using as a graduate student. I plan showing more about Adelfa in a later post, so I'll just be showing a general thought process involved in the construction of these theorems. I'll focus on Gradual Typing for Functional Languages for this post.
Syntax of The Language
We elide variables, ground types, constants, etc. since they are not of interest in any theorems we will mechanize. The paper describes the syntax of \(e \in \lambda^{?}_{\rightarrow}\) in section 1. I'll show the paper's description as one column and the formulation in Adelfa in the other.
Gradual Typing Syntax | Adelfa Signature | |
---|---|---|
Type | \(\tau\) | ty : type. |
Function Type | \(\tau \rightarrow \tau\) | arr: {t1: ty}{t2:ty} ty. |
Expressions | \(e\) | tm : type. |
Application | \(e \cdot e\) | app: {tm1: tm}{tm2: tm} tm. |
Abstraction | \(\lambda x:\tau . e\) | lam: {ty1:ty}{D: {x:tm} tm} tm. |
We also define a few extra items in Adelfa:
-
unit
andnat
, essentially placeholders to represent more meaningful types in an actual system. -
dyn
which will represent the \(?\) / \(\star\) type, standing for dynamic. -
empty
andz
which will be terms we can use of typeunit
andnat
respectively.
We could use this and then define a system to insert the casts like in the paper, but I'll only be dealing with the intermediate language of \(\lambda^{\langle \tau \rangle}_{\rightarrow}\) for simplicity. Therefore, we'll define the cast as well. In the paper this is written as \(\langle \tau \rangle e\) where we are casting \(e\) to the target type \(\tau\).
Here is the Adelfa section in its entirety:
|
|
Type Consistency
For a cast to occur between types, the types must be consistent. Consistency is shown through a \(\sim\), so \(\tau_{1} \sim \tau_{2}\) is a relation accepting two types. Here are all the rules for consistency as given in the paper:
-
CRefl \begin{equation} \tau \sim \tau \end{equation}
-
CUnr \begin{equation}\label{cunr} \tau \sim ? \end{equation}
-
CUnl \begin{equation}\label{cunl} ? \sim \tau \end{equation}
-
CFun \begin{equation} \frac{ \sigma_{1} \sim \tau_{1} \quad \sigma_{2} \sim \tau_{2} }{ \sigma_{1} \rightarrow \sigma_{2} \sim \tau_{1} \rightarrow \tau_{2} } \end{equation}
These can be encoded into Adelfa by first defining a consistency relation that
accepts two types, then we will define each rule based on the input types. Any
conditions that need to be met by the rule can be realized through some
derivation as seen in the consis-fun
rule.
|
|
Now that we have the LF signature finished for the consistency relation, we can prove properties about it. Let's prove all the points mentioned in Proposition 1.
-
\(\tau \sim \tau\): the relation is symmetric
-
If \(\sigma \sim \tau\) then \(\tau \sim \sigma\): the relation is commutative.
-
\(\neg (\forall \tau_{1} \tau_{2} \tau_{3} . \tau_{1} \sim \tau_{2} \land \tau_{2} \sim \tau_{3} \longrightarrow \tau_{1} \sim \tau_{3})\): the relation is not transitive.
Symmetry
This arises very naturally from our consis-refl
rule. So naturally that to prove
it is essentially unnecessary. Nevertheless, here is the proof.
|
|
Commutativity
The only tricky aspect of this proof is applying the inductive hypothesis in the case that it is a function type. The other cases are commutative by the \(?\) being on one side or having the same type on both.
|
|
Non-transitivity
We don't have the not (\(\neg\)) operator, but that's not a problem. We can prove that it doesn't hold in every case by posing an existential that would lead to a false assertion. Therefore, we'll formulate the following:
\begin{equation} \exists \tau_{1} \tau_2 \tau_3 . \tau_1 \sim \tau_2 \land \tau_2 \sim \tau_3 \implies \tau_1 \sim \tau_3 \implies \bot \end{equation}
The transitivity in consistency doesn't work in the case that \(\tau_{2}\) is
\(?\) and \(\tau_1 \not\equiv \tau_3\). Hence, why we cannot prove this with
only unit
type constructively.
|
|
We have to be careful about this theorem in particular. We could similarly prove false in this situation if \(\tau_{1} \not\sim \tau_{2}\) or \(\tau_2 \not\sim \tau_{3}\). In our case, \(() \sim ?\) and \(? \sim \mathbb{N}\), and clearly \(() \not \sim \mathbb{N}\), so case analysis will yield \(\bot\) but only because \(\tau_1 \not \sim \tau_3\) - and we've shown the property that we'd like to.
Typing Relations
We'll translate Figure 6's typing derivations for \(\lambda^{\langle \tau \rangle}_{\rightarrow}\) into Adelfa piece by piece. Just as before, we'll place any preconditions of the relation into some derivation necessary for the relation to hold.
-
Type System \begin{equation} \Gamma \vert \Sigma \vdash e : \tau \end{equation}
1
of : {t1: tm}{ty1 : ty} type.
-
TLam \begin{equation} \frac{ \Gamma (x \mapsto \sigma) \vert \Sigma \vdash e : \tau }{ \Gamma \vert \Sigma \vdash \lambda x : \sigma . e : \sigma \rightarrow \tau } \end{equation}
1 2 3
of-lam : {t1:{x:tm}tm}{ty1:ty}{ty2:ty} {D:{x:tm}{D': of x ty1} of (t1 x) ty2} of (lam ty1 ([x] t1 x)) (arr ty1 ty2).
-
TApp \begin{equation} \frac{ \Gamma \vert \Sigma \vdash e_{1} : \tau \rightarrow \tau^{\prime} \quad \Gamma \vert \Sigma \vdash e_2 : \tau }{ \Gamma \vert \Sigma \vdash e_1 e_2 : \tau^{\prime} } \end{equation}
1 2 3 4
of-app : {t1: tm}{t2:tm}{ty1: ty}{ty2:ty} {D1: of t1 (arr ty1 ty2)} {D2: of t2 ty1} of (app t1 t2) ty2.
-
TCast \begin{equation} \frac{ \Gamma \vert \Sigma \vdash e : \sigma \quad \sigma \sim \tau }{ \Gamma \vert \Sigma \vdash \langle \tau \rangle e : \tau } \end{equation}
1 2 3 4
of-cast : {t1: tm}{ty1: ty}{ty2: ty} {D1: of t1 ty2} {D: consis ty1 ty2} of (cast ty2 t1) ty2.
In addition, the the typing derivations listed in the paper, we have to add ones
for the new terms empty
and z
that we've derived.
-
Empty \begin{equation} \frac{} { \Gamma \vert \Sigma \vdash \langle \rangle : () } \end{equation}
1
of-empty : of empty unit.
-
z \begin{equation} \frac{} { \Gamma \vert \Sigma \vdash 0 : \mathbb{N} } \end{equation}
1
of-z : of z nat.
Context Lemmas & Type Equality
To translate this into Adelfa, we need to account for abstraction capturing a
variable in the context. Adelfa addresses this problem through a context
schema. In this instance we define it as Schema c := {T}(x: tm, y: of x T)
.
We also don't have a built-in way to determine type equality, we we'll define one. It turns out, equality by reflexivity is sufficient for our needs.
|
|
These are not relating directly to gradual typing, but are more properties of any typing relation. Firstly, a type in a context is also a type not in a context: \(\Gamma \vdash \tau \implies \varnothing \vdash \tau\).
|
|
Secondly, type equality also doesn't depend on a context: \(\Gamma \vdash \tau = \tau^{\prime} \implies \varnothing \vdash \tau = \tau^{\prime}\).
|
|
Type Uniqueness
Let's look at Lemma 2.
\begin{equation} \Gamma \vert \Sigma \vdash e : \tau \land \Gamma \vert \Sigma \vdash e : \tau^{\prime} \implies \tau = \tau^{\prime} \end{equation}
We then translate this into Adelfa as such
|
|
Which is:
\begin{equation} \Gamma \vert \Sigma \vdash e : \tau \land \Gamma \vert \Sigma \vdash e : \tau^{\prime} \implies \Gamma \vert \Sigma \vdash \tau = \tau^{\prime} \end{equation}
So, to take the context off of the consequent, we only have to apply our equality independent lemma.
|
|
Preservation
Stated simply, "reduction preserves types" is the principle we want to prove. We need a reduction strategy. The paper uses big step semantics, but I'll use small step which will display the next step that a term will take. These steps will occur until we reach a value. We define values to be:
-
Lambdas: \(\lambda x : \tau . e\)
-
Casts: \(\langle \tau \rangle e\)
-
Empty: \(\langle \rangle\)
-
Zero: \(0\)
|
|
We then have to define how our program will actually execute through the lambda terms. I'll use the single step notation of \(e \rightsquigarrow e^{\prime}\) to denote that \(e\) reduces to \(e^{\prime}\) in a single step. We define a set of reduction rules such that we know the exact reduction step the program will take at any moment. For example, if we have two lambda terms \(e_1\) and \(e_2\) being applied, \(e_1 \cdot e_2\), then we could reduce the left \(e_{1} \rightsquigarrow e_1^{\prime}\) or the right \(e_{2} \rightsquigarrow e_2^{\prime}\), or it could be the tricky case that \(e_1\) is of function type \(\sigma_1\rightarrow\sigma_2\) and needs to be expanded into a lambda term. We solve this issue by using the following order:
-
Reduce the left side until it is a value.
-
Reduce the right side until it is a value.
-
If the left side has a cast, we can remove it.
-
Expand the left side into a lambda abstraction.
These are captured in the following definitions:
|
|
Which captures all \(t1 \rightsquigarrow t2\) relations. The precision in which
we defined step
will come in handy when we move onto proving progress.
Before we move onto preservation, let's prove a corollary that states values cannot take any more steps.
|
|
This isn't necessary for proving preservation, but is a nice way to confirm our
internal idea of what a value
is. Looping back to preservation, we can prove
this without too much difficulty.
|
|
Progress
Progress states that when we are evaluating a term, are able to either take a step or we have reached a value. Progress and preservation together constitute "type-safety" of a system. We've already defined values and steps we can take within our language, so proving progress doesn't require too much more information.
The only new definitions we need are that of a canonical form. Well typed values have to be in a canonical form. When we have reached a point where we have \(e_1 \cdot e_2\), we want to limit the forms of \(e_1\) to ones where \(e_1\) is a cast \(\langle \tau_1 \rightarrow \tau_2 \rangle e_1\) or of function type, and can be expanded into a lambda \(e_1 : \tau_1 \rightarrow \tau_2 \Rightarrow (\lambda x : \tau_1 . e_1^{\prime}) : \tau_2\). Any other form for \(e_1\) would not lead to a well typed term. We want to list all canonical forms:
|
|
And formulate a theorem about well typed values being canonical:
|
|
We're now able to prove progress.
|
|