Started to go through and TeX up an account of pattern unification with irrelevance around, trying to start from Pientka-Pfenning's account of evars as relative-validity modal variables. The only question that stares me in the face is how to make sure equality and typechecking are still decidable. You can't just raise u :: (A_1, ..., A_n |- B) and u[M_1 ; ... ; M_n ; .] to x : A_1 -> ... -> A_n -> B and x M_1 ... M_n, can you? In any event, I think I had a minor revelation a day or two ago while meditating on the open-world assumption that in fact the right answer to \a\b X 2 = \a\b Y 1 is (X := \a Z, Y := \b Z), since the more complicated terms that might be substituted for X and Y (like cd o (ac 1) and cd o (bc 1)) in the appropriate signatures (like ac : a -> c, bc : b -> c, cd : c -:> d) are obtainable up to definitional equality by substituting (Z := cd o W) for W : c Also: more jazz, more B5.
Started to go through and TeX up an account of pattern unification with irrelevance around, trying to start from Pientka-Pfenning's account of evars as relative-validity modal variables. The only question that stares me in the face is how to make sure equality and typechecking are still decidable. You can't just raise u :: (A_1, ..., A_n |- B) and u[M_1 ; ... ; M_n ; .] to x : A_1 -> ... -> A_n -> B and x M_1 ... M_n, can you? In any event, I think I had a minor revelation a day or two ago while meditating on the open-world assumption that in fact the right answer to \a\b X 2 = \a\b Y 1 is (X := \a Z, Y := \b Z), since the more complicated terms that might be substituted for X and Y (like cd o (ac 1) and cd o (bc 1)) in the appropriate signatures (like ac : a -> c, bc : b -> c, cd : c -:> d) are obtainable up to definitional equality by substituting (Z := cd o W) for W : c Also: more jazz, more B5.
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
