The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 01/19/2017 06:02 PM, Théo Zimmermann wrote:
> Very good point Pierre. And now that you mention this, Matthieu was 
> precisely recently talking about the need for anonymous records (which 
> would probably be made available by creating a syntax for
> anonymous inductive types, since Coq's record are implemented in terms of 
> inductive types).

Then you do not need "module sublanguage". You can similate it via structural 
records and statical scoping.
(functors would become functions)

This is what Benjamin Pierce & David Turner did in Pict.

> 
> Le jeu. 19 janv. 2017 à 17:57, Pierre Courtieu 
> <pierre.courtieu AT gmail.com
>  
> <mailto:pierre.courtieu AT gmail.com>>
>  a écrit :
> 
>     Hi,
> 
>     Something that may confuse Matej is also that the only way of defining
>     an inductive in Coq is to declare it via a definition. Which Matej
>     associates to "changing the type Set by adding new inhabitants in it"
>     but this is a wrong interpretation. All inductive types exists from
>     the beginning, it is just that the implementation of Coq does not have
>     a anonymous syntax for them (and maybe other deeper problem I am not
>     aware of).
> 
>     You can define anonymous functions like this: (fun x:Prop => Prop).
>     And everyone will probably admit that this function existed even
>     before we write it (although we may reach philosophical problems with
>     this formulation).
> 
>     But you cannot declare an anonymous inductive in such a way in coq
>     (say for instance with a binder syntax like this: (Ind nat:Set =>
>     O:nat | S: nat -> nat). So one could conclude that nat "does not exist
>     until it is declared".
> 
>     But actually the underlying theory do have this kind of anonymous
>     inductive (see constr.ml <http://constr.ml> as suggested by Maxime). So 
> all typable
>     inductives types always existed as every typable other terms.
> 
>     Hope this helps,
>     Pierre
> 
> 
> 
> 
>     2017-01-19 17:31 GMT+01:00 Jonathan Leivent 
> <jonikelee AT gmail.com
>  
> <mailto:jonikelee AT gmail.com>>:
>     >
>     >
>     > On 01/19/2017 11:20 AM, Matej Kosik wrote:
>     >>
>     >> ...
>     >>    Coq < Check (forall x : Set, x) : Set.
>     >>    Toplevel input, characters 0-32:
>     >>    > Check (forall x : Set, x) : Set.
>     >>    > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>     >>    Error:
>     >>    The term "forall x : Set, x" has type "Type@{Set+1}"
>     >>    while it is expected to have type "Set".
>     >>
>     >>
>     >> So this is not the counter-example that would show that, when I start
>     >> "coqtop -noinit" it would be the case that:
>     >>
>     >>    Set not only has all the inhabitants of Prop, but it also has 
> some such
>     >> inhabitants, which are not in Prop.
>     >>
>     >> (in which case we could relax "Prop < Set" to "Prop ≤ Set").
>     >>
>     >> Are there such counter-examples?
>     >
>     >
>     >
>     > I think you are missing some implications of what Bruno Barras said 
> here:
>     >
>     >> The reason why Prop:Set does not hold (although it is consistent in 
> the
>     >> default settings of Coq: think of Set as Type(0) and Type(i) as 
> Type(i+1))
>     >> is that Coq allows to make Set impredicative, and we expect this to 
> be an
>     >> extension of Coq without the option set (all theorems of Coq without 
> the
>     >> option are theorems of Coq with it).
>     >> With this option set and Prop:Set, Coq would then contain system U 
> which
>     >> is inconsistent.
>     >
>     >
>     > (this, by the way, would be a great addition to the FAQ).
>     >
>     > Note that when -impredicative-set is used, then
>     >
>     > Check (forall x : Set, x) : Set.
>     >
>     > succeeds.  I think that plus the design constraint on Coq Bruno 
> mentioned
>     > above - all theorems without -impredicative-set are theorems with
>     > -impredicative-set - might imply that Prop can't bet <= Set even 
> without
>     > -impredicative-set.
>     >
>     > -- Jonathan
>     >
>     >
> 


-- 
Matej Košík