[Agda] AIM 10 notes

[Conor McBride]

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