### Gradual Typing

#### Posted by Mike Shulman

*(Guest post by Max New)*

Dan Licata and I have just put up a paper on the arxiv
with a syntax and semantics for a *gradually typed* programming
language, which is a kind of synthesis of statically typed and
dynamically typed programming styles.
The central insight of the paper is to show that the dynamic type
checking used in gradual typing has the structure of a proarrow
equipment.
Using this we can show that some traditional *definitions* of dynamic
type checks can be proven to be in fact *unique solutions* to the
specifications provided by the structure of an equipment.
It’s a classic application of category theory: finding a universal
property to better understand what was previously an ad-hoc
construction.

The paper is written for computer scientists, so I’ll try to provide a more category-theorist-accessible intro here.

#### Dynamic Typing

First, a very brief introduction to what dynamic typing is. To put it very simply, dynamically typed languages are languages where there is only one type, the “dynamic type” which I’ll call $?$ (more details here). They have the same relationship to typed languages that monoids do to categories or operads to multicategories. So for example, in a dynamically typed language the function application rule looks like

$\frac{\Gamma \vdash t : ?\,\, \Gamma \vdash u : ?}{\Gamma \vdash t(u) : ?}$

That is, it *always* type-checks, whereas in a typed language the $t$
above would need to be of a function type $A \to B$ and $u$ would have
to be of type $A$.
However, these languages are not like the pure untyped lambda calculus
where everything is a function: they will also include other types of
data like numbers, pairs, strings etc.
So whereas in a statically typed language the syntax $3(3)$ would be
rejected at type-checking time, we can think of the dynamic language
as *delaying* this type error until run-time, when the program $3(3)$
will crash and say “3 is not a function”.
This is implemented essentially by representing a value in the dynamic
language as an element of a coproduct of all the primitive types in
the language.
Then $3$ becomes $(number, 3)$ and the implementation for the function
application form will see that the value is not tagged as a function
and crash.
On the other hand if we have an application $(function, \lambda
x. t)((number, 3))$ the implementation will see that the tag is a
function and then run $t[(number,3)/x]$, which may itself raise a
dynamic type error later if $t$ uses its input as a pair, or a
function.

So with all that ugliness, why do we care about these languages? Well
it is very *easy* to write down a program and *just run it* without
fighting with the type checker. Anyone who’s had to restructure their
coq or agda program to convince the type checker that it is
terminating should be able to relate here.
Furthermore, even if I do think these languages are ugly and awful it
is a fact that these languages are extremely popular: JavaScript,
Python, Perl, Ruby, PHP, LISP/Scheme are all used to write real
working code and we certainly *don’t* want to chuck out all of those
codebases and laboriously rewrite them in a typed language.

#### Gradual Typing

Gradually typed languages give us a better way: they embed the dynamic language in them, but we can also program in a statically typed style and have it interoperate with the dynamically typed code. This means new code can be written in a statically typed language while still being able to call the legacy dynamically typed code without having to sacrifice all of the benefits of static typing.

To a first approximation, a gradually typed language is a statically typed language with dynamic type errors, a distinguished dynamic type $?$ and a distinguished way to coerce values from any type to and from the dynamic type (possibly causing type errors). Then a dynamically typed program can be compiled to the gradual language by translating the implicit dynamic type checking to explicit casts.

For a gradually typed language to deserve the name, it should be on
the one hand *typed*, meaning the types have their intended
categorical semantics as products, exponentials, etc and on the other
hand it should satisfy *graduality*.
Graduality of a language means that the transition from a very loose,
dynamic style to a precise, statically typed style should be as smooth
as possible.
More concretely, it means that changing the types used in the program
to be less dynamic should lead to a *refinement* of the program’s
behavior: if the term satisfies the new type, it should behave as
before, but otherwise it should produce a dynamic type error.

We can formalize this idea by modeling our gradually typed language as
a category *internal to preorders*: types and terms have related
“dynamism” orderings (denoted by $\sqsubseteq$) and all type and term
constructors are monotone with respect to these orderings.
Then we can characterize the dynamic type as being the most dynamic
type and the type error as a least dynamic term of each type.
Making everything internal to preorders reproduces exactly the rules
of type and term dynamism that programming language researchers have
developed based on their operational intuitions.

We can then make a simple logic of type and term dynamism that we call “Preorder Type Theory”. Since we are doing cartesian type theory, it is the internal logic of virtually cartesian preorder categories, rather than plain preorder categories due to the structure of contexts. In the paper I present VCP categories by a direct definition, but behind the scenes I used Crutwell-Shulman’s notion of normalized T-monoid to figure out what the definition should be.

#### Casts and Equipments

While preorder type theory can express the basic ideas of a dynamic
type and type errors, the key ingredient of gradual typing that we are
missing is that we should be able to *cast* terms of one type to
another so that we can still program in a dynamically typed style.

Gradually typed languages in the literature do this by having a cast form $\langle B \Leftarrow A\rangle t$ in their language whose semantics is defined by induction on $A,B$. Our approach is to carve out 2 subsets of these casts which have universal properties with respect to the preorder category structure, which are the upcasts $\langle B \leftarrowtail A\rangle t$ and downcasts $\langle A \twoheadleftarrow B\rangle u$ which can only be formed when $A \sqsubseteq B$. Then one of those “oblique” casts can be defined using the dynamic type: $\langle B \Leftarrow A\rangle t = \langle B \twoheadleftarrow ?\rangle \langle ? \leftarrowtail A\rangle t$.

What universal property do the upcasts and downcasts have? Well, first we notice that term dynamism gives a relational profunctor between terms of type $A$ and type $B$ (i.e. a relation that is monotone in $B$ and antitone in $A$). Then we characterize the upcast and downcast as left- and right-representables for that profunctor, which consequently means the upcast is left adjoint to the downcast. More explicitly, this means for $t : A, u : B$ we have $\langle B \leftarrowtail A\rangle t \sqsubseteq u \iff t \sqsubseteq u \iff t \sqsubseteq \langle A \twoheadleftarrow B\rangle u$

By uniqueness of representables, this defines the upcasts and
downcasts uniquely up to order-equivalence, giving us a
*specification* for the casts.
We show that this specification, combined with the monotonicity of all
the term connectives and the $\beta,\eta$ rules of the connectives
allow us to derive the standard implementations of these casts as the
unique solutions to this specification.

If you’re familiar with equipments this structure should look
familiar: it gives a *functor* from the thin category ordering the
objects to the category of adjunctions in the term category.
This is a special case of a proarrow equipment where we view our
preorder category as a “vertically thin” double category.
So we extend our syntax to be the internal logic of vertically thin
cartesian preorder categories that are equipments, and can model type
error, dynamic type, functions and products and we call that system
“Gradual Type Theory”.
Then in that syntax we give some synthetic proofs of the uniqueness
theorems for the casts and a few other theorems about equipments with
certain universal properties.

#### Constructing Models

Finally, we give a construction for models of gradual type theory that extends Dana Scott’s classical models of dynamic typing to gradual typing. This connects our semantics to previous programming languages approaches and proves consistency for the system.

Briefly, we start with a locally thin 2-category $C$ (such as the
category of domains) and construct an equipment by defining the
vertical arrows to be *coreflections* in $C$, which are adjunctions
where the right adjoint is a retract of the left. Then we pick an
object $d$ in $C$ and take a kind of vertical slice category $C/d$. So
the objects are coreflections into $d$ and the vertical arrows are
commuting triangles of coreflections.

We use coreflections rather than just adjunctions for 2 reasons: first
a sociological reason is that the casts people have developed are
coreflections, and second a technical reason is that every
coreflection is a monomorphism and so when we take the slice category
we get a thin category and so our double category becomes a preorder
category. This allows us to interpret type and term dynamism as
*orderings* rather than a more complex category structure.

We then show how Dana Scott’s domain theoretic models of dynamic typing extend to a model of gradual type theory (where the type error is a diverging program) and another model where the type error and diverging program are different.

## Re: Gradual typing

A naive question. Is gradual typing in any way related to the casts we are used to in DTT, e.g. coercions, type classes, canonical structures, … ?

A more practical question, which of the graduately typed languages is closest to your type theory?