[Agda] Self-containing inductive-recursive definitions

[Nils Anders Danielsson]

On 2010-06-11 16:02, Dan Doel wrote:
>    mutual
>      data U : Set where
>        u : U
>        x : (s : U) ->  T s ->  U
>
>      T : U ->  Set
>      T u       = U
>      T (x s y) = Σ (T s) (\z ->  z == y)

This example can also be encoded using the (highly experimental) flag
--guardedness-preserving-type-constructors:

   data UC : Set where
     u x : UC

   mutual

     U : Set
     U = Σ UC U′

     U′ : UC → Set
     U′ u = ⊤
     U′ x = Rec (♯ Σ U T)

     T : U → Set
     T (u , _)            = U
     T (x , fold (s , y)) = Σ (T s) λ z → z ≡ y

The recursive calls in the second clause of U′ are both guarded, and T
"preserves guardedness" and is locally structurally recursive.

If you add Π the code is no longer accepted, because calls in negative
position are never guarded:

   data UC : Set where
     u x π : UC

   mutual

     U : Set
     U = Σ UC U′

     U′ : UC → Set
     U′ u = ⊤
     U′ x = Rec (♯ Σ U T)
     U′ π = Rec (♯ Σ U λ s → T s → U)
                          -- ^^^ Negative.

     T : U → Set
     T (u , _)            = U
     T (x , fold (s , y)) = Σ (T s) λ z → z ≡ y
     T (π , fold (s , f)) = (x : T s) → T (f x)
                         -- ^^^^^^^^^ Negative.

--
/NAD