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

[Christopher Jenkins]

Hi, Gabriel and Sandro,

Thank you very much for the pointers and information! This was very
helpful, especially so the structural / relational distinction for
approaches to subtyping.

Gabriel,

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.
>

What you have described as the NuPRL approach is exactly what we use to
define Cast in Cedille. The only notion of subtyping in the core theory is
the one observed by Miquel for the Implicit Calculus of Constructions as
typing judgments of the form G,x:S |- x:T, and I'm interested in the design
space of languages with subtyping derived from this.

Sandro,

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
>

Excellent, this sounds like what I was looking for!

Thanks again,

On Tue, Jan 8, 2019 at 5:32 AM Sandro Stucki <sandro.stucki at gmail.com>
wrote:

> 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,
> > >
>