It is well known that adding unrestricted kind polymorphism to the higher-order polymorphic lambda calculus, a.k.a. System \(F_\omega\), leads to logically inconsistent paradoxes. For those in dependently typed theorem proving community, this is non of their concern, since dependently typed proof assistants are usually based on predicative calculus with stratified universes. However, there is an alternative approach that has not been well explored yet.

Consider taking an alternative approach of starting from a more traditional functional language based on impredicative polymorphism and turning that into a theorem proving system. For instance consider a certain subset of Haskell with GHC extensions such as `RankNTypes`

and `ImpredicativeTypes`

(after all, core of GHC is an extension of \(F_\omega\) ), and trying to carve out a logically consistent language. This is exactly the motivation of my Ph.D. thesis, and its resulting artifact is the Nax language. To make the long story short, we should be able to have a logically consistent subset of say Haskell with GHC extension including `GADTs`

and `PolyKind`

. The benefit of such design is that we can reuse all the facilities that have already been built around functional languages like Haskell, which has far more sophisticated and well-optimized compilers than most theorem proving systems.

If we take this route, we should figure out a safe way to extend impredicative polymorphism with a restricted form of kind polymorphism. I believe that extending \(F_\omega\) with Rank 1 polymorphic kind bindings for finite number of globally defined type constructor variables is safe. That is, the resulting calculus with this extension is logically consistent. Proof of logical consistency of this extended calculus should be quite straightforward by mapping the extended calculus back into \(F_\omega\) by inlining.

Here is the syntax of the extended calculus: $$ \sigma ::= \kappa \mid \forall \chi.\kappa $$ $$ \kappa ::= \chi \mid * \mid \kappa \to \kappa’ $$ $$ A, B, F, G ::= X \mid A \to B \mid \lambda X^{\kappa}.F \mid F~G \mid \forall X^{\kappa}.B $$ $$ \Sigma ::= \cdot \mid T^\sigma,\Sigma $$ $$ \Gamma ::= \cdot \mid X^{\kappa} \mid x:A $$ $$ t, r, s ::= x \mid \lambda x.t \mid r~s $$

A type constructor name \(T\) is no different than a type variable \(X\). It is just a notional convention to emphasize that the variable stands for a globally defined name for a type constructor. From a list of globally defined type constructors \( T_1 = F_1, T_2 = F_2, \ldots, T_n = F_n \) a global context \(\Sigma\) can be obtained such that \(\Sigma = T_1^{\sigma_1}, T_2^{\sigma_2}, \ldots, T_n^{\sigma_n}\) Each \(\sigma_i\) is a polymorphic kind of \(F_i\). For instance, the polymorphic kind scheme of \(F_1 = \lambda X^{\chi}.X\) is \(\sigma_1 = \forall \chi.\chi \to \chi\).

For simplicity, let us consider just one global definition where \(T_1 = F_1\). Assuming \(F_1\) is well kinded, we get \(\Sigma = T_1^{\sigma_1]}\). In the derivation tree of a typing judgment \(T_1^{\sigma_1};\Gamma \vdash t : A\), we inline each occurrence of \(T_1\) with an instantiation of its definition \(F_1\), instantiating all the free kind variables in \(F_1\) appropriately for each occurrence. For instance, if we had \(F_1 = \lambda X^{\chi}.X\), we might instantiate it to \(\lambda X^{*}.X\), \(\lambda X^{ * \to * }.X\), or any appropriate instantiation of \(\chi\) as needed. Once we have inlined every occurrence of \(T_1\), the global context \(\Sigma\) becomes irrelevant. Therefore, we can simply ignore \(\Sigma\), and the resulting derivation tree is exactly the derivation tree for a typing judgment in \(F_\omega\).

Generalizing the inlining for \(n\) definitions is not so hard. The only additional thing to consider is that the previously defined type constructor names can be used in the latter definitions. Consider \(T_1 = F_1, T_2 = F_2, \ldots, T_n = F_n\). The first name \(T_1\) can appear in any of \(F_2, \ldots, F_n\). So, inlining should be performed in a cascading manner starting from \(T_1\), inlining inside \(\Sigma\) as well as other parts of the derivation tree.

Next step is to generalize this idea for System \(F_i\) which extends System \(F_\omega\) with erasable type indices. Here, this will get more complicated because type variables and term-index variables can appear in kinds as well as kind variables.