The n-Category Café

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.