[Agda] AIM 10 notes

[Ulf Norell]

On Sun, Sep 20, 2009 at 8:50 PM, Dan Doel <dan.doel at gmail.com> wrote:

>
> I must admit, I had similar hopes. I don't know much Coq, but it seems to
> have
> quite serviceable universe polymorphism, based around rules like:
>
>  "Type" can be used in lieu of "Type[i]" when 'i's can be inferred
>  If A : Type[i], and i < j, then A : Type[j] as well
>
> Which seems to allow for not actually mentioning the indices much, even
> when
> multiple universe levels may be in play (as the solver is generally
> sufficient). Of course, that requires the indices and solver thereof to be
> more built-in, but I'm not sure that's unreasonable.
>

What you're describing is level inference rather than actual polymorphism. I
do believe there is an implementation of universe polymorphism as well, but
I'm not sure how it works.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090921/109a86c0/attachment.html