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:PolaritiesGround forms: $+$, $-$.Inversion: $+^\dagger = -$ and $-^\dagger = +$.VariancesGround forms: sets of polarities.Inclusion: set inclusion.Inversion: memberwise.KindsGround 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'$.TypesKinding:$\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.
Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking
type theory;lambda calculus