[Agda] Self-containing inductive-recursive definitions

[Thorsten Altenkirch]

I don't know wether it is described in the paper you mention but there  
is a systematic translation of such definitions which was also  
suggested by Conor. The basic idea is to define each datatype in an  
unindexed way and then introduce a family (i.e. a predicate)  
corresponding to the indexed version. In the example given  (after  
uncurrying the Sigma type) this corresponds to

mutual

    data U₀ : Set where
      u : U₀
      x : (s : U₀) -> T₀ -> U₀

    data T₀ : Set where
      u : U₀ → T₀
      x : ∀ {y} → (z : T₀) → z ≡ y → T₀

mutual
    data U₁ : U₀ → Set where
      u : U₁ u
      x : ∀ {s} {y} → (U₁ s) → T₁ s y -> U₀ → U₁ (x s y)

    data T₁ : (u : U₀)(t : T₀) → Set where
      u : ∀ {x} → U₁ x → T₁ x (u x)
      x : ∀ {s y z} → U₁ s → T₁ s y → T₁ s z → (p : z  
≡ y)
       → T₁ (x s y) (x z p)

data U : Set where
    _,_ : (u : U₀) → (U₁ u) → U

data T : U → Set where
    _,_ : ∀ {u₀} {u₁} → (t : T₀) → T₁ u₀ t → T  
(u₀ , u₁)


Cheers,
Thorsten



On 20 Jun 2010, at 22:32, Dan Doel wrote:

> 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