17
$\begingroup$

Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type theory -- it seems like this has not been explored very much, if at all.

In general, adding coercive subtyping to a type theory does not ruin its meta-theoretic properties such as strong normalization, so its categorical semantics should be something of actual interest, I think!

$\endgroup$
17
$\begingroup$

Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of coherence: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the program?

One of the first treatments of this issue was John Reynolds' 1980 paper, Using Category Theory to Design Implicit Conversions and Generic Operators, which shows how you can give a categorical semantics to a system of coercions and use it to ensure that it is coherent.

If you're interested in coercive subtyping for rich (e.g., dependent) type theories, then Zhaohui Luo is the go-to guy.

$\endgroup$
  • $\begingroup$ The John Reynolds paper looks great, thanks! (I've heard Philip Wadler once said that John Reynolds tends to be about 10 years ahead of time in research...) I actually am familiar with Zhaohui Luo, but what I've read from him seemed to primarily be working just with type theory and not exploring the other angles. $\endgroup$ – Darius Jahandarie Apr 18 '13 at 13:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.