Lifting coercions to theory refinements › Avoiding dependent coercions via “selfification” [01HS]

Many treatments of coercions do not handle well the problem of when the type of the coercion seems to depend on the value being coerced. Luo and Soloviev attempted to address this problem by introducing a notion of “dependent coercion”; Lean also has a notion of dependent coercion. Luo and Soloviev’s version seems to have some issues, where the most expressive rules that one would want cannot be included without breaking transitivity elimination; Lean’s version explicitly does not support chaining of dependent coercions, and I wonder if this is the reason why.

I am contending today that many useful cases of dependent coercions don’t actually need to be dependent. My idea is based off an old trick known only to the ML Modules Crew called “selfification”, which my PhD advisor Bob Harper kindly taught me several years ago. The idea of “selfification” is to transform a dependent coercion problem into a non-dependent one.

Suppose that we have a bidirectional elaborator, and we are now at the mode-shift. We have received some typed term M:T where T is a theory expression and we are trying to check it at type B. Rather than searching for a canonical coercion from T -> B, we instead first construct the maximal refinement “T/M” of T to a definitional singleton type that contains only M; this means refining all the fields of T to project the corresponding ones from \(M\). Then we try to find the canonical coercion from T/M to B.

(I think we can also generalise the algorithm to work even when the synthesised type is not a theory expression, but I won’t talk about that today. In case I forget, the idea is treat the mode shift as always being between theory types, which can be done by having a built-in theory for typed terms.)

I want to show an example. Consider the case of trying to define the following dependent function:

cool (X : Monoid): Semigroup / {car => X.car}
cool X => X

The idea here is that (1) if X is a monoid, then it’s a semigroup by forgetting the extra stuff; and (2) forgetting this extra stuff leaves the carrier set fixed. Can we justify returning X as above via elaboration?

Yes. The elaboration state at that point is asking us to convert X : Monoid to Semigroup / {car => X.car}. Obviously we cannot hope to find a coercion Monoid -> Semigroup / {car => X.car}, but what we do instead is attempt to find a coercion from

Monoid / {car => X.car, join => X.join, unit => X.unit, join/assoc => X.join/assoc, join/unit/left => X.join/unit/left, join/unit/right => X.join/unit/right}

to Semigroup / {car => X.car}. And that is something we can evidently do, using our notion of canonical coercion between refined theories!

In summary, we have very strong dependent-type-friendly coercions, without needing the coercions themselves to be dependent functions.