coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Eelis van der Weegen" <eelis AT eelis.net>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club][8.1beta] Sort-polymorphism propagation
- Date: Fri, 21 Jul 2006 19:33:10 +0200 (CEST)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
In Coq 8.1beta, sort-polymorphism on inductive families was added. list is
now of type Type->Type, which used to be Set->Set. We can now have a (list
Set) of type Type, while (list nat) remains of type Set as before.
Personally I think this is pretty neat.
In Coq 8.0 I used the following definition for length-limited lists:
Definition lim_list (limit: nat) (A: Set) := { l: list A | length l <=
limit }.
This still works, but it does not allow us to make a limited-length list
of Sets. I figured it would be nice to update lim_list to cover list's
newfound genericity by changing "Set" to "Type", corresponding to what was
done for list itself:
Definition lim_list (limit: nat) (A: Type) := { l: list A | length l <=
limit }.
This definition is accepted and we can now make for example (lim_last 5
Set) of type Type. However, it appears the sort-polymorphism has been
lost: (lim_list 3 nat) is now also of type Type, while we would have
wanted it to be of type Set.
This leads to my first question: is it possible to define a family of
limited-length lists similar to lim_list above, but in such a way that it
benefits from the same sort-polymorphism that list now features?
My second question involves the display of sort-polymorphic types. Consider:
Inductive X (A: Type): Type := x: A -> X A.
Definition Y := X.
Check X.
Check Y.
For both X and Y, Check displays Type->Type. However, the following tests
reveal that the types of X and Y are not quite that identical, as X's
sort-polymorphism has been lost in Y:
Definition test1: Set := X nat. (* ok, accepted by Coq *)
Definition test2: Set := Y nat.
(* Error: The term "Y nat" has type "Type" while it is expected to
have type "Set" *)
This leads to my second question: Is there a way to make visible this
difference between the types of X and Y?
Regards,
Eelis
- [Coq-Club][8.1beta] Sort-polymorphism propagation, Eelis van der Weegen
Archive powered by MhonArc 2.6.16.