4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ What do $\Omega$ and $V$ range over? $\endgroup$ – Martin Berger May 1 '16 at 6:34
  • $\begingroup$ @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”. $\endgroup$ – pyon May 1 '16 at 6:37
  • $\begingroup$ @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). $\endgroup$ – pyon May 1 '16 at 6:38
  • $\begingroup$ Do you intend that subtyping and subkinding are related? $\endgroup$ – Martin Berger May 3 '16 at 15:36
  • $\begingroup$ @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$. $\endgroup$ – pyon May 3 '16 at 17:56

Your Answer

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

Browse other questions tagged or ask your own question.