[Agda] Coinductive families

[Dan Doel]

On Monday 04 October 2010 4:04:19 am Andreas Abel wrote:

> It comes natural then to extend pattern matching to destructor
> patterns, so the constructor is creating an object defined by its
> observations.
> 
>    cons : .{A : Set} -> A -> Stream A -> Stream A
>    head (cons a as) = a
>    tail (cons a as) = as

Yes, I've seen that before, and it's what I expected. I hadn't fully thought 
through the corecursive definition angle, though, so I elided it.

I suppose another piece of the puzzle is that refinements happen in certain 
cases with indexed records/coinductive families:

  data Fin : Nat -> Set where
    zero : .{n : Nat} -> Fin (suc n)
    suc  : .{n : Nat} -> Fin n -> Fin (suc n)

  codata Cofin : Nat -> Set where
    pred  : .{n : Nat} -> Cofin (suc n) -> Maybe (Cofin n)
    empty : Cofin 0 -> Bot

  inject : .{n : Nat} -> Fin n -> Cofin n
  -- in the first two cases, n = suc m, refined by pred
  pred  (inject zero)    = nothing
  pred  (inject (suc i)) = just (inject i)
  -- in this case, n = 0, refined by empty
  empty (inject ())

or, in more generality:

  ana : .{F : Nat -> Set} -> (F 0 -> Bot)
                          -> (.{n : Nat} -> F (suc n) -> Maybe (F n))
      -> .{n : Nat} -> F n -> Cofin n
  -- pred (ana e p f) = mapMaybe (ana e p) (p f)?
  -- Would that pass a syntactic productivity check? I'm not entirely sure
  -- what the criteria would be.
  pred  (ana e p f) with p f
  ... | nothing = nothing
  ... | just f' = just (ana e p f')
  empty (ana e _ f) = e f

-- Dan