[Agda] What is coinduction?

[Peter Berry]

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.

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html