# Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking

I need an extension of System $F_\omega$ with subtyping, and where the variance of type constructors is reflected in their kind. Unfortunately, System $F^\omega_{<:}$, as defined in chapter 31 of Pierce's Types and Programming Languages, doesn't address the latter requirement, so I decided to roll my own.

Here is the list of additions to $F_\omega$'s I've made so far:

## Polarities

• Ground forms: $+$, $-$.

• Inversion: $+^\dagger = -$ and $-^\dagger = +$.

## Variances

• Ground forms: sets of polarities.

• Inclusion: set inclusion.

• Inversion: memberwise.

## Kinds

• Ground forms: $\Omega/V$ and $K \rightarrow K'$.

• Inclusion:

• Given $V_1 \subseteq V_2$, we can derive $\Omega/V_1 \subseteq \Omega/V_2$.

• Given $K_2 \subseteq K_1$ and $K_1' \subseteq K_2'$, we can derive $K_1 \rightarrow K_1' \subseteq K_2 \rightarrow K_2'$.

## Types

• Kinding:

• $\Gamma \vdash \top, \bot : \Omega/V$.

• $\Gamma \vdash (\rightarrow) : \Omega/V^\dagger \rightarrow \Omega/V \rightarrow \Omega/V$.

• The remaining rules are as one would expect.

• Inclusion:

• Given $\Gamma \vdash T : \Omega/V$ and $\{+\} \subseteq V$, we can derive $\Gamma \vdash \bot \subseteq T \subseteq \top : \Omega/V$.

• Given $\Gamma \vdash T : \Omega/V$ and $\{-\} \subseteq V$, we can derive $\Gamma \vdash \top \subseteq T \subseteq \bot : \Omega/V$.

• Given $\Gamma \vdash T_1, T_2 : \Omega/\{+,-\}$, we can derive $\Gamma \vdash T_1 \subseteq T_2 : \Omega/\{+,-\}$.

• The remaining rules are as one would expect.

And here I ran out of imagination. Now I have the following questions:

• Is what I've sketched so far sound? What sanity checks can I use to make sure I'm not doing something wrong? Perhaps something akin to automated testing in computer programming?

• A type system with polymorphism and subtyping must have bounded quantification. How hard should it be to add?

• A very important desideratum in type systems with subtyping is that the inhabitants of each kind form a lattice. How hard should it be make sure that each kind is a lattice?

• What's the most convenient tool for mechanizing formal systems like the one I sketched? Preferably, I'd like a library or framework that already does the “boring stuff”, like implementing variable substitution and handling contexts.

• What do $\Omega$ and $V$ range over? – Martin Berger May 1 '16 at 6:34
• @MartinBerger: $V$ ranges over variances. $\Omega$ doesn't range over anything: $\Omega/V$ means “a proper type (as opposed to a type operator) that can be used with $V$-variantly”. – pyon May 1 '16 at 6:37
• @MartinBerger: As for individual variances, $\emptyset$ means “invariant” (the type can appear in both covariant and contravariant position), $\{+\}$ means “covariant” (the type can't appear in contravariant position), $\{-\}$ means “contravariant” (the type can't appear in covariant position” and $\{+,-\}$ means “bivariant” (the type can't be used at all). – pyon May 1 '16 at 6:38
• Do you intend that subtyping and subkinding are related? – Martin Berger May 3 '16 at 15:36
• @MartinBerger: Yes. For instance, if I Church-encode Nat and Pos (TaPL p. 398-399), then Pos is a subtype of Nat at $\Omega/\{+\}$ (as expected), but Nat is a subtype of Pos at $\Omega/\{-\}$ (contravariance flips the subtype relation), and both are subtypes of each other at $\Omega/\{+,-\}$. More generally, if $K_1 \subsetneq K_2$, there will be types $T_1, T_2 : K_1$ such that $T_1 \not\subseteq T_2 : K_1$ but $T_1 \subseteq T_2 : K_2$. – pyon May 3 '16 at 17:56