[Agda] Agda goes coinductive

[Dan Doel]

On Thursday 05 June 2008, Ulf Norell wrote:
> One of the code sprints in the recent Agda meeting was to add coinductive
> datatypes to Agda.

Excellent! In celebration, here's everyone's favorite monad: partiality (a mix 
of stuff from Abstract Nonsense for Functional Programmers and General 
Recursion via Coinductive Types).

---- snip ----

data Maybe (a : Set) : Set where
  nothing : Maybe a
  just    : a -> Maybe a

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

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

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

-- return the result of the computation that finishes first
race : {a : Set} -> D a -> D a -> D a
race (now a)    _           ~ now a
race (later da) (now a)     ~ now a
race (later da) (later da') ~ later (race da da')

return : {a : Set} -> a -> D a
return = now

infixl 40 _>>=_
_>>=_ : {a b : Set} -> D a -> (a -> D b) -> D b
(now a)    >>= f ~ f a
(later da) >>= f ~ later (da >>= f)

-- getting something out of the partiality monad
compute : {a : Set} -> Nat -> D a -> Maybe a
compute zero    (now a)    = just a
compute zero    (later da) = nothing
compute (suc n) (now a)    = just a
compute (suc n) (later da) = compute n da

data _↓_ {a : Set} : D a -> a -> Set where
  convergeNow   : {x : a} -> (now x) ↓ x
  convergeLater : {x : a} {dx : D a} -> dx ↓ x -> later dx ↓ x

codata _↑ {a : Set} : D a -> Set where
  diverge : {dx : D a} -> dx ↑ -> later dx ↑

-- problems here
-- diverge-never : never ↑
-- diverge-never ~ diverge diverge-never
-- complaint: never != later never

fix-aux : {a b : Set} -> (a -> D b) -> ((a -> D b) -> a -> D b) -> a -> D b
fix-aux k f a with f k a
...           | now b   ~ now b
...           | later d ~ later (fix-aux (f k) f a)

fix : {a b : Set} -> ((a -> D b) -> a -> D b) -> a -> D b
fix ~ fix-aux (\_ -> never)

---------------------------------------------------------------
-- example: quicksort

data Bool : Set where
  false : Bool
  true  : Bool

not : Bool -> Bool
not true  = false
not false = true

_<=_ : Nat -> Nat -> Bool
zero  <= _     = true
suc x <= zero  = false
suc x <= suc y = x <= y

_>_ : Nat -> Nat -> Bool
x > y = not (x <= y)

infixr 70 _::_
data [_] (a : Set) : Set where
  []   : [ a ]
  _::_ : a -> [ a ] -> [ a ]

filter : {a : Set} -> (a -> Bool) -> [ a ] -> [ a ]
filter _ [] = []
filter p (x :: xs) with p x
...                | false = filter p xs
...                | true  = x :: filter p xs

infixr 60 _++_
_++_ : {a : Set} -> [ a ] -> [ a ] -> [ a ]
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

qsort-aux : ([ Nat ] -> D [ Nat ]) -> [ Nat ] -> D [ Nat ]
qsort-aux qsort [] = return []
qsort-aux qsort (x :: xs) = qsort l >>= \l' ->
                            qsort u >>= \u' ->
                            return (l' ++ x :: u')
 where
 l = filter (\y -> y <= x) xs
 u = filter (\y -> y > x) xs

qsort : [ Nat ] -> D [ Nat ]
qsort = fix qsort-aux

---- snip ----

As noted, the proof of the divergence of never (from General Recursion via 
Coinductive Types) doesn't seem to be liked. Also, I haven't yet figured out 
how to get the result of quicksort evaluated (no matter how large a number I 
pass to compute). I'm not exactly sure what I'm doing wrong.

This simpler example works, though:

---- snip ----

_+_ : Nat -> Nat -> Nat
zero    + n = n
(suc m) + n = suc (m + n)
{-# BUILTIN NATPLUS _+_ #-}

_*_ : Nat -> Nat -> Nat
zero * n    = zero
(suc m) * n = n + (m * n)
{-# BUILTIN NATTIMES _*_ #-}

fac-aux : (Nat -> D Nat) -> Nat -> D Nat
fac-aux _ 0 = return 1
fac-aux fac (suc n) = fac n >>= \fn -> return ((suc n) * fn)

fac : Nat -> D Nat
fac = fix fac-aux

fac' : Nat -> Maybe Nat
fac' n = compute (suc n) (fac n)

---- snip ----

Of course, factorial doesn't need general recursion.

-- Dan Doel