coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. =)
- [Coq-Club] newbie question concerning types, Matej Kosik
- Re: [Coq-Club] newbie question concerning types, Adam Chlipala
- Re: [Coq-Club] newbie question concerning types, Tillmann Rendel
- Re: [Coq-Club] newbie question concerning types, Lauri Alanko
- Re: [Coq-Club] newbie question concerning types, Adam Chlipala
Archive powered by MhonArc 2.6.16.