Software engineer, dilettante type theorist, syntactician, and philologist. Student of Ancient Greek, Sumerian, Hittite, Akkadian, Latin, Old English and German. I also co-host The Type Theory Podcast. Ideas written up here are rough at best.
I am in software engineering (functional programming preferred). I also provide tutoring services in any of the languages listed above, as well as type theory & proof theory. See my Curriculum Vitae.
Briefly, Diaconescu’s theorem states that the axiom of choice & extensionality together suffice to imply tertium non datur. In 100 Years of Zermelo’s Axiom of Choice, Martin-Löf distinguishes an intensional version of AC from an extensional one, and argues that whilst the former is a theorem of intuitionistic type theory, the latter leads to taboo. In this note, I hope to clarify a few matters, and demonstrate that the matter at hand is not so much extensionality, but infelicitous interpretation of quantifiers. When viewed through this lens, it becomes evident that the problem all along was setoids, not extensionality.
There are two standard techniques for representing dependently typed calculi in the LF. The first is to re-use the LF contexts for the object contexts, which can lead to difficulties when the meaning of hypothetico-general judgement in the object language is stronger than in the LF; this is, for instance, the case in MLTT 1979, where non-trivial functionality obligations are incurred in the sequent judgement.
Another technique advanced by Crary is to represent contexts explicitly, and then define a sequent judgement over them; this can be used to resolve the problem described above (and several others), but it comes at the cost of verbosity, and introduces certain other difficulties for my purpose. In this paper, I demonstrate an alternative, higher-order encoding of telescopes which can be used to faithfully encode the functional sequent judgement for MLTT 1979. You may also view a parallel Twelf development.
The intrinsic and extrinsic views on types are unified by considering two categories: one of syntactic types and terms, and another of semantic types and derivations, and then a forgetful functor from the latter to the former. Following Melliès and Zeilberger’s Functors are Type Refinement Systems, we might attempt to provide a similar characterization for computational type theories with universes, but there are some wrinkles; I attempt to provide a partial resolution to these here.
In 1994, Per Martin-Löf wrote Analytic and Synthetic Judgement in Type Theory, in which he convincingly showed that undecidability phenomena should be understood in terms of synthetic judgement, and demonstrated how the judgements of one theory may be made the propositions of another.
I am pleased to make available the result of joint research with Darryl McAdams, our new paper Dependent Types for Pragmatics which is currently under review for publication in the Journal of Logic, Language and Information. I’d like to discuss a few aspects of the work which I consider important, lending additional emphasis to foundational aspects of type theory which I fear were lost in the presentation, which was meant for a general Linguistics audience.
The key idea of Observational Type Theory1 is to make the propositional equality coextensive with the equality which is validated under the standard semantics for Type Theory, which is the meaning explanations and their metamathematical counterpart, the realizability interpretation. Now, Extensional Type Theory is usually characterized in terms of typechecking (membership) being undecidable because the “true” equality is made to hold judgementally; but this is a deceptive characterization when applied to Computational Type Theory (Nuprl), since there are many types besides equality which may be given meaning explanations but which have an undecidable membership judgement.
Whilst the judgements of type theory are preferred to be analytic, the practice of operating a proof assistant is inherently and unavoidably synthetic, and is always accompanied by some manner of refinement and tactics: and so the question is never whether to use tactics, but rather how much pain one intends to experience in the process of using them: this is inextricable from the activity of proving.
I’m so pleased to be able to announce the first fruit of a joint project with David Christiansen and Darin Morrison, which is an interview of Peter Dybjer for The Type Theory Podcast. We spoke to Peter about QuickCheck-style testing and its relation to proofs and verification in type theory. Subscribe to the RSS feed or follow us on Twitter if you are interested in listening to discussions with researchers, because we have more to come.