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

[Sandro Stucki]

Dear Christopher,

In addition to the work by Abel and others mentioned by Gabriel, I'd
like to point out Martin Steffen's thesis

  Polarized Higher-Order Subtyping
  Martin Steffen, PhD thesis, 1998
  https://heim.ifi.uio.no/msteffen/download/diss/diss.pdf

which starts out with a presentation of polarized subtyping that has
explicit kinding rules of the form "λX.T has kind k1 -{+}-> k2 iff
T[Y/X] <: T[Z/X]: k2 is
derivable assuming Y <: Z: k1 is in the context" very similar to the
one you suggest in your email (see the various K-Arrow-I rules in ch.
4.4). To establish decidability of subtyping, Steffen then goes on to
show that this system is equivalent to one more closely resembling
Abel's (following the "structural" approach mentioned by Gabriel).
That latter system makes kinding independent of subtyping by
introducing an explicit judgment for positivity checking (or rather,
variance checking) instead.

Best regards
/Sandro


On Tue, Jan 8, 2019 at 11:20 AM Gabriel Scherer
<gabriel.scherer at gmail.com> wrote:
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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,
> >