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

[Christopher Jenkins]

>
> Maybe silly question: What about F X = X, or beta-equivalent
> functions? That is covariant (satisfies `X <: Y -> F X <: F Y`), but
> mu F is not well-defined because F is not *contractive*.
> Do I miss something, or is that *the* obvious and implied exception?
> (Feel free to answer on-list if the question isn't too silly).
>
> Cheers,


It's not a silly question at all! I did some experimentation in Cedille and
the answer is that for our derived notion of functor fix-point you can
indeed take the fixpoint of `F X = X' -- but the resulting type is
uninhabited (you can construct a function of type mu F -> ∀ X: Type. X.)

On Tue, Jan 8, 2019 at 9:16 AM Paolo Giarrusso <p.giarrusso at gmail.com>
wrote:

> On Tue, 8 Jan 2019 at 09:55, 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.
>
> > 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 silly question: What about F X = X, or beta-equivalent
> functions? That is covariant (satisfies `X <: Y -> F X <: F Y`), but
> mu F is not well-defined because F is not *contractive*.
> Do I miss something, or is that *the* obvious and implied exception?
> (Feel free to answer on-list if the question isn't too silly).
>
> Cheers,
> --
> Paolo G. Giarrusso
>