[Agda] Self-containing inductive-recursive definitions

[Thorsten Altenkirch]

Hi Dan,

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.

Cheers,
Thorsten

On 11 Jun 2010, at 16:02, Dan Doel wrote:

> Greetings,
>
> I was reading the recent Forsberg and Setzer paper* on inductive- 
> inductive
> definitions, and they made a note that you could write definitions  
> of that
> form in Agda which contain codes for the type being defined.  
> However, this is
> currently no different than Agda's implementation of induction- 
> recursion:
>
> 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)
>
> Conor McBride confirmed for me that this definition would not be  
> expressible
> in the more formal treatments of induction-recursion (by Dybjer and  
> Setzer*,
> say). The positivity checker rules out some obviously bad variations  
> of the
> above, like if we try to add pi types to the universe:
>
> pi : (s : U) -> (T s -> U) -> U
>
> we could obtain:
>
> pi u : (U -> U) -> U
>
> which is correctly rejected. However, informally, even the first  
> definition
> above is bad, because the mutual definition plays on T being able to  
> be
> defined for 'the elements of U constructed thus far', while U as a  
> whole is
> not defined within the definition. More formally (Conor again  
> informs me), the
> problem is that the functor for the above definition refers to its  
> own initial
> algebra.
>
> I don't have an example where this sort of thing leads to a proof of  
> false; at
> a guess, you probably can't do anything really terrible unless the  
> positivity
> checker is off. But, is this cause for concern anyhow? Should it be
> disallowed? I'm not sure if this warrants filing an issue in the bug  
> tracker,
> so I thought I'd ask for opinions here first.
>
> Cheers,
> -- Dan
>
> [1] http://cs.swan.ac.uk/~csfnf/papers/indind_csl2010.pdf
> [2] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.2863
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda