[Agda] Universe polymorphism in the standard library

[Andreas Abel]

On Nov 20, 2009, at 4:20 PM, Nils Anders Danielsson wrote:
> 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.

Should be implemented sooner rather than later.

> * 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.

My words at AIM, but I could not convince Ulf that this is not a  
problem, since there is already an implementation that resolves level  
constraints in the sized types module.  Too bad you were not there at  
the workshop, maybe you can still convince Ulf.

Cheers,
Andreas



Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41