Proposal to extend boundary-sensitive refinement to positive types

[jonsterling]

Right now the boundary sensitive refinement via extension types only works for negative types. In particular we can reduce (M,N) : A * B [phi -> U] to M : A [phi -> U.1] and N : B [phi -> U.2]. But there is no corresponding principle for positive types like A+B.

I am proposing a new class of predicates with which to define extension types that will allow an appropriate refinement rule for inl/inr.

Here is the grammar:

L ::= [] | P L
P ::= inl | inr | ...
\Phi ::= \phi -> L = M

P is a positive "frame" for a pattern; L is some kind of positive stack, i.e. semantically some kind of linear function.

We then define a new kind of extension type {A | Phi}. This type is actually pretty hard to implement, because we must update the nbe to support the more complex partial boundaries given by Phi; we would have things like "I am a neutral that becomes M when you apply inl to me". All this is possible, but it should be accompanied by a bit of thought into how this should be most cleanly arranged. Ordinary extension types are recovered as the special case {A | phi -> [] = M}.

Refinement rule for positive constructors

We will need to have some judgment for positive frames / constructors P : A ~> B. We now have a refinement rule for the application of a constructor:

|- Q : B ~> A  | phi -> P
|- M : B | L = M
--------------------------
Q(M) : A | \phi -> P L = M

It is important to note that the above is compatible with HITs --- it will work equally well with path constructors.

Potential extension to support function signatures

We have discussed function signatures. In the non-recursive case this basically involves adding a new kind of stack ap([], L). Something tricky happens in the binding structure. The recursive case is just as hard as it was before, and I'm personally still not sure what to do about it.

[cangiuli]

Yes, let's do it! When I was working on the recursive case some months ago, my thought was to immediately left-invert these new equations, i.e. to have an operation in the domain that computes an equalizing substitution for each. This relies on the constrained variables being local (i.e., it implements only "extension types for coproducts" and not "cubical subtypes for coproducts") but that seemed desirable anyway because the patterns ought to be linear in these variables.

positive constructors

I'll just mention that the story for inl,inr doesn't work for HITs because the boundary of a linear pattern may not be linear. For example, inl is definitionally injective but merid i is not.

The recursive case

This is hard. :( The main obstacle I found is that we need some kind of "termination checking" for the patterns.

[jonsterling]

let’s talk more about the hit case. i think there may be a way to make it work, but it may be subtle.