[Agda] Universe polymorphism in the standard library

[Nicolas Pouillard]

Excerpts from Nils Anders Danielsson's message of Fri Nov 20 16:20:57 +0100 2009:
> 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.

I've started with 'List', and on the way I've changed 'Maybe'. I've left
some functions at level Set, since the dependencies was too large. I will
come up with patch soon.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr