Sending strict propositions to the Ripley cupboard [01IK]

Please note: I am no longer confident in the conclusions of this post, and I believe that I have made some mistakes. When I have ironed out what is true and what is not true, I will write a follow-up and link to it from here.

Conor Mc Bride likes to send hopeless ideas and design mistakes to their Ripley Cupboard, a reference to a scene in the highly underrated film Alien: Resurrection in which all the hopeless attempts to reconstruct Ellen Ripley from DNA are stored in a gruesome menagerie. I am afraid that in spite of their successful semantic rehabilitation, strict / definitionally proof-irrelevant propositions must nonetheless find their permanent residence in my own Ripley cupboard for syntactical reasons.

One thing that I had noticed a couple nights ago was that there might be a problem finding a suitable generalisation of Miller’s pattern fragment for dependent type theory with strict propositions. I was not really precise about what my concern was, but thankfully Matthieu Sozeau managed to pin it down.

In essence, the problem has to do with what syntacticians call “strengthening”. The thing that makes higher-order pattern unification work well is the ability to tell whether or not some term actually depends on a given variable up to definitional equality; this is important because if you can eliminate a syntactic dependency, two things might happen that could allow the unification process to proceed further (1) a blocked unification problem may suddenly fall into the pattern fragment, and (2) a failing “occurs check” may start to succeed.

With definitional singleton types, this is all fine: we can reliably eliminate dependency on singletons in a number of different ways, but these ways all rely on the fact that singleton types are inhabited. For definitional subsingletons, i.e. strict propositions, it is another story. Imagine that you have a strict proposition \(P\) and a subterm \(M(x,y,z):P\) of a larger proof-relevant unification problem; in order to find out whether or not the whole problem depends on \(x,y,z\) you need to know whether or not a “shorter” proof of \(P\) is derivable, which is obviously an undecidable problem.

The upshot is, as Matthieu put it, we are not going to be able to find most general unifiers in any fragment of the language that involves strict propositions. Completeness of unification within a well-defined fragment is, in my opinion, the mathematical shadow of a more important but intangible property of unification being reliable and predictable. Therefore, I think that this observation may imply that reliable and predictable unification is not compatible with having strict propositions in any form.

The implication for Project Pterodactyl is that we will not be pursuing strict propositions in any form, including my recent proposal.

(It would be very welcome if someone noticed a way to get around this apparent obstruction, but I am not optimistic. It seems pretty airtight to me at the moment.)