Universes [Re: [Agda] COMPILED_DATA directive for Maybe]

[Andreas Abel]

Dan Doel wrote:
> On Tuesday 24 November 2009 7:40:04 am Nils Anders Danielsson wrote:
>> On 2009-11-23 22:24, Dan Doel wrote:
>>>   build : {i : Level}{A : Set i}
>>>         -> ({j : Level}{R : Set j} -> (A -> R -> R) -> R -> R)
>>>         -> List A
>>>   build k = k _::_ []
>> Do you have any interesting use cases for build in the absence of
>> parametricity?
> 
> Not off the top of my head. As I said, I had only thought about using them 
> parametrically. The interpreter I've been experimenting with would let you 
> write things of type Level -> Level, but those could only look like:
> 
>   \i j -> max(i + 2, j + 3)
> 
> Where + and max(..) are built-in formers of levels. Of course, any level 
> dependency could be mimicked by writing inject : Nat -> Level, and doing 
> whatever case analysis you want on the Nat.
> 
> It also occurred to me that build might not show off what seems unique to me 
> about Agda's universe polymorphism, so instead consider:
> 
>   contrived :  ({j : Level} {A : Set j} -> A -> List A -> List A)
>             -> ({j : Level} {A : Set j} -> List A)
>             -> List (Set 1) * List (Set 2) * List (Set 3) * List (Set 4)
>   contrived c n = (c (Set 0) n, c (Set 1) n, c (Set 2) n, c (Set 3) n)
> 
> As its name suggests, this function is silly. However, it shows how a single 
> function can accept a universe polymorphic function, and use it as several 
> different levels. I'm not sure if most other systems can handle this, but I 
> wouldn't be surprised if they can't. Then again, I don't have an example of a 
> useful function like this. :)
> 
> Another thing I'd been considering that one can't even do in Agda's current 
> implementing is something like:
> 
>   Σ i:Level. Σ A:Set i. A
> 
> which is, roughly, a (tagged) union of all types. You can't write it in Agda 
> because it can't be built with the normal universe-polymorphic sigma type, and 
> writing this type specifically requires one to specify its type, which is   
> Set ω, but you're not allowed to talk directly about that. Of course, I don't 
> have any interesting use cases of this type, either. :)

Such a type could be useful when interpreting Agda (without Set-omega) 
in Agda (with Set-omega).  Any term of object-level Agda lives inside 
this meta-level Agda type.

The above examples are all fine wrt. to universe polymorphism.  I think 
this is the style we want, maybe with some sugar on the outside.

To be a bit more precise what I mean by parametricity is that your 
"build" may not depend on i:Level, so there cannot be a pattern match 
against i (except matching against a variable, of course).  Thus, Level 
needs to be an irrelevant type here, and what that means is described in 
Frank Pfennings LICS'01 paper and in Barras and Bernardo's Fossacs 08 
paper on ICC^*.  I have a prototype implementation of irrelevant 
abstraction in MiniAgda, however, it does not have universes.  I'd like 
to work out the Agda-specific meta theory of irrelevance when I get to it...

Non-parametric universe dependency is also useful, for modelling the 
Agda universe hierarchy in Agda by induction on the level.   But I deem 
dependently type programming (and erasure/extraction) more important 
than this small feature, so I advocate a parametric universe polymorphism.

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/