[Agda] More universe polymorphism

[Martin Escardo]

I show below that, in the presense of universe levels, there is an
Agda type that doesn't have any Agda type.

That is, I write two definitions,

x : X
x = ?

X' : ?
X' = X

such that X type checks (with the hole filled) and X' doesn't (even
before we attempt to fill the hole).

Indeed, there is something fishy about having a type of universe
levels, as illustrated below by Agda code.

Because Guillaume raised the matter, I finally express my opinion
about this, which I had in the back of my mind for a long time.

I think the notion of universe level is (or ought to be) a meta-level
concept. At least this is so in Coq, in Homotopy Type Theory, and in
the patched version of Coq for Homotopy Type Theory.

http://homotopytypetheory.org/book/

I would rather have typical ambiguity in Agda, as first explained by
Feferman, and as automated by Bob Harper's algorithm. The HoTT book
nicely explains typical ambuiguity.

Moreover, ignoring the above, explicit universe levels as in Agda are
painful, to the extent that some people (e.g. Dan Licata and Mike
Shulman in their LICS'2013 paper in Agda) prefer to use type-in-type
to achieve universe polymorphism, checking themselves by *hand* that
there is a consistent universe level assignment for everything they
write down in Agda.

Any first class citizen in Agda ought to have a type. In particular,
any type ought to have a type.

I show below that, in the presense of universe levels, there is an
Agda type that doesn't have any Agda type.

(Moreover, how can one be sure that adding a type of universe levels
doesn't lead to logical inconsistency? What is shown below is not an
inconsistency, but I think is close to one.)

\begin{code}

module fishy-levels where

postulate Level : Set
postulate lzero : Level
postulate lsucc : Level → Level
postulate lmax  : Level → Level → Level

{-# BUILTIN LEVEL     Level  #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsucc  #-}
{-# BUILTIN LEVELMAX  lmax   #-}

\end{code}

By a universe I mean Set l where l is some level.

The natural numbers live in all universes:

\begin{code}

data ℕ {l : Level} : Set l where
   zero : ℕ
   succ : ℕ → ℕ

\end{code}

The natural numbers of any level live inside the type (of level zero)
of levels.

\begin{code}

newlife : {l : Level} → ℕ {l} → Level
newlife zero     = lzero
newlife (succ n) = lsucc(newlife n)

f : {l : Level} (n : ℕ {l}) → Set(newlife n)
f zero = ℕ
f (succ n) = Set (newlife n) → f n

\end{code}

The above type checks in Agda 2.3.2 and 2.3.2.1.

Using ctrl-c-ctrl-n to normalize, we get

f zero = ℕ
f (succ zero) = Set → ℕ
f (succ (succ zero)) = Set₁ → Set → ℕ
f (succ(succ (succ zero))) = Set₂ → Set₁ → Set → ℕ

But the following doesn't type check (of course):

\begin{code}

-- too-big : ?
-- too-big = {l : Level} (n : ℕ {l}) → Set(newlife n)

\end{code}

Uncomment to get the error "Setω is not a valid type".

That is, the type "{l : Level} (n : ℕ {l}) → Set(newlife n)" is too
big. But it is the type of the function f, which Agda accepts.

The point I am trying to make is that it doesn't make sense to have a
type of universe levels. Type levels ought to be meta-liguistic.

I suggest that Agda should move to typical ambiguity, using Harper's
algorithm. This would both solve this problem and make the Agda users'
lives easier, and Agda programs much more readable.

Best,
Martin


On 26/06/13 20:14, Guillaume Brunerie wrote:
> Hi all,
>
> Quick recall of Agda’s universe polymorphism:
>
> There is a type Level of universe levels together with the following constants:
>
> zero : Level
> suc : Level -> Level
> max : Level -> Level -> Level
>
> For every i : Level, there is a universe Set i, which is also a term
> of type Set (suc i).
> A dependent product (x : A) -> B x such that A : Set i and B x : Set j
> for all x : A is of type Set (max i j) (note that j cannot depend on
> x, it has to be uniform).
> Moreover, the type of universe levels Level is itself small (of type Type zero).
>
>
> Why is Level required to be small?
>
> If we drop this requirement, it seems to me that we could extend max
> so that we can get the maximum of any small family of universe levels,
> i.e. have some max2 of type:
>
> max2 : (i : Level) (A : Set i) (j : A -> Level) -> Level
>
> Then a dependent product (x : A) -> B x where A : Set i and B x : Set
> (j x) would be of type Set (max2 i A j), so there is no "uniformity of
> levels" restriction anymore, the only restriction is that the domain
> and the codomain(s) are small.
> You need the condition that Level is not small, or else you would be
> able to define the max of all levels, which is likely to cause some
> trouble.
>
> Such universe polymorphism would permit to define a lot of new
> universes, indexed by a lot of big countable ordinals (maybe up to the
> Feferman–Schütte ordinal?)
>
> Does that make sense? Is that consistent?
> Did I miss something obvious?
> I think there was something requiring Level to be small, but I don’t
> remember what it is.
>
> Guillaume
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>