Stream: Coq devs & plugin devs

Topic: Sort polymorphism plans


view this post on Zulip Jason Gross (Apr 16 2023 at 20:27):

@Pierre-Marie Pédrot Do your plans for sort polymorphism include the ability to write a "sort case" operator? e.g., I define #[sorts(polymorphic)] Definition foo@{s\in sort{SProp,Prop,Type} } := sort_match s with SProp => bar | Prop => baz | Type => qux end or something? (I'm thinking about how to replicate match notation without needing higher-order/non-prenex sort-polymorphism. Though I don't see any theoretical obstacle to having higher-order/non-prenex sort polymorphism.)

view this post on Zulip Karl Palmskog (Aug 01 2023 at 07:10):

Sort polymorphism (slated for 8.19.0) was discussed extensively at the Coq Workshop session with the Coq Team.

If I understand correctly, sort polymorphism is a solution to some problems preventing wider application of (1) SProp and (2) universe polymorphism. However, for all of these to be widely used in practice, there needs to be library support, specifically universe/sort polymorphic definitions of products/sums/lists, etc. And as of right now, nobody has announced plans to change Stdlib for this or to introduce an alternative to Stdlib that has these properties.

view this post on Zulip Matthieu Sozeau (Sep 22 2023 at 10:15):

@Karl Palmskog that update of the stdlib to use polymorphism everywhere is part of an experiment to handle algebraic universes more uniformly I’m doing. This is not entirely orthogonal to sort polymorphism, so I hope to attract Pierre-Marie to help with this ;)

view this post on Zulip Karl Palmskog (Sep 22 2023 at 10:18):

@Matthieu Sozeau sounds good, but as you can see here, there is significant demand from the community to get access to this kind of code in reusable form. Maybe you can think about whether it could be packaged for reuse on opam, etc.

view this post on Zulip Karl Palmskog (Sep 22 2023 at 10:20):

coordination with similar efforts might be expensive, so at this point I think we'd just like to see more options for practically using various polymorphic definitions, even if those options are competing/incompatible


Last updated: Nov 29 2023 at 21:01 UTC