WingNews logo WingNews
top | item 28729689

(no title)

mbid | 4 years 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.

discuss

order

caotic123|4 years ago

Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).

caotic123|4 years ago

As far i know, pompom has a decidable type check though.