[Agda] AIM 10 notes

[Benja Fallenstein]

Hi Conor,

>> (new to this, please be kind if I say something particularly stupid :-))
>
> I don't think the question arises!

Glad to hear :-) Thanks for the answers!

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

Ah, seems that I misunderstood what typical ambiguity means in this
context. I know the phrase from simple type theories, referring IIUC
to an informal practice that can be formalized using Hindley-Milner
(as done in HOL), so I thought it referred to something similar here.

I do have the problem in Coq that while I have some intuitive
understanding of the semantics as "sort of Hindley-Milner-like", I
don't understand what's going on exactly and I sometimes get universe
inconsistency errors I wasn't expecting and don't understand. This
means that I'm not always sure how much I've accomplished -- for
example, I've written a type of Coq terms parametrized by the term's
value, i.e.

Inductive Term' (n:nat) (A:Type) (t:Telescope n A)
              : forall T:A->Type,
                  (forall a:A, T a) -> Type := ...

(n = length of context, A = type of assignments to context variables,
t = reification of context, T = type of value of term, given variable
assignment; anonymous parameter = value of term, given variable
assignment)

My intention is for this to support "typing dynamic typing" a la
Haskell's Dynamic:

Definition Term (X:Type) (x:X) :=
  Term' O Unit nil (const X) (const x).

Inductive Dyn : Type :=
  dyn (T:Type) (t:Term Type T) (x:T) : Dyn.

but one of the clauses of Term' reads simply

  | typeT : Term' n A t (const Type) (const Type)

and I just don't understand Coq's polymorphism enough to be sure
whether I can use this at different universe levels inside the same
Term as I seem to need to (haven't had time for trial-and-error with
it, yet)...

It'd be really nice to have a simple core that the declarations
elaborate into, to better understand what's going on (as in the Ulf's
version)!

>> 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.
...
> Also, you're bound to run into a term of type
> (T (rtl (ltr x)) when you want one of type (T x).

Right. I remember well a bunch of problems I had last month or so with
types littered with 'coerce's I didn't want, which ultimately instead
of solving I circumvented by turning from a fan into a user of
heterogeneous equality, so I have good reason to listen to your wisdom
there, I suppose =-) (though still, I begrudge the loss in simplicity
in the core system, compared to a literal reading of Ulf's notes as
the core to be elaborated into.)

Thanks,
- Benja