[Agda] What is coinduction?

[Gregory Crosswhite]

  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.
>