New explanation about template universe polymorphism #34
Conversation
|
Gentle ping. I added the main contributors field from #36. Is there anything else I should do? |
|
Hi @lephe , it is going a bit slow because of the holiday. Considering the discussions we had on the zulip, I suggest the following steps:
Does that sound good to you ? |
|
Ah, perfect, thanks for the process. This sounds good to me. |
There was a problem hiding this comment.
I have looked at the tutorials, it is very interesting and a very good version on the subject. Thanks for the contribution.
Concerning the tutorial and the structure, I suggest to:
- Section is unclear and most of section 2 is an introduction to universes as
indicated by "Let's see this in action."
Hence, I suggest moving / merging all such content with Section 1.
Like everything which is not related to mprod and the limitations of using it.
Then dedicate section 2 to monomorphic and limitations - Maybe add subsections in section 3 and 4.
Like "Principles of (Template Poly // UnivPoly) / "advantages" / "limitations".
I think it will make a bit easier to read and easier to improve later on,
for a very little cost - It is not clear in section 2 what monomorphic means, maybe elaborate on it
- Maybe rework the intro to say this tuto discuss the two approaches, their advantages and limitations as it is the end goal. In which case, maybe mention it is a first version or sth ?
Otherwise sounds great !
| represents a universe level. | ||
|
|
||
| Here is the product of two types living in universe [uprod]. *) | ||
| Universe uprod. |
There was a problem hiding this comment.
If I write Print Universes Subgraph (uprod) here, I get Set < uprod, why is that ?
You mention later that we don't care but I still find it a bit confusing.
There was a problem hiding this comment.
All global universes are > Set.
Records of why this was decided are lost but AFAICT the main consequence is that they are prevented from being made = Set, which seems desired as if the user wanted a universe to be = Set they should have written Set not Type.
|
|
||
| All of this results in the following basic rule: wherever a type in universe | ||
| [Type@{j}] is expected, you can provide a type from any universe smaller | ||
| than [j], i.e. that lives in [Type@{i}] with [i <= j]. |
There was a problem hiding this comment.
Say in the sentence what is the point ?
|
|
||
| (** ** 2. Some issues with monomorphic universes *) | ||
|
|
||
| (** The core limitations of template universe polymorphism will be related to |
There was a problem hiding this comment.
It is unclear what monomorphic means
| (** Also, as we'll see later, Coq doesn't allow you to | ||
| name universes directly with a number (e.g. [Type@{42}]). So in order to | ||
| name a specific universe we have to create a variable [uprod] that | ||
| represents a universe level. | ||
|
|
||
| Here is the product of two types living in universe [uprod]. *) |
There was a problem hiding this comment.
| (** Also, as we'll see later, Coq doesn't allow you to | |
| name universes directly with a number (e.g. [Type@{42}]). So in order to | |
| name a specific universe we have to create a variable [uprod] that | |
| represents a universe level. | |
| Here is the product of two types living in universe [uprod]. *) | |
| (** Let us create a variable [uprod] representing a universe level. | |
| Here is the product of two types living in universe [uprod]. *) |
| max of two levels (e.g. [max(uprod, uprod+1)]). Counter-intuitively, we | ||
| cannot name a specific universe by number. *) |
There was a problem hiding this comment.
| max of two levels (e.g. [max(uprod, uprod+1)]). Counter-intuitively, we | |
| cannot name a specific universe by number. *) | |
| max of two levels (e.g. [max(uprod, uprod+1)]). Counter-intuitively, we | |
| actually cannot specify universes directly by numbers. *) |
| is called [Type@{Top.N}] or [Type@{JsCoq.N}] for some [N], depending on the | ||
| environment in which you're running this file). We could also instantiate | ||
| [prod] with propositions or sets and have it live in [Prop] or [Set]. *) | ||
| Check (fun (P: Prop) => P * P). |
There was a problem hiding this comment.
Not sure what is the point of this comment.
Plus Prop is complicated.
There was a problem hiding this comment.
Well, more examples that the universe of T * T depends on the universe of T.
| (** There are other constraints here but they're unrelated to the inconsistency | ||
| that we had with the monomorphic version. *) | ||
|
|
||
| (** So, problem solved, right? Nope! Because this only works with inductive |
There was a problem hiding this comment.
Sounds like you had a lot of issues with it 😆
| Definition pstate_lazy {S T: Type} (t: T) := | ||
| pstate_pure (S := S) (lazy_pure t). | ||
|
|
||
| (** Problem solved! ... well, assuming you are ready and able to re-define your |
There was a problem hiding this comment.
It sounds a bit bitter
| Fail Definition state_lazy {S T: Type} (t: T) := | ||
| state_pure (S := S) (lazy_pure t). | ||
|
|
||
| (** Tricks to bypass the limitations of template universe polymorphism generally |
There was a problem hiding this comment.
Should there be examples ?
There was a problem hiding this comment.
I'm not really familiar with these, I just know they exist.
There was a problem hiding this comment.
I suggest creating a subsection as you mentioned and leave it for further contributions
|
Thanks, I'll go through that! One point on which I need an expert's opinion is the status of template to full universe polymorphism. The latter is more expressive on paper, and I thought it was seen as superseding template polymorphism. I'd heard in particular of attempts to write a universe polymorphic standard library, suggesting that this was desirable. I indeed had issues with it. ^^" At some point in my last project I debugged universes for 20-30 hours, with some problems arising from the project itself, the others from template polymorphism in the standard library. Having to untangle these and sometimes purge standard types from sections was very painful (hence the slightly bad vibe, sorry—will fix). As of now this project still reimplements the product type btw, so I was truly writing under the assumption that template polymorphism was insufficient. Can anyone more involved with this stuff comment on how the relationship between these two types of polymorphism should be presented? Is template polymorphism really considered to be superseded by full universe polymorphism (either now or in the future)? Are there contexts in which it is specifically desirable to use one type of polymorphism over the other? Maybe some context about what the project's direction is? |
|
Not sure if it answers, no time to read it again but I am recalling https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Template.20vs.2E.20proper.20universe.20polymorphism.20tutorial/near/454897533 |
|
Pushed things. I've addressed all comments so far except for:
Hoping for more background, the post linked above goes into useful technical details but I'm still not sure whether template polymorphism is supposed to be superseded and used for legacy reasons + cases where univ poly blows up or whether these are really two parallel systems that are designed to exist concurrently.
I'll have to look up what happens exactly as I don't know directly.
I also don't know these very well. I just personally inline stuff. Gaëtan recently demonstrated how eta-expansion helps but it seems like the trick should be an entire section by itself. Which would be on topic, IMO. |
| (** ** 2. Some issues with monomorphic universes *) | ||
|
|
||
| (** The core limitations of template universe polymorphism are related to when | ||
| it _isn't_ polymorphic, so we can first demonstrate these issues on |
| index and avoid the bump, but it's not the case in general (e.g., the freer | ||
| monad or functor laws). *) | ||
|
|
||
| (** We can see this in a universe constraint if we bring them both in a single |
There was a problem hiding this comment.
I think it would be good here to explain a bit much how each constrains appear because it easy to get lost in the direction of the inequalities
| Definition lazy_pure {A: Type} (a: A): lazyT A := lazy (fun _ => a). | ||
| Print Universes Subgraph (lazy_pure.u0 lazyT.u0 lazyT.u1). | ||
|
|
||
| (** The core of the problem now shows up if we now happen to want products in |
There was a problem hiding this comment.
That is an example of how the issue arises, but it is not a very general comment.
Would you have a more general explanation for when this issues arise to add in complement just before ?
| (** Template universe polymorphism is a middle-ground between monomorphic | ||
| universes and proper polymorphic universes that allow for some degree of | ||
| flexibility. We can see it in action in the type of [prod] from the standard | ||
| library. *) |
There was a problem hiding this comment.
About prod is printed but there are no explanations, they come further.
I suggest adding a line or two to discuss the change here.
| Definition state (S: Type) := fun (T: Type) => S -> (S * T). | ||
| About state. | ||
|
|
||
| (** [state.{u0,u1}] correspond to the old [uprod]: the type of [T] is |
There was a problem hiding this comment.
Could you develop here, I have some trouble understanding what is the issue as the type of state is
prod : Type@{prod.u0} -> Type@{prod.u1} -> Type@{max(prod.u0,prod.u1)}
state : Type@{state.u0} -> Type@{state.u1} -> Type@{max(state.u0,state.u1)}
which to me looks like the same as prod and not mprod
There was a problem hiding this comment.
The difference is not in the type, it's in the annotation "X is template universe polymorphic" shown by About. This status affects the way instances of the definition are treated, and that's what makes the difference. I clarified.
|
Moving further, I suggest fixing the last tiny issues, then merge it. |
|
@lephe Have you had time to progress ? I would like to merge it soon |
|
I can do the next (supposedly last) pass tomorrow. |
|
Ok sounds good to me. I'll merge it and then create issues to improve it |
|
@thomas-lamiaux Ready to merge if nothing major remains. |
Discussed on Zulip: https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Template.20vs.2E.20proper.20universe.20polymorphism.20tutorial
The claimed scope, for now, is just an explanation of what template polymorphism does and doesn't do, with bridges around it to where the problem it solves come from (as explained with monomorphic universes) and how the limitations can be worked around (with universe polymorphism).
I think a detailed explanation of universes would be mostly independent so probably better separated. If such an explanation is written, linking to it could replace the current first section.
On the other hand, discussing other limitations of template universe polymorphism and better showing the tricks that can be used to hack around them would be, IMO, clearly in scope for this document. I could see a generalization to "more things about template polymorphism" more than to "more things about universes". The current text is still right at the limits of my understanding so I'm not really confident I can extend further.
Cc @YaZko