The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

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.