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.
-
(no subject)
After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…
-
(no subject)
Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…
-
(no subject)
I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
