search

coq / platform-docs

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
https://coq.inria.fr/platform-docs/
Other
16 stars 9 forks source link

Improve the discussions on TemplatePoly and UnivPoly #46

Open thomas-lamiaux opened 2 weeks ago

thomas-lamiaux commented 2 weeks ago

Improve the discussions on TemplatePoly and UnivPoly, in particular on performances https://github.com/coq/platform-docs/blob/main/src/Explanation_Template_Polymorphism.v

MevenBertrand commented 1 week ago

I have a few minor improvements (basically, typos, including one in the code), for now it's on a branch of mine here. I can open a PR if you want them.

The tutorial makes it sound like universe poly is strictly better than template poly in most (all?) cases. However, there is the caveat that template poly also extends to Prop and Set (and SProp, too, I think), but universe poly does not: you cannot replace a polymorphic universe by Prop. This is somewhat implicit in the tutorial, but might be better to make explicitly?

Also, this is the reason for the new and shiny sort polymorphism coming up starting in 8.19 (not sure this is worth mentioning at this point, but that means that the tutorial might need changes once sort poly is consolidated).

SkySkimmer commented 1 week ago

univ poly handles Set and sort poly handles Prop/SProp template poly does not handle SProp

MevenBertrand commented 1 week ago

I thought there were (used to be?) restrictions about replacing a universe poly variable with Set, but my bad!

thomas-lamiaux commented 1 week ago

Don't hesitate to make a PR if you have improvements. The tuto is a bit biased hence this issue, and we hope to improve over time with contributions