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
19 stars 11 forks source link

New explanation about template universe polymorphism #34

Closed lephe closed 2 months ago

lephe commented 3 months ago

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

lephe commented 2 months ago

Gentle ping. I added the main contributors field from #36. Is there anything else I should do?

thomas-lamiaux commented 2 months ago

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:

  1. I review it
  2. after changes, we merge it without waiting for completion with further content
  3. we create issues "intro tuto" and "complete the trade of" ?

Does that sound good to you ?

lephe commented 2 months ago

Ah, perfect, thanks for the process. This sounds good to me.

lephe commented 2 months ago

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?

thomas-lamiaux commented 2 months ago

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

lephe commented 2 months ago

Pushed things. I've addressed all comments so far except for:

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 ?

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.

Explain somewhere that whenever Type is used, then a new variable is created or sth and the universe constrains. Maybe add a Print Universes Subgraph (lazyT.u0 lazyT.u1).

I'll have to look up what happens exactly as I don't know directly.

Should there be examples [of tricks to bypass limitations of template universe polymorphism] ?

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.

thomas-lamiaux commented 2 months ago

Moving further, I suggest fixing the last tiny issues, then merge it. It does not matter if it not perfect

thomas-lamiaux commented 2 months ago

@lephe Have you had time to progress ? I would like to merge it soon

lephe commented 2 months ago

I can do the next (supposedly last) pass tomorrow.

thomas-lamiaux commented 2 months ago

Ok sounds good to me. I'll merge it and then create issues to improve it

lephe commented 2 months ago

@thomas-lamiaux Ready to merge if nothing major remains.