by Conor on February 21, 2006.
Tagged as: Lunches.
I rambled interminably about the slippery tar pit that is equality in Type Theory, dicussing the various enviable and execrable aspects of both Intensional and Extensional variants. More or less, the intensional story gives you a definitional equality which is computable, given a suitable notion of partial evaluation, but the propositional equality is annoyingly weak: in particular, extensionality for functions does not hold. Extensional type theory fixes this by making the definitional equality reflect the propositional equality, but in some ways the cure is worse than the disease: the definitional equality is no longer computable, typechecking is undecidable, and well-typed programs may be utter nonsense in the presence of assumptions. Thorsten and I propose a remedy, Observational Type Theory, in which the reflection happens in the other direction: the non-computational definitional equality rules are reflected as the typing rules for equality proofs; the structural equality constructor for λ just expresses extensionality. We get all the provable equations of Extensional Type Theory, and if we’ve played our cards right, we get all the defintional equations of Intensional Type Theory. It’s a win-win situation.