17
$\begingroup$

Mostly when I read about impredicativity I see people bemoaning its downsides.

But it's not clear to me why I would want impredicativity in the first place.

Impredicativity is useful for analyzing impredicative systems. And impredicative Pi types can be used to encode recursive datatypes without going up a universe. However, from what I understand Cedille has to go through a few contortions to have induction principles over impredicative encodings of datatypes.

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ Cedille goes through some contortions because Aaron Stump & co. are trying to make Church/Scott encodings practical. In the pure calculus of constructions you can't show Church numerals satisfy induction, but Cedille internalises just enough parametricity (less than I expected, actually) to make proving it possible. $\endgroup$
    – Neel Krishnaswami
    Mar 12, 2022 at 7:36
  • $\begingroup$ Related at Theoretical CS: "Impredicative" in type theory. $\endgroup$
    – hardmath
    Mar 12, 2022 at 19:18
  • 3
    $\begingroup$ "Impredicativity" has many different meanings. The question you link to is about impredicative propositions, and this is what Neel's answer (in particular) is about: it's a property that's just true in classical mathematics. However, often when people talk about "impredicative type theory" they mean an impredicative universe that contains non-propositions as well; this is I think what you refer to re "encoding recursive datatypes", and this sort of impredicativity is inconsistent with classical mathematics. So be careful! $\endgroup$
    – Mike Shulman
    Mar 14, 2022 at 6:55

2 Answers 2

Reset to default
8
$\begingroup$

There are some tricks that only work when you have access to an impredicative universe. They tend to construct "the smallest object" of some kind, without an explicit construction, i.e. a textbook impredicative encoding.

A fancy one that comes to my mind is Mendler encoding. In a nutshell, given some function P : (Prop -> Prop) -> (Prop -> Prop) in CIC, this encoding constructs the "free strictly positivization" of P. This can be used to compose inductive predicate constructions in a modular way, since one effectively abstracts over the syntactic criterion of strict positivity.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I was wondering about encoding inductive predicates using impredicative encodings although this Mendler encoding stuff is fairly beyond me. Something like $\mu (F: \text{Prop} \rightarrow \text{Prop}) = \forall Q, (F Q \rightarrow Q) \rightarrow Q$ seems fairly useless. You'd have to construct indexed inductive propositions to be useful right? Not sure if proof irrelevance makes the lack of induction unimportant. Maybe you would need SProp in Coq? $\endgroup$
    – Molly Stewart-Gallus
    Mar 13, 2022 at 1:48
18
$\begingroup$

All impredicativity means is that propositions form a complete lattice! This is a basic principle of mathematics.

So if you want to be able to use the architecture of mathematics developed in the last century, you need to either support impredicativity or commit to redoing all of mathematics in the fragment of logic your system supports.

The latter isn't as absurd as it first sounds, because it's useful to figure out how the conceptual ideas of mathematics can be embodied in terms of weaker axioms. Weaker axioms give you more models, and hence more situations where you can deploy the arguments/structures.

But it is a lot of work, and if you are interested in doing other things than foundations (e.g., proving the correctness of a compiler), not having impredicativity is a big distraction.

Improve this answer
$\endgroup$
5
  • 10
    $\begingroup$ You could have gone one step further and claimed that the architecture of mathematics developed in the last century is build on top of a particular complete lattice which is claimed to have precisely two elements. $\endgroup$
    – Andrej Bauer
    Mar 12, 2022 at 8:39
  • 2
    $\begingroup$ This is also sensible: Larry Paulson once told me he prefers classical mathematics for backwards compatibility reasons. $\endgroup$
    – Neel Krishnaswami
    Mar 13, 2022 at 8:37
  • 5
    $\begingroup$ OTOH, I choose my foundations for trolling purposes: classical around type theorists and constructive around mathematicians. 🧌 $\endgroup$
    – Neel Krishnaswami
    Mar 13, 2022 at 8:40
  • 1
    $\begingroup$ I troll by switching between foundations in every sentence. $\endgroup$
    – Andrej Bauer
    Mar 13, 2022 at 11:11
  • $\begingroup$ @AndrejBauer as long as foundations have a Kripke frame structure, I can accommodate for that. $\endgroup$
    – Pierre-Marie Pédrot
    Mar 13, 2022 at 14:55

Your Answer

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

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