[Agda] Agda goes coinductive

Anton Setzer A.G.Setzer at swansea.ac.uk
Tue Jun 24 02:40:00 CEST 2008


I discussed today with my PhD student Chi Ming Chuang the implementation
by  Dan Doel  of the
delay monad (or partiality monad), and here are some comments:
(his implementation can be found at the end of this email.

We looked at the following part:
> never : {a : Set} -> D a
> never ~ later never
> 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
If we rewrite this code using coalgebras we get the following:


> mutual
>    coalg D  (A : Set) : Set where
>       _* : D A -> Dshape A
>
>   data D (A : Set) : Set where
>       now' : A -> Dshape A
>       later' : D A -> Dshape A
>
> now : {A : Set} -> A -> D A
> (now a) * = now' a
>
> later : {A : Set} -> D A -> D A
> (later d) * = later' d
>
>
> mutual
>     coalg _↑ {A : Set} : D A -> Set where
>         _* : d ↑ -> d ↑shape
>
>     data _↑shape {A : Set} : D A -> Set where
>         diverge : {d : D A} -> d ↑ -> (later d) ↑shape

Now we see that
diverge constructs an element of (later d) ↑shape
rather than an element of      d' ↑shape
for any d' such that d' * = later' d

That's why it is not possible to prove that
never ↑
holds, because we don't have that
never = later never


I suspect it is not possible to proof for any element d
that    d ↑   holds.

What should work is the following:

> data emptyset : Set where
>
> mutual
>     coalg _↑ {A : Set} : D A -> Set where
>         _* : d ↑ -> d ↑shape
>
>     _↑shape {A : Set} : D A -> Set
>     d ↑shape   with d *
>     ... | now _   = emptyset
>     ... | later d  = d ↑
This code should guarantee that all we need
for defining an element of
d ↑
is that d * = later d' for some d'
and we have a proof of
d' ↑
In case of  

never : {A : Set} -> D A
never * = later never

the following should then work

never_diverges : never ↑
never_diverges * = never_diverges

which should work since
never_diverges on the right hand side is an element
of
never ↑shape
which is equal to
never ↑



We can fake my coalg construct by codata by
replacing the _* by the reverse operation which I call pack.
We get

> mutual
>     codata _↑ {A : Set} : D A -> Set where
>          pack  :  {d : D A} -> d ↑shape -> d ↑
>
>     _↑shape : {A : Set} -> D A -> Set
>     (now _) ↑shape  = emptyset
>     (later d)  ↑shape= d ↑


Then in my opinion the following should work:

> never_diverges : never ↑
> never_diverges ~ pack  never_diverges


In fact when having the code

> never_diverges : never ↑
> never_diverges ~ pack  {! !}

we can solve the goal with never_diverges,
since the goal requires an element of

never ↑shape
which if we compute it is equal to
never ↑

But if we then load the code Agda gives an errow message

> later never != never of type D _35
> when checking that the expression pack never_diverges has type
> never ↑
which seems to be wrong.


I get the impression that the codata syntax leads to lots of confusion,
and I am starting to wonder whether it is such a good idea to
use the syntax of having codata combined with the ~ abbreviation:
Even so it makes sense (provided in pattern matching
one uses (~ (now a)) or (~ (later d))
instead of (now a) or (later d)
)
I get the impression that it will still be confusing and makes Agda a bit
unpredicable.

A syntax like

mutual
   coalg D  (A : Set) : Set where
      _* : D A -> Dshape A

  data D (A : Set) : Set where
      now' : A -> Dshape A
      later' : D A -> Dshape A

is much more verbose, but makes Agda more predicable.

Anton








Dan Doel wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>   


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
 
                    
  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080624/fa341074/attachment.html


More information about the Agda mailing list