[Agda] COMPILED_DATA directive for Maybe

[Nicolas Pouillard]

Excerpts from Andrés Sicard-Ramírez's message of Mon Nov 23 17:20:35 +0100 2009:
> Nicolas,
> 
> On Mon, Nov 23, 2009 at 10:31 AM, Nicolas Pouillard
> <nicolas.pouillard at gmail.com> wrote:
> > Excerpts from Nils Anders Danielsson's message of Mon Nov 23 13:50:09 +0100 2009:
> >> On 2009-11-22 23:05, Andrés Sicard-Ramírez wrote:
> >> > Any ideas how to define a COMPILED_DATA directive for the (new)
> >> > universe polymorphic datatype Maybe defined in Data.Maybe.Core?
> >>
> >> 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. If you want to interoperate with
> >> the Haskell Maybe type, then I suggest that you define a
> >> non-universe-polymorphic variant of Maybe in Foreign.Haskell.
> >
> > Could we export Maybe {zero} which is really the Haskell one. It would
> > be nice to don't have to redefine a new one.
> >
> 
> 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).

-- 
Nicolas Pouillard
http://nicolaspouillard.fr