[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