[Agda] Coinductive families

[Thorsten Altenkirch]

On 4 Oct 2010, at 23:45, Dan Doel wrote:

> On Monday 04 October 2010 1:49:11 pm Thorsten Altenkirch wrote:
>> I think it is a good idea if we distinguish two issues:
>> 
>> 1) The definitions of datatypes by constructors or destructors
>>     corresponding to labelled sums (data) and labelled products (codata)
>> 2) The definition of recursive datatypes as either inductive or coinductive
>>     corresponding to initial algebras or terminal coalgebras.
>> 
>> E.g. sometimes it is more natural to represent coinductive datatypes in
>> their constructor representations, eg. for colists. Also decoupling the
>> two allows a flexible syntax for mixed inductive / coinductive datatypes
>> (see Nisse's and main recent papers on this).
> 
> How well does this work, though? It seems like there are problems with it.

I tried to guess what "it" is. :-)

Reading on, it seems that you are saying that the termination checker should be
aware of destructors in the sense that a destructor should make things structurally 
smaller but that this would lead to non-termination (for open terms).

Is this a sensible summary? I don't have a good answer, actually I haven't thought of this.

Thorsten

> The 
> correspondence of inductive types with data as labelled sums is, of course, 
> due to some mangling of the algebra action:
> 
>  in : F A -> A
>    ~ F A = F1 A + F2 A + ...
>  (c1 : F1 A -> A) * (c2 : F2 A -> A) * ...
> 
> If we instead want to define an inductive type by its destructors, it's a 
> roundabout process.
> 
>  F A = F1 A * F2 A * ...
>  in : F A -> A
>  cata : (F B -> B) -> A -> B
>  cata (map in) : A -> F A
>  d_i = proj_i . cata (map in) : A -> Fi A
> 
> and the projections are only really justified in light of the general 
> eliminator. Importantly, the projections don't directly give you a basis for 
> writing inductively justified functions. The bug report I mentioned had an 
> example of this:
> 
>  record R : Set where
>    destructor
>      p : R -> R
> 
>  foo : R -> R
>  foo r = foo (p r)
> 
> Inductively this is justified, but it won't normalize. Really, if we expect 
> records to be inductive, we probably have to perform the *reverse* 
> translation: projections into constructors (and lose eta?).
> 
>  foo r = foo (p r) ==> foo (record { r }) = foo r
> 
> This is the form that is (obviously) justified by the induction principle, and 
> doesn't have normalization problems.
> 
>> In any case, I think it is a good idea to dualize our current way to define
>> indexed datatypes by indexed constructors to indexed records defined by
>> destructors as Dan and Andreas suggest. To add another example, we can
>> define Vec using destructors:
>> 
>> record Vec (A : Set) : ℕ → Set where
>>  destructor
>>    hd : ∀ {n} → Vec A (suc n) → A
>>    tl : ∀ {n} → Vec A (suc n) → Vec A n
> 
> This can have some oddness, too:
> 
>  foldr : {A R : Set} {n : Nat} -> (A -> R -> R) -> R -> Vec A n -> R
>  foldr {n = 0}     f z l = z
>  foldr {n = suc m} f z l = f (hd l) (foldr f z (tl l))
> 
> if we want to use the projections, we are required to do induction on n, 
> otherwise we'll fail to normalize, l won't have the right type, we'll have no 
> base case.... What even is the constructor-based definition?
> 
>  foldr f z (record {hd = x ; tl = xs}) = f x (foldr f z xs)
>  foldr f z ???                         = z
> 
> The inductive family is sort of split into disjoint injections by an accident 
> of the index, but I don't know if this is good enough to base elimination 
> around. I think typically the underlying theory is like (neglecting the slice 
> stuff and using families):
> 
>  F : (Nat -> Set) -> Nat -> Set
>  F X 0 = Top
>  F X n = Bot
> 
>  G : (Nat -> Set) -> Nat -> Set
>  G X 0       = Bot
>  G X (suc n) = A * X n
> 
> And then Vec A = initial algebra of (F + G), meaning there's a clear way to 
> split even on an arbitrary family (and then you erase the bottom cases). The 
> inductive codata instead looks like:
> 
>  F : (Nat -> Set) -> Nat -> Set
>  F X 0       = Top
>  F X (suc n) = A * X n
> 
> So it is less obvious that the family itself is an initial algebra of a sum of 
> functors on the category of families. Recognizing it in general would probably 
> require decomposing arbitrary functors in the right way (we could, of course, 
> decompose it in many ways, but it may not correspond to the constructors we'd 
> want). This isn't necessarily an academic question, either, because the 
> checker presumably needs to rewrite the inductive-projections into inductive-
> matching before it can decide how/whether the termination of the function is 
> justified; so it'd need to be done for foldr above, even though it's 
> ultimately unnecessary.
> 
> Coinduction and constructors also have impedence mismatches, as Agda's history 
> with it has shown. Most notably, the sums/constructors being defined are for 
> the result of the observation, and so matching on them doesn't make sense in 
> the usual inductive, dependent pattern matching way.
> 
> If we wanted to really make this work, it'd probably be necessary to have 
> destructor and constructor clauses for both inductive and coinductive types:
> 
>  data Vec (A : Set) : Nat -> Set where
>    constructor
>      []   : Vec A 0
>      _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
>    destructor
>      head : {n : Nat} -> Vec A (suc n) -> A
>      tail : {n : Nat} -> Vec A (suc n) -> Vec A n
> 
> where, for inductives, destructor-based code is rewritten into constructor-
> based code, and constructors cannot be elided, and the opposite is true for 
> coinductives. I see that Andreas Abel has something like that from his message 
> that recently arrived. I note that the above sort of definition requires that 
> we verify that the shape defined by the constructors matches that defined by 
> the destructors, as well; I'm not sure how hard that is in general.
> 
> 
> I'm kind of skeptical about citing the mixed induction and coinduction, too, 
> because what Agda has (and has had for some time) is not exactly coinduction. 
> If it were, then ∞ would just be the identity functor, and writing:
> 
>  data T : Set where
>     t : ∞ T -> T
> 
> would not result in a coinductive type, and we'd be able to write:
> 
>  foo : T → ⊥
>  foo (t x) = foo (♭ x)
>  -- ♭ x <= x < t x
> 
> There's probably a theory underlying how Agda works (and the stuff Nisse* and 
> others have built on it is impressive), but coinduction isn't (obviously) it.
> 
>> Dually to the fact that we can encode indexed datatypes using equality and
>> sigma-types, we can can encode these indexed records using eqaulity and
>> pi-types, namely
>> 
>> record Vec (A : Set)(n : ℕ) : Set where
>>  field
>>    hd : ∀ {m} → n ≡ suc m → A
>>    tl : ∀ {m} → n ≡ suc m → Vec A m
> 
> Yeah. I was thinking about this, but for some reason I was thinking there'd 
> have to be a sigma in there. It can be curried away, clearly.
> 
> This, I guess, gives credence to the idea that the indices quantified over 
> aren't a problem.
> 
> -- Dan
> 
> [*] Have I been Doing It Wrong by spelling it Nils? They are the same person, 
> right? If so, I'm sorry.