[Agda] Self-containing inductive-recursive definitions

[Dan Doel]

On Sunday 20 June 2010 9:00:18 am Thorsten Altenkirch wrote:
> I haven't read the Setzer/Forsberg paper yet but it seems clear that
> your code is equivalent to an inductive/inductive definition, namely
> 
>   data U : Set where
>     u : U
>     x : (s : U) -> T s -> U
> 
>   data T : U → Set where
>     u : U → T u
>     x : ∀ {s y} → Σ (T s) (λ z → z ≡ y) → T (x s y)
> 
> and we know how these can be translated into conventional inductive
> definitions (w.o. dependency). I guess that's what the paper is about.

This is actually what I thought when I first saw reference to the paper in 
another by Conor McBride (Outrageous but Meaningful Coincidences). But such 
definitions are apparently *not* implied by conventional inductive 
definitions. Mutual inductive definitions are, like:

    data U : Set where
      c1 : ... T ... -> U
      ...

    data T : Set where
      k1 : ... U ... -> T
      ...

in fact, when I asked, Conor noted that they're easily represented by 
inductive families:

    data F : Fin 2 -> Set where
      c1 : ... F 1 ... -> F 0 -- taking liberties with numeric syntax
      ...
      k1 : ... F 0 ... -> F 1
      ...

    U = F 0
    T = F 1

(and this extends to mutually inductive families, as long as they aren't 
indexed by each other) but this is not what's happening here. Here, we have 
the mutual definition of a datatype U, and a family T indexed by U, which 
presumably isn't covered by, e.g. Peter Dybjer's work on induction and 
inductive families and whatnot (otherwise, people wouldn't be writing new 
papers about it :)). For instance, if you try to apply the above trick, then 
you get an inductive family indexed by itself:

    I : Set -> Fin 2 -> Set
    I A 0 = Unit
    I A 1 = A

    data F : (f : Fin 2) -> I (F 0 _) f -> Set where
      ...

which would certainly be new territory.

Anyhow, in the induction-induction paper, they specifically mention that their 
formalization tries to rule out definitions where a universe has a code for 
itself, just like the previous inductive-recursive definitions. They mention 
that Agda allows such definitions, but that that doesn't mean that it's 
actually a sensible decision (and if you're judging by conformance to 
established theory for the definitions, it's wrong).

I'm actually not certain if your above definition is the sort they had in mind 
(as I recall, they don't give a specific example of what they mean), but I do 
know that the inductive-recursive definition is one that isn't justified by 
the literature on the subject.

Of course, if someone can find a formalization (and an associated category for 
initial algebras, and some promising denotational semantics) for such 
definitions, that's probably a paper or two for the taking. :)

-- Dan