When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type property in ML)? Or are they just the result of arbitrary heuristics? Or something in between?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
7
It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:
Matthieu Sozeau and Nicolas Tabareau: Universe Polymorphism in Coq, Interactive Theorem Proving - 5th International Conference, ITP 2014
Beta Ziliani & Matthieu Sozeau: A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading, ACM SIGPLAN International Conference on Functional Programming 2015.
answered Feb 4, 2019 at 10:13
-
-
$\begingroup$ Then you get a combinatorial explosion and your computer releases blue smoke. Also, if the downvoter would care to explain the downvote, I could improve the answer. I know it's terse, but this really is not the place for a general introduction on how universe constraints are handled. $\endgroup$ Feb 4, 2019 at 13:00
-
$\begingroup$ Assuming I have a very good ventilation and that I omit the simplifications, will a distant descendant of mine get the most general universe and constraint assignment? $\endgroup$– BobFeb 4, 2019 at 13:15
-
2$\begingroup$ You might also want to mention "Type Checking with Universes" by Harper and Pollack; this is what Coq's algorithm is based on. $\endgroup$ Feb 5, 2019 at 17:29
-
3$\begingroup$ According to link.springer.com/chapter/10.1007/3-540-50940-2_39 "We show type synthesis is effective in CCω. Even if explicit universe levels are erased from a term it is possible to compute a “schematic type” for that term, and a set of constraints, that characterize all types of all well-typed instances of the term. " So I suspect there is in fact a "most general" set of universes and constraints, or perhaps multiple equivalent sets. $\endgroup$ Feb 5, 2019 at 17:33