[TYPES] Literature relating subtyping to positivity checking for recursive types?

[Gabriel Scherer]

Dear Christopher,

I would say that the observations you have made hold in many systems
(and are well-understood), but that their usefulness, in reducing one
problem into the other, highly depends on the pragmatics of the
specific system you are working on. In most cases, my intuition is
that the *converse* transformation to the one you highlight is more
convenient, so it is an interesting observation if you can demonstrate
that Cedille goes against the grain on that topic -- as well.

1. (Cast S T) can be defined/derived in many systems. For example, if
you have definitional subtyping, (t : S <: T) being the coercion of
(t : S) into a T when (S <: T) holds, and a propositional equality,
you can define

    Cast S T := Sigma (f : S -> T). (f = lambda (x : S). (x : S <: T))

I would expect that, in most system, using a subtyping judgment
directly is more convenient that searching for inhabitants of
Cast. NuPRL (where I expect that you can just write (f = lam x. x))
might be a place to look for the converse phenomenon.


2. I think that the direct relation between fixpoints and positivity
(and monotonicity) is well-known, but then again, I expect that in
most cases it is simpler to establish a property such as
(F : * -{+}-> *) by reasoning on the structure of F than a relational
property such as (A <: B).

For an example of direct connection between positivity-in-fixpoints
and positivity-for-subtyping, see the relation between

  Fixed Points of Type Constructors and Primitive Recursion
  Abel and Mattes, 2004

and

  Polarized Subtyping for Sized Types
  Abel, 2006

The latter has a system for subtyping in F-omega (arrow kinds (k ->
k') are extended to have a variance (k -{v}-> k'), typically v \in
{+, -}) which directly extends the former's system to check positivity
for fixpoint types.

I think it makes sense to call (F : k) the "structural" approach, and
(F X <: F Y) the "relational" approach to establish positivity.

Most developments of the "structural" approach and its meta-theory
contain a proof that structural judgments imply relational judgments:
if you prove (F : * -{+} -> *), then for any (X <: Y) you have (F X <:
F Y). (In the polarized presentation above the presentation is
slightly different and I like it: if you prove (G |- A : +), then (g
<: g' : G) implies (A[g] <: A[g'])).

Conversely, many works on subtyping prove inversion lemmas on the
subtyping judgment (often used to define an "algorithmic" subtyping
judgment), typically that (A -> B <: A' -> B') holds iff (A :> A') and
(B <: B'). For systems where all connectives are invertible in this
way, you know that the structural approch is complete wrt. the
relational approach: to prove a goal of the form (F X <: F Y), you can
reason only on the structure of F by repeated inversion, all subgoals
remains of the form (T[X] <: T[Y]) until the axiom rules, and the
resulting relational derivation is isomorphic to a structural
derivation (only on F).

The relational approach would be more interesting in a system where
non-structural rules are more expressive (they are not admissible in
the structural fragment by cut-elimination or such): where some
subtyping judgments start with two types of the same shape, but their
premises have different shapes. I don't know if if it is the case in
your system.

Finally (and slightly off-topic), there are some cases where
a relational judgment of the form (G |- A <: B) can be seen as
a non-relational type system, by seeing (<:) as a connective with an
introduction rule (into something like (G; A |- B). There is such
a presentation of subtyping with intersection types as the "ISC
system", a sequent calculus for deriving intersection subtypings, in

  Intersection Subtyping with Constructors
  Olivier Laurent, 2018


On Tue, Jan 8, 2019 at 9:55 AM Christopher Jenkins <cwjnkins at gmail.com>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> In Curry-style type systems, it is possible for a term to have two
> different types; in the setting that I am interested in (Cedille) it is
> possible to define a type of "Cast S T" witnessing that all terms of type S
> also have type T, which in turn induces a form of subtyping S <: T.
>
> I would like to know whether anyone knows about or can point me to work
> related to the following two subjects:
>
> 1. type systems in which the subtyping judgment is replaced by a type (like
> Cast) and where subtyping inference rules elaborate terms with inserted
> coercions (Luo's "Coercive Subtyping" is closely related in this second
> respect)
>
> 2. the connection between subtyping and positivity checking for recursive
> types. To expand on this, let F be some type-scheme of kind Type -> Type.
> Often (such as when working with inductive data-types as least fixpoints of
> functors) one is interested in restricting F to be positive. With Cast as
> the notion of subtyping, this requirement can be stated as the existence of
> a proof / function of type X <: Y -> F X <: F Y, in effect allowing one to
> replace the usual detailed account of positivity checking with a set of
> (elaborating) subtyping rules and saying "F is positive iff F X <: F Y is
> derivable assuming X <: Y is in the context".
>
> Maybe this second observation isn't very deep, but nonetheless I could not
> find any work reducing positivity checking to a subtyping problem, and
> wanted to know if someone else has also made this connection.
>
> Thanks,
>