natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Typecase is a version of ad hoc polymorphism that appears in some type theories.
Typecase in a dependent type theory implies that the type theory does not satisfy parametric polymorphism in the meta-theory (see Boulier, Pédrot & Tabareau 2017). As a result, typecase is inconsistent with explicit parametricity.
Some discussion on typecase in dependent type theory occurs in:
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau, The next 700 syntactical models of type theory, CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Pages 182 - 194, 16 January 2017 [doi:10.1145/3018610.3018620]
Continuations, parametricity, and polymorphism, Category Theory Zulip (web)
Last revised on July 11, 2025 at 16:25:43. See the history of this page for a list of all contributions to it.