[Agda] COMPILED_DATA directive for Maybe

[Dan Doel]

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. :)

Cheers,
Dan