[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> > 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 <[email protected]> wrote: > On Tue, 8 Jan 2019 at 09:55, Christopher Jenkins <[email protected]> > 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 >
