Polarities: subtyping for datatypes

[catalin-hritcu]

(x:int{x>1} * y:int{y>1}) is not a subtype of (int * int)

[nikswamy]

This is not a bug. The type on the left is just (Tuple2 (x:int{x > 1}) (y:int{y > 1})), where Tuple2 is just an inductive type, like any other.

We do not have subtyping on the indexes of an inductive type.

We cannot add it unless we enhance the type system with a notion of polarities for type indices.

You can, however, write a total coercion of the following type and use it to massage your type as needed.

val forget: a:Type -> b:Type -> p:(a -> Type) -> q:(b -> Type) -> r:(x:a{p x} * y:b{q y}) -> Tot (s:(a * b){fst s = fst r && snd s = snd r})

Once we add support for ghost code, we should be able to erase uses of coercions like forget in generated code.

[catalin-hritcu]

Was thinking with @victor-dumitrescu the other day that polarities can be seen as a form of relational refinements. For instance, a positive type constructor like list could have type:

list: a:Type -> Tot (b:Type{L a <: R a => L b <: R b})

where <: is an internalization of the subtyping judgment. Would doing polarities this way be a crazy idea? :)

[catalin-hritcu]

#593 has some good examples where polarities are really needed.

[catalin-hritcu]

Was discussing with @alejandroag the other day that internalizing subtyping (or any other judgment) is tricky, since the logical encoding is sound but incomplete. It seems that for the negative positions in a formula (like L a <: R a above) we would need an unsound but complete encoding. Such encodings that are "sound for counterexamples" exist (e.g. in Nitpick and Nunchaku), but it's very unclear how well one can mix the two kind of encodings. And anyway, there are better reasons to implement "sound for counterexamples" encodings ... if we ever do that, we can do further experiments with mixing things.

[catalin-hritcu]

@aseemr Wondering whether we will also get this from your positivity check for inductives.

[catalin-hritcu]

@kyoDralliam has discovered a counterexample/paradox in the literature showing that enabling subtyping for datatypes would currently be unsound. He knows about this for a while, still it would be good to write this all down somewhere (e.g. here). From what I understand, a potential solution for this would be to remove type arguments to datatype constructors.

[danelahman]

@catalin-hritcu @kyoDralliam Is that the counterexample from Luo's note about Russell-style universes (http://www.cs.rhul.ac.uk/~zhaohui/universes.pdf)?

[kyoDralliam]

It's that same counterexample. Here's is what it looks like for F* + subtyping for pairs.

type pair a b : Type = | MkPair : a -> b -> pair a b

let elim (a b : Type) (c : pair a b -> Type) (f: (x:a -> y:b -> c (MkPair #a #b x y))) (p: pair a b) : c p 
= match p with | MkPair x y -> f x y

let subject_reduction_failure (x y:nat) (c:pair int int -> Type)
    (f : (x:int -> y:int -> c (MkPair #int #int x y)))
    : c (MkPair #nat #nat x y <: pair int int (* we don't have this now *)) = 
  elim int int c f (MkPair #nat #nat x y <: pair int int (* we don't have this now *))

(* This returns -1 at type nat *)
let unsound () : nat =
  subject_reduction_failure 1 2 (function (MkPair #a #b x y) -> a) (fun x y -> -1)

this is well typed because (x,y) <: int * int but reduces to f x y which is of type c (MkPair #int #int x y) and not c (MkPair #nat #nat x y)

[catalin-hritcu]

The current fix proposal discussed with @theolaurent and @kyoDralliam is to prevent matching inductive parameters. In Kenji's counterexample this will make it impossible to write (function (MkPair #a #b x y) -> a).

[catalin-hritcu]

Discussed this again with @kyoDralliam and @mtzguido, and the main challenge for adding datatype subtyping is that now constraints such as a * b <: c * d will no longer reduce to equalities a == c and b == d but to subtyping a <: c and b <: d, which might be less efficient. I vaguely remember discussions with @nikswamy in Redmond in fall 2016, but I'm not sure what the conclusion was on this.

[catalin-hritcu]

I'm now getting errors on (function (MkPair #a #b x y) -> a):

This pattern (_) binds an inaccesible argument; use a wildcard ('_') pattern

It seems a recent change from July by @nikswamy : 8939c3e#diff-9a12b72662f95654a4c5ab46f41257b3R99
Does this completely prevent matching on inductive parameters, as we would need for fixing this issue? :)

[nikswamy]

@catalin-hritcu Confused by your last remark. Projecting the parameters of a datatype is exactly what we want to prevent. Why do you want to write it?

[catalin-hritcu]

@nikswamy Sorry if this was unclear. Completely preventing matches on inductive parameters is indeed what we need for fixing this issue. And the question is whether your change completely prevents such matches already.

[catalin-hritcu]

Status update on this issue:

• As required for soundly implementing subtyping for datatype parameters, pattern matching on parameters is now disallowed (see comment above) and a fix by Nik changed the SMT encoding to forbid injectivity for some inductive types with parameters in too large universes. The current issue would require extending this to all parameters of all inductives, which Nik tried but has lead to regressions.
• There has been no work so far on implementing subtyping for datatypes, and one worry Nik and others (see above) had is that this could impact typechecking performance, since subtyping constraints on the type parameters are harder to solve than the current equality constraints.

[nikswamy]

Addressing this issue requires more research. Closing as a wontfix until then.

[catalin-hritcu]

Just for the record, wanted to mention that @kyoDralliam and @theolaurent are doing some of that research. For instance, the French readers can see this: https://kenji.maillard.blue/Writings/mettons-de-l-ordre-dans-cic-171220.pdf

[catalin-hritcu]

... and a more recent extended abstract in English: Noninvasive Polarized Subtyping for Inductive Types. Théo Laurent and Kenji Maillard. TYPES 2022.
https://types22.inria.fr/files/2022/06/TYPES_2022_paper_62.pdf
https://types22.inria.fr/files/2022/06/TYPES_2022_slides_62.pdf
https://www.youtube.com/watch?v=2xXiVzxzm_M

[catalin-hritcu]

Let me mention that there is a now paper about the research above that will appear at ESOP'24:
Definitional Functoriality for Dependent (Sub)Types. Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard.