Stream: Coq users

Topic: Universe Polymorphic Data Types

view this post on Zulip Gregory Malecha (May 17 2024 at 21:51):

A long time ago (I can not find the thread), there was some discussion of making a library of universe polymorphic data types with some infrastructure around them. At BedRock Systems, we have recently released some of our code around this in support of a robust, universe polymorphic monads library. At the moment, this library is focused on programming rather than proving so there is not much theory to go along with these, though the theory will generally be the same as Coq's theory.
The library is available here: https://github.com/bedrocksystems/BRiCk/tree/master/coq-upoly
We welcome contributions and comments, especially from experts on universe polymorphism.
Thanks to @Yannick Zakowski for getting me justification for getting this library released.

view this post on Zulip Meven Lennon-Bertrand (May 20 2024 at 09:59):

I believe this was the thread in question? In any case, thanks for making this open!

view this post on Zulip Yannick Zakowski (May 21 2024 at 07:16):

Thanks a lot again @Gregory Malecha !
I got side tracked by a couple of deadlines, but I'll get back to my experiment of porting itrees/vellvm and surroundings to stdpp soon, and will try building on coq-upoly doing so!

view this post on Zulip Gregory Malecha (May 22 2024 at 14:42):

Let us know if you have suggestions.

view this post on Zulip Thomas Lamiaux (May 22 2024 at 16:37):

For CUDW Nicolas wants to

(Nicolas) implementation of a sort and universe polymorphic standard library

view this post on Zulip Gregory Malecha (May 22 2024 at 19:32):

From BedRock, @Janno is attending, but he is aimed at a different project more in the kernel.
It would be great to have some cohesion here, but it depends on the goals of the project. Our library uses different conventions to the Coq standard library. I do feel like an update to the standard library with these new features could be a good time to break some compatibility in the name of modernizing the conventions, but that may hinder adoption. I'm sure David Swasey would be interested in discussing some of the thoughts for the future here if that would be of interest.

view this post on Zulip David Swasey (May 23 2024 at 15:01):

I'm sure David Swasey would be interested in discussing some of the thoughts for the future here if that would be of interest.

I'd be happy to help (but will not be attending CUDW).

Last updated: Oct 13 2024 at 01:02 UTC