[Agda] AIM 10 notes

[Conor McBride]

Hi Ulf, hi Dan,

On 21 Sep 2009, at 08:58, Ulf Norell wrote:

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

>  "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
>
> What you're describing is level inference rather than actual  
> polymorphism.

sometimes referred to as "typical ambiguity"

> I do believe there is an implementation of universe polymorphism as  
> well, but I'm not sure how it works.

 From what Hugo said at that CHIT/CHAT meeting (which we should
have another one of sometime), there's some sort of generativity
in the instantiation of universe variables for type constructors
at usage sites, but perhaps we should just RTFM and then ask
nicely. I believe it allows one to write

   cons (List Nat) nil : List Set

but it might be worth having a crack at other trickier cases, e.g.

   (i) n-ary vZipWith (taking a vector of n source sets and a
       target set, lifting the function thus specified to m-ary
       vectors); you tend to want vectors at both levels and
       also operations like map;
  (ii) a universe-polymorphic universe, giving codes for level i
       sets, and Set i itself perhaps, in Set i+1.

In any case, great that you're on this case. Overdue. It's clear
that *something* has to be explicit, as the combination of
polymorphism and typical ambiguity gives rise to systems which
tend to be somewhat underconstrained.

Meanwhile, on the postulates/implicit-rules question, might there
be a third possibility? Should \uparrow compute through the
structure of types? 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..?

Again, many apologies for not making it to Goteborg last week,
despite having given Michael O'Leary the money. It was something
I realised I had to not do, given the timing.

All the best

Conor