Universe polymorphism [Re: [Agda] AIM 10 notes]

[Conor McBride]

Hi Andreas

On 24 Sep 2009, at 16:22, Andreas Abel wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hi Conor,

> My opinion is to implement implicit cumulativity and explicit  
> parametricity.

My hope, too, is that something of that form should
work. But I do fear that we may not be able to make
cumulativity entirely implicit.

I also think it highly desirable that both be made
explicit in some internal language of readily checkable
evidence. (I hesitate to use the phrase "core theory"
for this as it is now used with other meanings.)

>> If I'm trying to solve
>>
>>  Nat : ?X
>>
>> I am not free to presume that ?X = Set, because
>> ?X = Set1 is also a solution.
>
> We would have
>
>  Nat : forall {i} -> Set i

Indeed. We want every universe to have a Nat, and we
want the (silent in public, we hope) embedding ^
from Set i to Set (i+1) to obey

   ^(Nat {i}) = Nat {i+1}

> In this case one should get
>
>   Nat : Set ?i
>
> with ?i an unconstrained level meta variable.  (Or just the trivial
> constraint ?i >= 0.)

Yes, but what about ?X ? Is ?X = Set ?i, or is
?X = Set ?j for some ?i <= ?j ?

After all, when we wrote

   Nat : ?X

we might have meant

   ^^^^Nat : ?X

> We have explicit polymorphism as in
>
>  List : forall {i} -> Set i -> Set i

I rather hope we might manage
   (a) a universe successor operator, allowing
         Set, Set', Set'', etc
   (b) silent outermost quantification over the
         lowest universe in play
   (c) an agreement to call the variable which
         stands for that universe "Set"

so we can write

   Nat : Set
   List : Set -> Set
   Set : Set'

and mean uniformly parametric statements about the
whole hierarchy.

But perhaps that's wishful thinking. Or perhaps it's
just Damas-Milner.

> Levels are made up from variables, zero, and successor.  Constraints  
> are
> of the form
>
>  ?i + n <= ?j
>  ?i <= ?j + n
>
> for n a constant natural number.

Sounds good to me.

> Constraints are solved for each declaration independently,
> underconstrained levels default to the minimum possible.  If one is  
> not
> happy with defaults, one can always decorate Set in one's Agda code  
> with
> the desired level.

This makes me a little nervous. I'd like to see more data
on how often defaulting happens. But it's worth the
experiment. One has to be careful about when one chooses
defaults and when one waits for more information, given that
the program arrives incrementally. Any unforced move is
potentially dangerous, resulting in programs which only
typecheck when delivered by a specific refinement sequence.
These bugs are extremely subtle. I learned to fear them the
hard way.

> Constraint solving is an application of Warshall's algorithm.  All  
> this
> is already in Agda for the case of sized types, which work according  
> to
> the same principles (explicit polymorphism, implicit subtyping).

This certainly suggests that there's an art of the possible.
If defaulting doesn't work out, asking for more information
should be ok.

> There is no need for a lifting on types then.

I'd still be happier if I knew that the role of the constraint
solver was to elaborate the insertion of explicit appeals to
cumulativity in a language with a more straightforward checker.
But then I would say that, wouldn't I? (Yous lot won't give
up on external termination checking until you're really stuck on
productivity, right?)

> Do you have some experience with this style of universe polymorphism?

I've been sniffing around it for a while, but I've never
quite decided on something to implement. So far, I'm very
positive about explicit polymorphism with one locally
quantified variable and a successor (why more variables?
why zero?) and I can see that cumulativity can and should
be silent much of the time. I've never spent long enough
on this problem to be comfortable in the corners.

Basically, go for it!

Cheers

Conor


>
> Cheers,
> Andreas
>
> Conor McBride wrote:
>> Hi Benja
>>
>> On 21 Sep 2009, at 11:23, Benja Fallenstein wrote:
>>
>>> Hi Conor,
>>>
>>> (new to this, please be kind if I say something particularly  
>>> stupid :-))
>>
>> I don't think the question arises!
>>
>>>
>>>> As it is, you may find traditional miseries
>>>> arising, when (^ Nat) -> (^ Nat) turns out to be different from
>>>> ^(Nat -> Nat). But perhaps you've got that covered..?
>>>
>>> I've noticed that IIUC, the two are isomorphic:
>>>
>>> ltr : ∀ {A} → ↑ (A → A) → ↑ A → ↑ A
>>> ltr f x = ⇑ (f (⇓ x))
>>>
>>> rtl : ∀ {A} → (↑ A → ↑ A) → ↑ (A → A)
>>> rtl f = ⇑ (λ x → ⇓ f (⇑ x))
>>>
>>> so what would be the traditional miseries? Definitional equality?
>>
>> Yes. It's annoying to need to pump values across an
>> iso explicitly, but the trouble doesn't stop there.
>> Once you have dependent function types and you start
>> working with the iso, you'll have terms like (ltr x)
>> appearing in types. These behave less well in
>> unification, as found in dependent pattern matching.
>> Also, you're bound to run into a term of type
>> (T (rtl (ltr x)) when you want one of type (T x).
>> Presumbly, we'll need ^ to commute with other type
>> constructors, and then we'll have questions like
>> whether (ltr x , ltr y)  =  ltr (x , y).
>>
>> I had a nasty time with these things when I was trying
>> to model observational equality for a hierarchy of
>> universes. By introducing multiple names for the same
>> type ("same" in the sense that the iso is constructor-
>> preserving, hence a no-op at run-time), I acquired a
>> huge coherence problem (gotta treat 'em all the same)
>> which I never solved. I think it's worth working for a
>> canonical representation, the better to support
>> generic programming.
>>
>>> Annoyance if the inference algorithm is too naive to insert all the
>>> arrows you want?
>>
>> That's certainly a problem. It's already a problem just
>> with cumulativity and unification. If I know that
>>
>>  Nat : Set
>>
>> and I'm trying to solve
>>
>>  Nat : ?X
>>
>> I am not free to presume that ?X = Set, because
>> ?X = Set1 is also a solution. As far as I'm aware, Agda
>> already hits this kind of trouble: I don't normally
>> file the bad examples, but perhaps I should.
>>
>> I do not know what rules Agda uses for unification: are
>> there any places where it is pragmatically necessary to
>> make less than most general guesses? Typical ambiguity
>> is one potential source of such weird corner cases;
>> implicit Pi is another.
>>
>> Once you add universe polymorphism, you have even more
>> degrees of freedom, and should thus expect less of
>> inference in the absence of explicit disambiguation.
>>
>>>
>>> [on Coq]
>>>> I believe it allows one to write
>>>>
>>>> cons (List Nat) nil : List Set
>>>
>>> It does; I happened to try that one yesterday after reading some old
>>> post of yours about universe polymorphism :-)
>>>
>>> Isn't typical ambiguity sufficient for that, though? It seems like  
>>> you
>>> only need to infer an index one level higher for the List Set
>>> constructors than for List Nat?
>>
>> Right, but you need both levels to be closed under
>> List type formation. Typical ambiguity would presume
>> a single i for which you can declare
>>
>>  List : Set i -> Set i
>>
>> but leave that i subject to a gradual accumulation of
>> constraints. There is no such i for which the above
>> typechecks. Coq somehow allows the two uses of List
>> above to be typed at different levels, so that's more
>> than typical ambiguity: it's some sort of polymorphism,
>> but I don't know what the rules are.
>>
>> It's good to experiment, but it's not yet time to
>> abandon the hope that one day we might actually
>> understand this stuff.
>>
>> Tread carefully
>>
>> Conor
>>
>> _______________________________________________
>> 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
> http://www.tcs.informatik.uni-muenchen.de/~abel/
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.9 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
>
> iEYEARECAAYFAkq7jrUACgkQPMHaDxpUpLPwtwCgmirR2t3y5kNw7Ecl7vDYB8a2
> dR4An1eYYqBnUczB3PeDne831V5U2eo1
> =DYfc
> -----END PGP SIGNATURE-----