[Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)

[Aaron Bohannon]

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.