[Agda] Universe polymorphism in the standard library

[Nils Anders Danielsson]

On 2009-11-19 18:33, Luke Palmer wrote:
> I notice that a decent amount of the standard library is not
> using universe polymorphism.  Is there a reason for this, or is it
> just that nobody has got a round tuit?

The current mechanism for universe polymorphism is experimental, and I
do not know if it is likely to change in the future, hence work put into
a conversion could be wasted. However, I really dislike having several
pieces of almost identical code, so I have started to convert the parts
of the library where I felt it was most urgent (for me).

I have noticed some potential problems with the current approach to
universe polymorphism:

* There is currently no automatic lifting, so when defining data types I
  have chosen to use distinct level indices for every type parameter.
  Consider the following example:

    data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
      _,_ : (x : A) (y : B x) → Σ A B

  If lifting was automatic I would probably have used the following
  definition instead:

    data Σ {ℓ} (A : Set ℓ) (B : A → Set ℓ) : Set ℓ where
      _,_ : (x : A) (y : B x) → Σ A B

  If automatic lifting is later implemented the definitions can be
  simplified, but this means extra work.

* Typically it is not enough to change data type definitions, one also
  needs to update the type signatures of relevant functions. This can be
  quite tedious, and the type signatures become less readable. A more
  implicit approach to universe polymorphism could be beneficial.

> I'd be happy to start converting things if the latter.

Library contributions are welcome, see the README. I am currently in the
process of generalising Relation.Binary (but I am stuck due to a bug),
so you may want to focus on other parts of the code.

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.