⟨ortho|normal⟩

Type Theory


Impredicative Inductives Need Not be Strictly Positive

If you look around for why inductive datatypes need to be strictly positive, you’ll probably end up at Vilhelm Sjöberg’s blog post Why must inductive types be strictly positive?, which gets passed around a lot as an accessible and modernized description of the inconsistency that arises from a certain large, impredicative inductive datatype that is positive but not strictly positive. This example originally comes from Coquand and Paulin-Mohring’s COLOG-88 paper Inductively defined types. A key component of the inconsistency relies on the injectivity of its constructor, but since the inductive is large, even if Rocq were to permit nonstrictly positive inductives, it would still disallow its strong elimination and therefore injectivity!

More …

Impredicative Type Theories

Models of predicative type theory are well-studied and have been mechanized, ranging from proofs of consistency for a minimal type theory with a predicative hierarchy in 1000 lines of Rocq to proofs all the way up to decidability of conversion in 10 000 lines of Agda.

In contrast, the story for impredicative type theory is not so clear. Incorporating different features alongside an impredicative Prop may require substantially different proof methods. This post catalogues these various models, what type theories they model, and what proof technique is used. Most proofs fall into one of three techniques: proof-irrelevant set-theoretic models, reducibility methods, and realizabililty semantics.

Overview

Work Theory Proof method Universes Inductives Equality
Coquand (1985) CC ? Prop, Type none untyped
Pottinger (1987) CC ? Prop, Type none untyped
Ehrhard (1988) CC ω-Set Prop, Type none none
Coquand and Gallier (1990) CC reducibility Prop, Type none untyped
Luo (1990) ECC reducibility; ω-Set Prop ⊆ Type{i} dependent pairs untyped
Terlouw (1993) CC reducibility Prop, Type none untyped
Altenkirch (1993) CC Λ-Set Prop, (Type) impredicative typed
Goguen (1994) UTT set-theoretic Prop, Type predicative typed
Geuvers (1995) CC reducibility Prop, Type none untyped
Melliès and Werner (1998) PTS Λ-Set Prop ⊈ Type{i} none untyped
Miquel (2001) CCω set-theoretic; ω-Set Prop ⊆ Type{i} none untyped
Miquel (2001) ICC ? Prop ⊆ Type{i} none untyped
Miquel and Werner (2003) CC set-theoretic Prop, Type none untyped
Lee and Werner (2011) pCIC set-theoretic Prop ⊆ Type{i} predicative typed
Sacchini (2011) CIC^- Λ-Set Prop, Type{i} predicative, sized untyped
Barras (2012) CCω set-theoretic Prop ⊆ Type{i} naturals untyped
Barras (2012) CC Λ-Set Prop, Type naturals untyped
Timany and Sozeau (2018) pCuIC set-theoretic Prop ⊆ Type{i} predicative typed
More …

ECIC is Inconsistent

…probably. To be clear, ECIC1 refers to Monnier and Bos’ Erasable CIC2, with erasable in the sense of erasable pure type systems (EPTS)3. I’ll argue that even with erased impredicative fields, Coquand’s paradox of trees4 is still typeable.

  1. Not to be confused with their eCIC, the erasable CIC. 

  2. Stefan Monnier; Nathaniel Bos. Is Impredicativity Implicitly Implicit? TYPES 2019. doi:10.4230/LIPIcs.TYPES.2019.9

  3. Nathan Mishra-Linger; Tim Sheard. Erasure and polymorphism in pure type systems. FOSSACS 2008. doi:10.5555/1792803.1792828

  4. Thierry Coquand. The paradox of trees in type theory. BIT 32 (1992). doi:10.1007/BF01995104

More …

Designing Stratified Type Theory

I’ve wanted to write an informal (but technical!) post1 about my current research in progress on Stratified Type Theory (StraTT), but we’ve been occupied with writing up a paper draft for submission to CPP 2024, then writing a talk for NJPLS Nov 2023, then being rejected from CPP, then I’ve just been randomly distracted for two weeks but I’m so back now.

That paper draft along with the supplementary material will have all the details, but I’ve decided that what I want to focus on in this post is all the other variations on the system we’ve tried that are either inconsistent or less expressive. This means I won’t cover a lot of motivation or examples (still a work in progress), or mention any metatheory unless where relevant; those can be found in the paper. Admittedly, these are mostly notes for myself, and I go at a pace that sort of assumes enough familiarity with the system to be able to verify well-typedness mentally, but this might be interesting to someone else too.

  1. A draft of this post was first published on Cohost. 

More …

Notes on Guarded Types

Overview

Work Summary
Nakano1 STLC + recursive types + guarded types
Birkdeal, Møgelberg, Schwinghammer, Stovring2 dependent types + recursive types + guarded types
Atkey and McBride3 STLC + recursive types + guarded types + clocks
Birkedal and Møgelberg4 dependent types + guarded types
Møgelberg5 dependent types + guarded types + clocks
GDTT6 dependent types + guarded types + clocks + delayed substitution
CloTT7 dependent types + guarded types + ticks + clocks
GCTT8 cubical type theory + guarded types + delayed substitution
TCTT9 cubical type theory + guarded types + ticks
CCTT10 cubical type theory + guarded types + ticks + clocks
  1. Nakano, Hiroshi. A Modality for Recursion. (LICS 2000). ᴅᴏɪ: 10.1109/lics.2000.855774

  2. Birkedal, Lars; Møgelberg, Rasmus Ejlers; Schwinghammer, Jans; Stovring, Kristian. First Steps in Synthetic Guarded Domain Theory: .Step-Indexing in the Topos of Trees. (LICS 2011). ᴅᴏɪ: 10.1109/LICS.2011.16

  3. Atkey, Robert; McBride, Conor. Productive Coprogramming with Guarded Recursion. (ICFP 2013). ᴅᴏɪ: 10.1145/2500365.2500597

  4. Birkedal, Lars; Møgelberg, Rasmus Ejlers. Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. (LICS 2013). ᴅᴏɪ: 10.1109/LICS.2013.27

  5. Møgelberg, Rasmus Ejlers. A type theory for productive coprogramming via guarded recursion. (LICS 2014). ᴅᴏɪ: 10.1145/2603088.2603132

  6. Bizjak, Aleš; Grathwohl, Hans Bugge; Clouston, Ranald; Møgelberg, Rasmus Ejlers; Birkedal, Lars. Guarded Dependent Type Theory with Coinductive Types. (FoSSaCS 2016). ᴅᴏɪ: 10.1007/978-3-662-49630-5_2

  7. Bahr, Patrick; Grathwohl, Hans Bugge; Møgelberg, Rasmus Ejlers. The Clocks Are Ticking: No More Delays! (LICS 2017). ᴅᴏɪ: 10.1109/LICS.2017.8005097

  8. Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea. Guarded Cubical Type Theory. (Journal of Automated Reasoning, 2019). ᴅᴏɪ: 10.1007/s10817-018-9471-7

  9. Møgelberg, Rasmus Ejlers; Veltri, Niccolò. Bisimulation as Path Type for Guarded Recursive Types. (POPL 2019). ᴅᴏɪ: 10.1145/3290317

  10. Kristensen, Magnus Baunsgaard; Møgelberg, Rasmus Ejlers; Vezzosi, Andrea. Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. (LICS 2022). ᴅᴏɪ: 10.1145/3531130.3533359

More …

An Analysis of An Analysis of Girard's Paradox

While it’s rather difficult to accidentally prove an inconsistency in a well-meaning type theory that isn’t obviously inconsistent (have you ever unintentionally proven that a type corresponding to an ordinal is strictly larger than itself? I didn’t think so), it feels like it’s comparatively easy to add rather innocent features to your type theory that will suddenly make it inconsistent. And there are so many of them! And sometimes it’s the interaction among the features rather than the features themselves that produce inconsistencies.

More …

How to Use Sized Types?
Let Me Count the Ways

This post is inspired by this thread from the Agda mailing list.

Because Agda treats Size like a first-class type, there’s quite a bit of freedom in how you get to use it. This makes it a bit unclear where you should start: should Size be a parameter or an index in your type? What sizes should the constructors’ recursive arguments’ and return types have? Here are two options that are usually used (and one that doesn’t work.) The recommended one is using inflationary sized types and Size<.

More …

The State of Sized Types

Sized types hold great potential as a very practically useful way to do type-based termination checking, but sufficiently expressive sized types in dependent type theory come with a host of problems, mostly related to its incompatibility with the infinite size found in most simpler or nondependent type systems. This post attempts to describe some potential but ultimately unsatisfying solutions.

More …

Ramblings on the Coq Kernel

Back during the summer of 2019, I worked a bit on the Coq kernel. At the same time, I posted a lot of toots on Mastodon about whatever random problems I was encountering. I’ve decided to collect them here, as it might just be that some of these will be useful to me again at some point.

More …