Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: [coqdev] messy behavior with universes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: [coqdev] messy behavior with universes


chronological Thread 
  • From: Andreas Abel <andreas.abel AT ifi.lmu.de>
  • To: Randy Pollack <rpollack AT inf.ed.ac.uk>
  • Cc: Vladimir Voevodsky <vladimir AT ias.edu>, Carlos Simpson <Carlos.Simpson AT unice.fr>, Tom Prince <tom.prince AT ualberta.net>, Coq-Club Club <coq-club AT inria.fr>, coqdev <coqdev AT inria.fr>
  • Subject: Re: [Coq-Club] Re: [coqdev] messy behavior with universes
  • Date: Tue, 19 Apr 2011 08:14:50 +0200

On 18.04.11 5:41 PM, Randy Pollack wrote:
Agda has some nearly-first-class treatment of universe levels.  I
don't know what the theory behind it is.

We are working on it... ;-) The theory should become clearer in the near future.

Cheers,
Andreas


Matita (from Bologna) has some kind of explicit universe notation.

Look at the very old paper  by Robert Harper and myself: "Type
checking with universes" Theoretical Computer Science, 89:107-136,
1991 (file attached), where we give a detailed account of typical
ambiguity and type polymorphism (not the same thing) in a slightly
simpler system than the current CIC.

Randy
--
On Mon, Apr 18, 2011 at 9:51 AM, Vladimir 
Voevodsky<vladimir AT ias.edu>
  wrote:
Dear Carlos,

there is no need to introduce a new universe every time "Type" is mentioned. 
At the beginning of the file one declares the universe structure which one wants to 
work with by something like

Variable UU0 UU1 : Univ.

etc.

(of course currently there is no identifier Univ and also Univ is not a type. 
May be one should use something other than : with Univ.)


Then  one can have a definition like that:

Definition iscontr {U:Univ}(T:U) : U := ....

which is polymorphic or like that

Definition trrr (T:UU0):UU0 :=

which assumes a fixed universe UU0.


Vladimir.




On Apr 16, 2011, at 10:26 AM, Carlos Simpson wrote:

Dear Vladimir,
  It may be an interesting theoretical question to try to understand
what happens if we try to make all definitions parametric over universes.
Of course each time you make a new definition this introduces possibly many
new universe indices. It could have something to do with quantum mechanics
in that the ``universes'' which occur here might be related to the
``universes'' in the many-universe interpretation of quantum mechanics.
---Carlos Simpson


Selon Vladimir 
Voevodsky<vladimir AT ias.edu>:

Uhhh-uhh. I see. I got so used working with fixed universes that I forgot
about this behavior. Thanks! V.

On Apr 15, 2011, at 7:24 PM, Tom Prince wrote:

On 2011-04-15, Vladimir Voevodsky wrote:
In the following example:

File 1 (ex1.v) :

Definition dneg (X:Type) := ((X ->  Empty_set) ->  Empty_set).


File 2 (ex2.v):

Require Export ex1.
Variable X:Set.
Check (dneg X).
Check ((X ->  Empty_set)->  Empty_set).


Coq responds that (dneg X) is in Type while ((X ->  Empty_set)->  Empty_set)
is in Set. This does not look right.

This is expected. Everything in Set is also in type, so

Check ((X ->  Empty_set)->  Empty_set) : Type.

Unfortunately, coq doesn't currently support looking through the
definition of dneg to see that (dneg X) is convertible with a term of
sort Set.

There is limited support for doing this with paramaters of inductives,
but nothing else.

Tom










--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/



Archive powered by MhonArc 2.6.16.

Top of Page