[Agda] What is coinduction?

[Jean-Philippe Bernardy]

See also section 4 of:

http://www.jucs.org/jucs_10_7/total_functional_programming

Cheers,
JP.

On Tue, Oct 5, 2010 at 5:32 AM, Gregory Crosswhite
<gcross at phys.washington.edu> wrote:
>  Yay!  That is the first explanation that I've seen that made everything
> clear to me.  Thanks!  :-)
>
> Cheers,
> Greg
>
> On 10/4/10 7:30 PM, Peter Berry wrote:
>>
>> On 4 October 2010 23:57, Gregory Crosswhite<gcross at phys.washington.edu>
>>  wrote:
>>>
>>> Would someone be kind enough to give me a brief explanation about what
>>> the
>>> point of Coinduction/Codata is?  I've tried googling it, but most
>>> discussions seem to either assume that you already know what the purpose
>>> of
>>> it is or to give a very involved explanation from which it is hard to
>>> gleam
>>> the basic insight behind it.
>>
>> I was going to write a long explanation of data vs codata, but then I
>> remembered that Dan Piponi got there first (though his article is
>> aimed at Haskell programmers):
>> http://blog.sigfpe.com/2007/07/data-and-codata.html
>>
>> I'm sure there's room for something similar written for dependently
>> typed programmers / users of theorem provers / aspiring logicians in
>> general.
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>