16
$\begingroup$

The title pretty much covers it. I'm wondering if someone is maintaining a list of counterexamples in type theory. I'm aware of Counterexamples in Type Systems, which I think is very nice, but I guess I'm more interested in something closer to the mentality of Counterexamples in Topology or counterexamples in category theory. I'm thinking of something like a list of type systems which don't have desired meta-theoretic properties because of interesting features (e.g., non-normalization of impredicativity + proof-irrelevant equality [Abel, Coquand, 2020]) or which lie in a general class of systems that one might expect to be well-behaved (e.g., the cute example in [Pollack 1992] of a strongly normalizing functional PTS without decidable type checking).

(This is obviously a soft question, and personally, I would also love to also see answers/comments with some greatest-hits counterexamples, especially if such a document doesn't exist, but I'm admittedly somewhat new to StackExchange and don't know if that fits into the ethos of the site. So feel free to cross this part out if it doesn't.)

$\endgroup$
4
  • 2
    $\begingroup$ There are already many counterexamples on this website, but very scattered. It would be nice if they can be collected $\endgroup$
    – ice1000
    Dec 24, 2022 at 2:42
  • $\begingroup$ Should we make it wiki answers, and just collect references here. $\endgroup$ Dec 24, 2022 at 23:10
  • $\begingroup$ Again, I'm a bit new to StackExchange, but if I understand this post correctly, I think that makes sense to do, especially since it seems I've verified there is not an obvious list I missed. $\endgroup$
    – Nathan
    Dec 25, 2022 at 0:07
  • $\begingroup$ To get thisngs strated, perhaps you can amend your question with a list of suggested counter-examples, although many of the most famous ones will appear in Stephen Dolan's counterexamples in type systems. $\endgroup$ Dec 26, 2022 at 10:29

3 Answers 3

7
$\begingroup$

Coq maintains a document of historical proofs of absurdity, including brief explanations of the flaw that allowed them to pass. Most of these are more "counter-examples in type theory implementations" ("Set+2 was incorrectly simplified to Set+1", various de Bruijn indexing bugs), but the section titled "Conflicts with axioms in library" has some interesting ones (the guard checker used to be incompatible with propositional extensionality, for example).

Bug trackers are also probably good places to go digging if you want. For example, Coq's SProp UIP + impredicative Prop breaks decidability of typechecking, and the way Agda implements mutual blocks allows something very close to Very Dependent Types / Insanely Dependent Types which might or might not be inconsistent.

$\endgroup$
1
4
$\begingroup$

Making this a community wiki. Here are a few that come to mind, some more obvious than others, with a theme, and not described in detail. May add more later.

  1. A simply typed $\lambda$-term whose computation in the $\lambda\sigma$-calculus does not always terminate. [Mellies (1995)]

  2. $\lambda U$ and $\lambda U^-$ are non-normalizing PTSs which are functional and non-dependent. [Girard (1972)]

  3. The non-functional PTS with sorts $\{1, 2, 3\}$ and axioms $1 : 2$ and $1 : 3$ does not satisfy type unicity.

  4. The PTS with sorts $\mathbb N$, no rules, and axioms $$ \mathcal A = \{(i: n) : \text{the $i$th Turing machine halts on $i$ in $n$ steps}\} $$ is strongly normalizing and functional but has undecidable type checking [Pollack, 1992]. But any functional PTS with finite sorts has decidable type checking [Jutting, 1993].

  5. Impredicative type theory with proof-irrelevant propositional equality is not weakly normalizing. [Abel, Coquand (2020)]

  6. Tight reduction (i.e., $\beta$-reduction on terms with type-annotated application and abstraction) does not satisfy CR on non-well-typed terms.

  7. Cyclic F (i.e., F with the additional axiom $\square : *$) is strongly normalizing and has cyclic axioms.

$\endgroup$
3
  • $\begingroup$ Wait, what's that 3rd one? Usually type correctness means "type safety", which holds for all PTSes (functional or not). $\endgroup$
    – cody
    Jan 1, 2023 at 1:54
  • 1
    $\begingroup$ Apologies, meant type unicity (all types of a given term are $\beta$-equivalent). Fixed. $\endgroup$
    – Nathan
    Jan 1, 2023 at 23:05
  • $\begingroup$ Any reference for number 7? $\endgroup$
    – cody
    Jan 22, 2023 at 4:59
3
$\begingroup$

As mentioned in this answer on this site, so-called "positive coinductive types" break subject reduction.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.