5 ms·

>Pompom is an attractive implementation of an extensional (!) dependently typed language >Pompom provides [...] a strong normalization system How is this poss

by mbid 5y ago

>Pompom is an attractive implementation of an extensional (!) dependently typed language >Pompom provides [...] a strong normalization system How is this possible? Extensional dependent type theory has undecidable term/type equality, so there cannot be a strong normalization algorithm.

caotic123 5y ago
Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).
- caotic123 5y ago
  As far i know, pompom has a decidable type check though.