[Agda] Getting codata right

[Dan Doel]

On Saturday 07 June 2008, Anton Setzer wrote:
> I think I have now a suitable understanding
> of in what sense codata can be regarded as an abbreviation
> for coalgebraic definitions, which includes now as well
> a good notation for pattern matching on codata.
> Here follows my proposal, which correspond pretty much
> to the implementation in Agda at present, with a slight modification
> on pattern matching.
>
> I think codata should be a notational convenient way
> of dealing with coalgebra, but everything should be reducible
> to coalgebras.
> Although it would be desirable to have coalgebras directly,
> since they probably will soon get their own independent
> life, I think one can live with the fact to have only coalgebras
> and that codata definitions should only in principal reduce to
> codata.

This mail was extremely helpful. Thanks! Especially this part:

> With respect to indexed codata I think only the
> restricted version (or coinductive families) make to me full sense yet.
>
> Something like
> codata _bisim_ : coNat -> coNat -> Set where
>     pZ : (~ Z) bisim (~ Z)
>     pS : (n m : coNat) -> n bisim m ->  ~ (S n)  bisim ~ (S m)
>
> doesn't make much sense
> but something like
>
> mutual
>    _bisim_ : coNat -> coNat -> Set where
>    (~ Z) bisim (~ Z) = bisimZ
>    (~ (S n)) bisim (~ (S m)) = n bisimS m
>    (~ _) bisim (~ _) = bisimFalse
>
>    codata bisimZ : Set where
>        pZ : bisimZ
>
>    codata _bisimS_ : coNat -> coNat -> Set where
>         pS : n  bisim m -> n bisimS m
>
>    codata bisimFalse where
>
> makes sense.

I was able to cargo cult my way through translating proofs from General 
Recursion via Coinductive Types to this definition scheme:

---- code ----

module Partial2 where

  data Σ (a : Set) (P : a -> Set) : Set where
    _,_ : (w : a) (pf : P w) -> Σ a P

  data ⊥ : Set where

  codata co-⊥ : Set where

  void : {a : Set} -> ⊥ -> a
  void ()

  infixr 60 ¬_
  ¬_ : Set -> Set
  ¬ P = P -> ⊥

  data _==_ {a : Set} (x : a) : a -> Set where
    ==-refl : x == x

  infixr 50 _+_
  data _+_ (a b : Set) : Set where
    inl : a -> a + b
    inr : b -> a + b

  codata D (a : Set) : Set where
    now   : (v  : a)   -> D a
    later : (dv : D a) -> D a

  never : {a : Set} -> D a
  never ~ later never

  mutual
    _↑ : {a : Set} -> D a -> Set
    later dv ↑ = DivergeLater dv
    now v    ↑ = co-⊥
    
    codata DivergeLater {a : Set} : D a -> Set where
      diverge : (dv : D a) -> (pfd : dv ↑) -> DivergeLater dv

  mutual
    infix 60 _↓_
    _↓_ : {a : Set} -> (dv : D a) -> (v : a) -> Set
    now v    ↓ v' = ConvergeNow (now v) v' 
    later dv ↓ v  = ConvergeLater dv v 

    data ConvergeNow {a : Set} : D a -> a -> Set where
      converge-now : {v : a} -> ConvergeNow (now v) v

    data ConvergeLater {a : Set} (dv : D a) (v : a) : Set where
      converge-later : dv ↓ v -> ConvergeLater dv v

  diverge-never : forall {a} -> never {a} ↑
  diverge-never ~ diverge never diverge-never

  ¬↓→↑ : {a : Set} (x : D a) -> ¬ Σ a (\v -> x ↓ v) -> x ↑
  ¬↓→↑ {a} (now v)    ¬sig ~ void (¬sig (v , converge-now))
  ¬↓→↑ {a} (later dv) ¬sig ~ diverge dv (¬↓→↑ dv ¬sig')
   where
   ¬sig' : ¬ Σ a (\v -> dv ↓ v)
   ¬sig' (v , pf) ~ ¬sig (v , converge-later pf)

  race : {a : Set} (x y : D a) -> D a
  race (now v)    y           ~ now v
  race (later dv) (now v)     ~ now v
  race (later dv) (later dv') ~ later (race dv dv')

  race-converge : {a : Set} (x y : D a) (v : a)
                  -> race x y ↓ v -> x ↓ v + y ↓ v
  race-converge (now .v)   y        v converge-now = inl converge-now 
  race-converge (later dv) (now .v) v converge-now = inr converge-now 
  race-converge (later dv) (later dv') v (converge-later pf)
                                         with race-converge dv dv' v pf
  ...                                    | inl pfx = inl (converge-later pfx) 
  ...                                    | inr pfy = inr (converge-later pfy)

---- /code ----

(Only a portion of the proofs in that paper, of course.) Aside from the 
somewhat wonky definitions for codata-indexed types, this is pretty much 
exactly the code I wanted to write for this stuff.

Excellent work! :)

-- Dan