Stream: Coq devs & plugin devs

Topic: Why are native arrays universe polymorphic?


view this post on Zulip Chantal Keller (Nov 08 2021 at 16:06):

Hi
Why are native arrays universe polymorphic?

view this post on Zulip Guillaume Melquiond (Nov 08 2021 at 16:07):

To allow for arrays of arrays?

view this post on Zulip Enrico Tassi (Nov 08 2021 at 16:09):

Do you face a bug?

view this post on Zulip Pierre-Marie Pédrot (Nov 08 2021 at 16:10):

@Guillaume Melquiond you don't need polymorphic arrays to nest them

view this post on Zulip Pierre-Marie Pédrot (Nov 08 2021 at 16:11):

this is because 1. you might want to store stuff that lives in various levels, and 2. monomorphic constraints in the kernel are a real plague

view this post on Zulip Chantal Keller (Nov 08 2021 at 16:15):

Thanks for your answers.
So for instance, I want to define a constr which is a native array, at the OCaml level. What is the first argument I should give to mkArray?
@Enrico Tassi indeed, I face "universe inconsistency" when switching a development based on non universe polymorphic arrays to native arrays, but it is very difficult to make a small example...

view this post on Zulip Karl Palmskog (Nov 08 2021 at 16:16):

I think we are very firmly in the Coq plugin dev and Coq dev territory here

view this post on Zulip Notification Bot (Nov 08 2021 at 16:17):

This topic was moved here from #Coq users > Why are native arrays universe polymorphic? by Karl Palmskog

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 16:24):

are you working with econstr or constr?

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 16:24):

what's the type of the elements of the array?

view this post on Zulip Chantal Keller (Nov 08 2021 at 16:25):

Hi Gaëtan

  1. Both
  2. Some inductive type

view this post on Zulip Guillaume Melquiond (Nov 08 2021 at 16:27):

I guess you could pass it the result of Evd.fresh_array_instance, if you are working at the econstr level.

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 16:27):

the type of the type of the elements is some universe
if it's a level use that
if it's algebraic you need to generate a fresh level and constrain it to be higher

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 16:29):

if using fresh_array_instance you will need to use Typing.type_of on the generated array term (or on the type array@{u} (some inductive type)) so that the right constraints get generated

view this post on Zulip Chantal Keller (Nov 08 2021 at 16:31):

Ok, thanks a lot for these explanations. I will get back to you if I run into a problem.


Last updated: Feb 05 2023 at 22:03 UTC