Post #968742
2026-02-09 11:10 UTC
New paper with @edwinb on a SOGAT approach to erasure for dependent types, where erasure is an open modality:
https://cthe.me/erasure-sogat.pdf
Turns out this is pretty nice for implementation: having a structural specification means it is clear how to do pattern unification.
Demo impl: https://github.com/kontheocharis/erasure-impl
Replies (3)
-
@olynch@mathstodon.xyz 2026-02-09 13:40
@edwinb @constantine I think we've been thinking very similar thoughts! https://owenlynch.org/archive/2025-aria-ta1-seminar/1.html
-
@jonmsterling@mathstodon.xyz 2026-02-09 13:57
@constantine @edwinb Very nice! Glad someone took this up properly.
-
@ncf@types.pl 2026-02-12 13:51
@constantine @edwinb The sort # ∈ Γ is interpreted as a map Γ → ϕ Should this be Γ → Ω?