[Agda] COMPILED_DATA directive for Maybe

[Dan Doel]

On Monday 23 November 2009 4:35:09 pm Nicolas Pouillard wrote:
> > Why Maybe {zero} is the Haskell one? It seems each Maybe {a : Level}
> > could be.
> 
> Maybe I understand this wrong but for me Maybe {zero} is a type (Set0)
>  which classifies values, whereas Maybe {suc zero} is a Set1 which
>  classifies types. Moreover in Haskell sorts classify types and sorts are
>  only made of * (Star) and arrows (I mean without the fancy GHC
>  extensions).

Well, things aren't quite so simple. Set1 doesn't just contain types, it 
contains datakinds, so to speak. And moreover, some Agda types are forced into 
Set1 when they are able to live in * due to a moderate level of 
impredicativity in the Haskell type system (assuming higher-rank types). For 
instance:

  data Step a s = Done | Yield a s

  data Stream a where
    Unfold :: forall s. s -> (s -> Step a s) -> Stream a

Stream a :: * in Haskell, but in Agda, it must be at least Set1, because the 
existential (if you want to call it that) quantification over the Set 's' will 
require it.

Of course, there are also Set1s that won't make sense as *s in Haskell, 
impredicativity or no. But the issue is somewhat tricky.

I think I'd agree with what Andreas Abel said, though. I wouldn't expect to be 
able to do computationally relevant case analysis on universe levels; I'd 
expect them to be used parametrically. I've been fooling with implementing 
Agda-like universe polymorphism, but the only way I've built in to my systems 
to eliminate levels (so to speak) is with the Type/Set family. Of course, I've 
allowed elimination *into* Levels, which could cause the same weirdness, I 
suppose.

On a tangent (in reference to the last universe polymorphism thread), I'd say 
that after having read some of the little there is out there on universe 
polymorphism, the ability to do at least some explicit handling of universes 
is desirable (not that anyone was suggesting otherwise). Making it completely 
implicit, as in Coq, seems to lead to universe consistency being non-local and 
non-composable, which is undesirable. I suppose it may be that the function-
level may not be the right place for it, though. But then again, Agda's 
current setup has some appeal, as universe polymorphic functions are first-
class:

  build : {i : Level}{A : Set i}
        -> ({j : Level}{R : Set j} -> (A -> R -> R) -> R -> R)
        -> List A
  build k = k _::_ []

I'm not sure if the above is typically supported or not. It may not even be 
useful in practice. But it looks pretty cool. :)

-- Dan