[Agda] Re: Induction-recursion, indexing and universes.

[Dan Doel]

On Friday 23 April 2010 8:20:00 pm Dan Doel wrote:
> So (assuming I've understood IIR), has there been any thought given to
> extending Agda's induction-recursion to indexed induction-recursion?

Apologies for replying to myself. I went back to take another crack at the 
Indexed Induction-Recursion paper, and decided to try the example in the paper 
that was most amenable to implementation in Agda, and it worked. So, 
apparently Agda does have indexed induction-recursion, and it doesn't, in 
fact, mean what I thought it means. My idea is, in fact, an invalid 
definition, having a negative occurrence of U.

So, to change my question a bit: is my idea totally flawed? I suppose it 
essentially boils down to accepting definitions by recognizing that there is 
always some structural decrease:

  For T
    1) Base cases
    2) Cases that are legitimate induction-recursion
    3) Structural decrease in n

  For U
    k)   Usual conditions for inductive-recursive datatypes
    k+1) Indices of recursive parameters are always smaller than
         the output index of a constructor.

k+1 is obviously not usually required. For instance, in well-scoped lambda 
terms there's a constructor:

  lam : (n : Nat) (Term (suc n)) -> Term n

And it is k+1 along with 3 that makes the definition seem reasonable.

Anyhow, I'm a bit less enthusiastic about my idea now. Perhaps it's too ad-hoc 
to allow arbitrary negative-looking references if we have some other 
structural indicator (the papers on induction recursion note how difficult it 
is to find good models for it). If any type theory gurus think its a good 
enough idea to run with, though, I won't stop you from making it a reality.

Also, apologies for suggesting the Agda implementors had skimped on the 
induction-recursion front. :) I suppose I should look harder to see if I 
missed some devious way of actually making things work out.

-- Dan