[Agda] Universe polymorphism

[Ulf Norell]

The development version now has (very experimental) support for
(non-uniform) universe
polymorphism. At this stage there's no lifting between levels, but you can
get quite far
without that. Some examples are in test/succeed/UniversePolymorphism.agda.

Happy hacking!

>From the release notes:

  To enable universe polymorphism give the flag --universe-polyorphism
  on the command line, as an OPTIONS pragma (recommended) or set it in
  the emacs mode options.

  When universe polymorphism is enabled Set takes an argument which is
  the universe level. For instance, the type of universe polymorphic
identity
  is

    id : {i : Level}{A : Set i} -> A -> A

  The type Level is isomorphic to the unary natural numbers and should be
  specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:

    data Level : Set where
      zero : Level
      suc  : Level -> Level

    {-# BUILTIN LEVEL     Level #-}
    {-# BUILTIN LEVELZERO zero  #-}
    {-# BUILTIN LEVELSUC  suc   #-}

  There is an additional BUILTIN LEVELMAX for taking the maximum of two
  levels:

    max : Level -> Level -> Level
    max  zero    m      = m
    max (suc n)  zero   = suc n
    max (suc n) (suc m) = suc (max n m)

    {-# BUILTIN LEVELMAX max #-}

  The non-polymorphic universe levels Set, Set₁, .. are sugar for Set zero,
  Set (suc zero), ..

  At present there is no way to lift types from one level to another, that
  is, there is no function

    lift : {i : Level} -> Set i -> Set (suc i)

  This is likely to change at some point.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20090925/856c17d9/attachment-0001.html