🌌 Make the Universe Strict #367
Conversation
|
Thanks for this work, and I'm very sorry that your code has not received an official review after all this time! I am thinking about the definitional equality issue you mentioned... Let me ponder it a little bit. |
There was a problem hiding this comment.
My concern about making ElStable definitionally equal to its unfolding is exactly the thing you point out --- in parts of the implementation, we rely on something being a code. Unfortunately, it is not reasonable for these parts of the code to not be stable under definitional equivalence. To put it another way, an important invariant of an implementation of type theory is that if you replace equals by equals, things continue to work --- but this change will violate that.
Thus I think that something a bit more elaborate will be required in order to maintain the necessary invariants.
|
Let me continue reviewing this actually, I misunderstood some of it. |
|
Closing, as we have discussed some new design. |
This PR does away with
ElInandElOut, and makesElStable codedefinitionally equal tounfold_el code, and closes #189.I initially tried removing
ElStableentirely, but found that this solution was the simplest, as there are several places where we rely on something being a code.The main complication this introduces is that pattern matching on a type requires also matching on its code, because they're now equal. The only place we don't have to do this is when matching on the goal in a tactic, because we have still have
intro_implicit_connectivesandelim_implicit_connectives, which now unfold anElStablebut do not addElInorElOut. PerhapsElStableshould no longer be an "implicit connective" and we should instead be pattern matching on codes in tactics as a matter of consistency?Having multiple representations of definitionally equal types in the core theory initially felt awkward to me, but @TOTBWF pointed out to me that this is sort of like an eta law for the universe. The main difference is that we're not usually pattern matching on "a variable at function type or a lambda" but we match on types pretty regularly.
This is a non-trivial change to cooltt, so please let me know if this implementation is a Bad Idea and needs to be reworked.