[Agda] Coinductive families

[Dan Doel]

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. 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.