3
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:

Improve this answer
$\endgroup$
7
  • $\begingroup$ What if those simplifications are omitted? $\endgroup$
    – Bob
    Feb 4, 2019 at 12:12
  • $\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$
    – Andrej Bauer
    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$
    – Bob
    Feb 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$
    – Jason Gross
    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$
    – Jason Gross
    Feb 5, 2019 at 17:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.