Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] newbie question concerning types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] newbie question concerning types


chronological Thread 
  • From: Adam Chlipala <adamc AT hcoop.net>
  • To: Matej Kosik <kosik AT fiit.stuba.sk>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] newbie question concerning types
  • Date: Sun, 10 May 2009 07:14:26 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Matej Kosik wrote:
In Coq, the `list' function has the type `Type -> Type'. This means that
whenever apply some value whose type can be converted to `Type', I will
get a value whose type is `Type'.

[...]

There is, however, one thing I do not understand. How could the type of
the whole term (`list nat' or `list bool') be `Set' instead of `Type' as
the type of the `list' function suggests?

The answer involves the fact that [list] isn't really just a function. Coq includes a kind of fake, "template-style" universe polymorphism, where inductive definitions are effectively copied automatically to make it possible to use [Set] instead of [Type] in some places. The Coq type-checker automatically detects opportunities to do this.

I looked quickly for a reference to this in the manual but didn't find one, so I hope my description of the feature is accurate. =)





Archive powered by MhonArc 2.6.16.

Top of Page