Universe dependency [Re: [Agda] COMPILED_DATA directive for Maybe]

[Andreas Abel]

On Nov 23, 2009, at 1:50 PM, Nils Anders Danielsson wrote:
>
> If the universe polymorphism was uniform, then I believe it would be
> possible to map all variants of Maybe to the Haskell Maybe type.
> However, an Agda program can treat Maybe {zero} and Maybe {suc zero}
> differently, so this is not possible.

So actually, it is not universe polymorphism (like in System F  
polymorphism), but universe dependency.  This was my smartass comment  
for today.

But seriously, since universe levels are only there to check  
termination, they should be eraseable, just like the size indizes in  
sized data types.  If that is not the case, one might want to go back  
and rethink the design of universe handling...




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