The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

Hi,

I have been trying to working coinductive data and definitions
recently and have found that Coq been very helpful in developing
intuition about this sort of thing.  So I found your remarks below
very interesting.  Specifically, you seem to imply that a
CoInductive/codata definition in Coq/Agda permits some operations that
an abstract type with an "observe" function would not permit.  Can you
(or anyone else) be more specific about what these would be?

 - Aaron

On Thu, Nov 20, 2008 at 6:21 PM, Dan Doel 
<dan.doel AT gmail.com>
 wrote:
> The scheme that did yield a proof is based on mails from Anton Setzer, who I
> suspect would say that codata as found in Agda and Coq gives you poor
> intuition about how to work with coinductive data. Instead you want to think
> in terms of coalgebras. So, rather than:
>
>  codata D (a : Set) : Set where
>    now : a -> D a
>    later : D a -> D a
>
> Which looks like you have constructors, what you want is something more 
> like:
>
>  -- For any a:Set, D a is the terminal coalgebra where the observation is
>  -- of type B -> a + B
>  D : Set -> Set
>
>  observe : {a : Set} -> D a -> a + D a
>
> Importantly, a value of type D a is not either (now a) or (later a). The 
> only
> operation on it is "observe" (which was the star operation in my code), 
> which
> yields either a regular value, or another D a.