[Agda] More universe polymorphism

[Gabriel Scherer]

Guillaume Brunerie wrote:
> I think that what makes universe management painful in Agda is not the
> explicit universe polymorphism but rather the lack of cumulativity.
> For instance when you define Sigma-types in the most polymorphic way,
> you need two different universe levels and the Sigma-type ends up in
> the max of the two levels. With cumulativity you could have only one
> level.

Do not expect wonders by just trading one source of impliciteness for
another.

My understanding of typical ambiguity is essentially the application
of ML-style type inference to universe level polymorphism: abstraction
over universe levels and instantiation to specific levels
(possibly re-generalized afterwards) are both explicit. You are
suggesting a system where abstraction and instantiation are explicit,
and in exchange universe subtyping is implicit. (Nobody really dares
to ask for both because it's well-known that inferring both
polymorphism and subtyping at the same time is a Pandora's box¹)

My humble guess would be that in such a system, some people would
still complain about implicitness being an issue in some cases. I can
see why it's attractive to be explicit about abstraction
(something everybody likes and therefore appreciates to think about
during its development, despite the notational pain), but soon enough
you'll have users complaining that depending on a single biggest
universe level is too coarse-grained, and that it's more aesthetically
pleasing to them (or better suited to their view of size problems) to
be precise on levels on the library-side, instead of forcing users to
lose precision by using subtyping:
  (forall i j . Set{i} -> Set{j} -> Set{max(i,j)} * Set{j})
would be a much better type than
  (forall k . Set{k} -> Set{k} -> Set{k} * Set{k})

¹: Matthieu Sozeau's recent work on universe polymorphism for Coq does
show signs of lack of principality problems
  http://mattam.org/research/publications/Universe_Polymorphism_and_Inference_in_Coq-TYPES13-250413.pdf

Regarding the discussion as whole, I will put my old-school ML-level
type-system engineer hat to remark that it's maybe not really an issue
if some types don't themselves have types. In Fω, types are classified
by kinds that are not types. In dependent systems we've been used to
the "merged layers" view where everyone pretends to be a type, but
I don't find it particularly problematic that this illusion falls at
the edge. We can have a Setω kind to classify universe-polymorphic
types, that is not itself a type. We could make it a type by adding
a Set{ω+1} kind that is not itself a type, etc.

In the basic Martin-Löf type theory (as described eg. in
http://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory ),
it is convenient to give the syntax (Γ ⊢ A : Type) to the judgment
saying that A is a well-formed type, but that doesn't make the Type
kind itself well-typed, so A may not "have a type". Similarly for the
(Γ ⊢ M : *) in the original Calculus of Construction articles: * does
not have a type.

(Of course that is orthogonal to the ongoing technical discussion
about what Agda precisely implements and the interest of a precise
formalization of it.)

On Sat, Jun 29, 2013 at 2:00 AM, Guillaume Brunerie
<guillaume.brunerie at gmail.com> wrote:
> Martin Escardo wrote:
>> I show below that, in the presense of universe levels, there is an
>> Agda type that doesn't have any Agda type.
>> [...]
>> Indeed, there is something fishy about having a type of universe
>> levels,
>> [...]
>> I would rather have typical ambiguity in Agda,
>
> There is a much shorter example of a type that doesn’t have a type:
>
> -- Works
> x : (i : Level) -> Set (lsucc i)
> x = \ i -> Set i
>
> -- Fails
> X' : ?
> X' = (i : Level) -> Set (lsucc i)
>
> But I don’t see a problem with that, I’m perfectly happy with the fact
> that not every type is small. I would even say that it would seem
> fishy to me if everything was small.
> Moreover, when I started using Agda I already knew a bit of Coq, and I
> found Agda’s explicit universe polymorphism much easier to understand
> than Coq’s typical ambiguity. It’s more painful to use, but at least
> you understand what you’re doing.
> To give a concrete example, here are three mathematical theorems (most
> likely formalizable in type theory)
>
> 1) The category of sets is complete
> 2) Every *small* complete category is a preorder
> 3) The category of sets is not a preorder
>
> In a system with typical ambiguity, the smallness condition is
> completely invisible so instead of 2) you can only state and prove the
> following:
>
> 2') Every complete category is a preorder
>
> Of course, 1) + 2') + 3) looks inconsistent, but it’s only when you
> try to prove false from them that you get the "Universe inconsistency"
> error.
> With explicit universe polymorphism, you can express smallness so
> there is no problem, nothing looks inconsistent.
> If you look closely at the HoTT book, you will find a few places where
> we switch back to explicit universe management because typical
> ambiguity is not precise enough.
>
>> 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.
>
> Just to make sure there are no misconceptions, it’s not correct to say
> that the notion of universe level is a meta-level concept in homotopy
> type theory. We indeed decided to use typical ambiguity in the HoTT
> book, but we could just as well have used Agda-style universe
> polymorphism. Homotopy type theory has nothing to do with universe
> management.
>
> Also if you prefer you can call "type" every Agda term whose Agda type
> is Set i for some i : Level, and "metatype", or "framework type" for
> every other Agda type. Then call "term" every Agda term whose Agda
> type is a "type" and "template", or "macro" every Agda term whose Agda
> type is a "framework type".
>
> So universe management is still somehow part of the meta-level, except
> that one layer of this meta-level is also implemented in Agda.
>
>> Moreover, ignoring the above, explicit universe levels as in Agda are
>> painful
>
> I think that what makes universe management painful in Agda is not the
> explicit universe polymorphism but rather the lack of cumulativity.
> For instance when you define Sigma-types in the most polymorphic way,
> you need two different universe levels and the Sigma-type ends up in
> the max of the two levels. With cumulativity you could have only one
> level.
> Similarly, if you have a module where you don’t have to raise any
> universe level, you could just parametrize your module by a universe
> level `i` and use `Set i` everywhere. That’s not more painful than
> --type-in-type and you have the added bonus that you can express
> smallness conditions when you need to.
>
>> (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.)
>
> It seems pretty straightforward to give a set-theoretic model of MLTT
> + Agda’s explicit universe polymorphism.
> In what follows I’m working in ZFC + enough inaccessible cardinals.
>
> There are two different kind of things: types and terms (not every
> type being a term of some universe).
> Every type is interpreted as a family of sets (parametrized by the
> context) and every term as an dependent element of the interpretation
> of its type.
> The type of universe levels is interpreted as the set of natural numbers N.
> The operations lzero, lsucc, lmax as interpreted in the obvious way.
> The type family (i : Level) |- Set i  is interpreted as the sequence
> (V_{\kappa_n})_{n\in N} where \kappa_n is the nth inaccessible
> cardinal.
> Everything else is interpreted as usual.
> Note that there is a notion of Pi-type in every fixed universe but
> there is also a notion of Pi-type for a not necessarily small family
> of types (this is necessary for the type (i : Level) -> Set (lsucc i)
> to make sense).
> Semantically they are both interpreted in the obvious way.
>
> In this model, a type is small when its rank is < sup(\kappa_n). But
> for instance the type (i : Level) -> Set (lsucc i) is interpreted as a
> set of rank sup(\kappa_n), so it’s a type which is not small, but
> there is no problem.
>
> One can also get a similar hand-waving model for the kind of universe
> polymorphism I was sketching in my first message.
>
> Let’s assume that there is a 1-inaccessible cardinal L (that means
> that L is the L-th inaccessible cardinal).
> The type of universe levels is interpreted as L.
> The type family (i : Level) |- Set i is interpreted as above, as
> (V_{\kappa_\alpha})_{\alpha\in L} where \kappa_\alpha is the \alpha-th
> inaccessible cardinal.
> The operations lzero, lsucc and lsup are interpreted in the obvious
> way. Note that a small type is of rank < \kappa_L = L, hence of
> cardinality < L. Hence any small collection of elements of L has a sup
> in L, so lsup is well-defined. Also, the type of universe levels
> cannot be small.
> Everything else is interpreted as usual.
>
> This is really sketchy but maybe it’s enough to convince you that
> there should not be any inconsistency.
>
> Guillaume
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda