Gradual Typing [for category theorists]
golem.ph.utexas.edu
golem.ph.utexas.edu
The curry-howard isomorphism is the idea that formal logics and programming languages (usually typed lambda calculi) are so related that they're almost the same thing. There's a more elaborate version that creates a three-way correspondence between formal logic, programming languages and categories. The most well known correspondence goes like Intuitionistic Logic <=> Simply Typed Lambda Calculus <=> Cartesian Closed Categories (cf. [0]). In particular, the types of the programming language are the objects, and terms in the language with a given context are morphisms in the category: in `t : A -> B`, A is the context and B is the type of the term t, i.e. t can contain free variables of A, with a minor note [1].
Now, the programming languages being examined here have more structure than that. They handle this by considering internal categories. Usually categories are defined with sets of objects and sets of morphisms. Internal categories are such that there is some fancier structure on both. In this case, there is a relation "X is more dynamic than Y", for both types and terms. The definition isn't too hard of a leap from plain categories: The term composition operation should respect the dynamism relation.
A functor is a map between categories: It sends objects (types) to objects and sends morphisms (terms) to morphisms while respecting the algebra of categories, which corresponds to being compatible with term substitution for programming languages. Translating via curry-howard, a functor is a parametric construction of some sort: you can carry it out without knowing anything about the particulars of the term you're translating. Generics are a form of parametric construction, for example. `map` in various languages internalizes the compatibility with the construction.
A profunctor is a bit gnarlier, but it bears a similar relation to functors as relations do to functions. The prototypical profunctor is Hom(-, --), which is defined such that Hom(A, B) is the set of morphisms between objects A and B. In good situations, the data of a profunctor is equivalent to the data of a functor, much the same way that functions and cofunctions are special kinds of relations [2]. This situation is called a representable profunctor.
In really good situations, a profunctor can have two non-equivalent descriptions as a functor. In such a case the functors are specially related: They are adjoint [3]. Adjoint functors are constructions that are dual to each other in a technical sense which makes them really useful to calculate with. The upshot is that the data of the profunctor boils down to two fundamental parametric operations which are dual to each other.
In this case, "dynamism" boils down to two canonical operations: upcasting and downcasting. That's really intuitive, and the usefulness here is that the category theory has essentially captured this intuition while also stating exactly how upcasting / downcasting interact with terms, this is the part about "proarrow equipments". Turning intuition into a precise, technical tool is the core strength of category theory.
The conclusion is an application: Using this machinery to construct abstract models of the semantics of such a lanugage. I haven't read the details, but the post describes two semantics where type errors are the same as a diverging program, and one where they are different. The latter is interesting because there you could conceivably extend the semantics further to model exception handling for type errors.
[0] https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...
[1] What about multiple free variables in the term? The simplest way to handle contexts with multiple variables is to conflate them with contexts of a single cartesian product of values. In this construction, the authors are going all the way and fully distinguishing cartesian products inside the programming language from the idea of complex contexts, hence "virtual cartesian preorder categories".
[2] By cofunction I mean functions where the domain and the range have been swapped. Technically speaking, a profunctor can be represented either as Hom(f -, --) or Hom(-, f --) for a functor f.
A couple comments 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper. We basically showed that graduality + extensionality determines almost all of the behavior of casts. 2. Exception handling for type errors is actually in direct conflict with graduality. The reason is that the type error is the least element and every term has to be monotone with respect to the type error, so if you catch a type error, to be monotone you have to show that the result you produce is less dynamic than the result you would have produced if there was no exception. This means that if you want to catch type errors you need to have a fancy catch form, or you need to do it at an "extra-linguistic" level, or you can use modal types (think monads) to say that catching a type error is a "reflective" operation and so any code that does it is uses the reflection modality.
Also as a side-note, in my opinion profunctors are an essential component of category theory, and it's really a shame that in intro courses we explain everything in terms of adjunctions, limits, presheaves, etc when profunctors are ultimately simpler. They are unavoidable when you do enriched/internal category theory and they are more directly useful in designing type theories than adjunctions.
I think you accidentally a word.
Re 2: That makes sense to me. In Haskell any terms can contain exceptions but they can only be caught in IO.
I look forward to reading the paper this weekend! I started really appreciating profunctors when I first learned what an equipment was, they just seemed to make everything fall into place. One thing I find intriguing about your paper is that the equipment participates directly in the models of the type theory instead of being a way to relate different models ala formal category theory.
Perhaps the reason why profunctors aren't highlighted more often is the same prejudice that gives functions a more central place than relations.