<p>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_{&lt;:}$, as defined in chapter 31 of Pierce's <em>Types and Programming Languages</em>, doesn't address the latter requirement, so I decided to roll my own.</p>

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

<h2>Polarities</h2>

<ul>
<li><p><strong>Ground forms:</strong> $+$, $-$.</p></li>
<li><p><strong>Inversion:</strong> $+^\dagger = -$ and $-^\dagger = +$.</p></li>
</ul>

<h2>Variances</h2>

<ul>
<li><p><strong>Ground forms:</strong> sets of polarities.</p></li>
<li><p><strong>Inclusion:</strong> set inclusion.</p></li>
<li><p><strong>Inversion:</strong> memberwise.</p></li>
</ul>

<h2>Kinds</h2>

<ul>
<li><p><strong>Ground forms:</strong> $\Omega/V$ and $K \rightarrow K'$.</p></li>
<li><p><strong>Inclusion:</strong></p>

<ul>
<li><p>Given $V_1 \subseteq V_2$, we can derive $\Omega/V_1 \subseteq \Omega/V_2$.</p></li>
<li><p>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'$.</p></li>
</ul></li>
</ul>

<h2>Types</h2>

<ul>
<li><p><strong>Kinding:</strong></p>

<ul>
<li><p>$\Gamma \vdash \top, \bot : \Omega/V$.</p></li>
<li><p>$\Gamma \vdash (\rightarrow) : \Omega/V^\dagger \rightarrow \Omega/V \rightarrow \Omega/V$.</p></li>
<li><p>The remaining rules are as one would expect.</p></li>
</ul></li>
<li><p><strong>Inclusion:</strong></p>

<ul>
<li><p>Given $\Gamma \vdash T : \Omega/V$ and $\{+\} \subseteq V$, we can derive $\Gamma \vdash \bot \subseteq T \subseteq \top : \Omega/V$.</p></li>
<li><p>Given $\Gamma \vdash T : \Omega/V$ and $\{-\} \subseteq V$, we can derive $\Gamma \vdash \top \subseteq T \subseteq \bot : \Omega/V$.</p></li>
<li><p>Given $\Gamma \vdash T_1, T_2 : \Omega/\{+,-\}$, we can derive $\Gamma \vdash T_1 \subseteq T_2 : \Omega/\{+,-\}$.</p></li>
<li><p>The remaining rules are as one would expect.</p></li>
</ul></li>
</ul>

<p>And here I ran out of imagination. Now I have the following questions:</p>

<ul>
<li><p>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?</p></li>
<li><p>A type system with polymorphism and subtyping must have bounded quantification. How hard should it be to add?</p></li>
<li><p>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?</p></li>
<li><p>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.</p></li>
</ul>

CC BY-SA 3.0
2016-05-01T06:34:29.900Z
What do $\Omega$ and $V$ range over?
Martin Berger
CC BY-SA 3.0
2016-05-01T06:37:07.223Z
@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”.
isekaijin
CC BY-SA 3.0
2016-05-01T06:38:52.910Z
@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).
isekaijin
CC BY-SA 3.0
2016-05-03T15:36:07.587Z
Do you intend that subtyping and subkinding are related?
Martin Berger
CC BY-SA 3.0
2016-05-03T17:56:00.263Z
@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$.
isekaijin
CC BY-SA 3.0
2016-05-03T18:51:12.233Z
@MartinBerger: I have a hunch that explicitly tracking variances could fix the problems that arise when combining polymorphism and subtyping, like the non-existence of joins and meets. If this alone doesn't fix it, then I might also need to extend kinding contexts, so that type variables are bounded both by above and below.
isekaijin
<type-theory><lambda-calculus>
Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking
isekaijin
# Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking

(Asked by: username_0 on 2016-04-28)

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.

**Tags:** type-theory, lambda-calculus
> **Comments:**
> **username_1**: What do $\Omega$ and $V$ range over?  
> **username_0**: @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”.  
> **username_0**: @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).  
> **username_1**: Do you intend that subtyping and subkinding are related?  
> **username_0**: @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$.  
> **username_0**: @MartinBerger: I have a hunch that explicitly tracking variances could fix the problems that arise when combining polymorphism and subtyping, like the non-existence of joins and meets. If this alone doesn't fix it, then I might also need to extend kinding contexts, so that type variables are bounded both by above and below.  

---

## 0 answers

