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

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Conor,

you were dearly missed on AIM 10.

My opinion is to implement implicit cumulativity and explicit parametricity.

> 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.

We would have

  Nat : forall {i} -> Set i

In this case one should get

   Nat : Set ?i

with ?i an unconstrained level meta variable.  (Or just the trivial
constraint ?i >= 0.)

We have explicit polymorphism as in

  List : forall {i} -> Set i -> Set i

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.

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.

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).

There is no need for a lifting on types then.

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

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-----