[Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")

[Andreas Abel]

Yes, this is the way to go, a core with explicit universe levels and an 
elaboration on top which gives you the conveniences.  What Agda misses 
at this point is

   - cumulativity
   - level inequality constraint solving
   - silent level generalization

It's on my agenda to make this work, but I don't know when I get to it.

--Andreas

On 02.07.2013 13:07, Matthieu Sozeau wrote:
>
> Le 1 juil. 2013 à 23:43, Guillaume Brunerie <guillaume.brunerie at gmail.com> a écrit :
>
>> On 2013/7/1 Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>>>
>>> On 01/07/13 20:16, Guillaume Brunerie wrote:
>>>>
>>>> Well, if you want to define a polymorphic function (polymorphic on all
>>>> small types, not restricted to some universe), you have to quantify
>>>> over all levels.
>>>> Or you can use typical ambiguity,
>>>
>>>
>>> I don't think this should be an "either or" situation. One should have an
>>> explicit understanding of what universes and levels are, and typical
>>> ambiguity should be a shorthand for making types and terms readable (very
>>> much like implicit-argument notation) by erasing levels that can be
>>> automatically inferred.
>>
>> Is there a way to mix explicit universe polymorphism with typical
>> ambiguity? I only know Agda where there is no typical ambiguity at all
>> and Coq where everything is implicit.
>> If there is a way to have the benefits of both I would like to see it.
>
> That's what I'm aiming for in my design for Coq. You start with a theory,
> à la Agda, where everything is explicit. In my version, universes are
> another kind of variables, as in Vladimir's proposed system, and judgments
> are relative to a set of constraints as well.
>
> Then typical ambiguity is just seen as an elaboration (Harper & Pollack style)
> that transforms terms with anonymous levels into terms with explicit
> levels. Of course you can also explicitly name universes directly
> in the source, e.g. to write down universe-polymorphic types.
> Implicit polymorphism relies on ML-style abstraction. It is implicitely
> a meta-level prenex quantification, not higher-rank, so you can't have
> nested (for all i : Level, …) quantifications. Additionally, to handle
> cumulativity you need to abstract on constraints as well. There is a
> straightforward interpretation from a term of non-polymorphic type in
> this explicit system to a term in the non-polymorphic theory (with
> just Type_n's), which just expands polymorphic definitions.
>
> The main issue in this system is not exactly one of principality,
> as constraints give you enough flexibility to get most general typings.
> However the inferred polymorphism is often more general than necessary,
> so you might not always want the most general types to be inferred.
> Typically, if you write a polymorphic term [t := id bool true] where
> [id_i : Π A : Type i, A -> A], elaboration will give you a
> judgment for [t_i' := id_i' bool true : A -> A] along with a
> constraint [0 <= i'] (bool : Type 0). The quantification on [i'] here
> is certainly unnecessary and you'd rather have it instantiated with [0].
> The proliferation of such quantifications is also an issue for
> readability and performance. To reduce these constraints or
> not is a type inference choice, basically deciding where to
> allow subtyping and where to use strict equality. If you are
> unhappy with the choice you can always explicitly say so, as
> user-introduced variables are not tempered with during simplification.
> As Gabriel mentioned it's already been encountered in e.g. Fsub and
> partial but practical solutions were used in that case as well.
> -- Matthieu_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/