coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Xavier Leroy <xavier.leroy AT college-de-france.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Impredicative Set
- Date: Tue, 2 Apr 2019 17:19:23 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xavier.leroy AT college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy AT college-de-france.fr; spf=None smtp.helo=postmaster AT smtpout10.partage.renater.fr
Hi Xavier,
If you are not (yet) interested in logical consistency
then isn’t Type : Type better? At least there is no pretence of being consistent (or strongly normalising).
I call this “honest impredicativity”.
Cheers,
Thorsten
From: <coq-club-request AT inria.fr> on behalf of Xavier Leroy <xavier.leroy AT college-de-france.fr>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 2 April 2019 at 15:16
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Impredicative Set
On Tue, Apr 2, 2019 at 3:42 PM Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:
Maybe you can tell us for what you actually want to use an impredicative universe?
The question is not addressed to me, but at any rate:
Impredicative systems such as F and F_omega may be questionable from a logical point of view, but make perfect sense as type systems for programming languages. Haskell contains F_omega, OCaml contains F (in the core language) and bits of F_omega (at the module level). Strong normalization doesn't really matter since those languages have general recursion to begin with. But stratification by universes is not nice in programming languages: it gets in the way of some programming idioms, as JF Monin alluded to.
Coming back to the original question, my only use for Coq's impredicative-Set option is to learn and teach about system F / F_omega and their impredicative encodings of data types. I think Coq works better than Haskell or OCaml for this teaching purpose, as Coq's presentation of F_omega is closer to the textbook presentations.
Best,
- Xavier
Thorsten
On 15/03/2019, 18:35, "coq-club-request AT inria.fr on behalf of Jay Kruer" <coq-club-request AT inria.fr on behalf of kruerj AT reed.edu> wrote:
Hi coq-club,
I am wondering how “sketchy” the use of impredicative Set in Coq developments is considered. I have seen that impredicative Set is inconsistent with some axioms of classical mathematics (e.g. excluded middle), but for the careful user who avoids such axioms (or needs no axioms in their development at all) is there any reason to avoid it? The Coq reference manual alludes to some intuitionists taking issue with impredicative Set even before one introduces inconsistency with axioms but I haven't been able to find any of those arguments.
Thanks,
— Jay
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.
- Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Xavier Leroy, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Xavier Leroy, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Stefan Monnier, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Xavier Leroy, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Xavier Leroy, 04/02/2019
Archive powered by MHonArc 2.6.18.