Mercurial > cpdt > repo
diff src/Coinductive.v @ 395:3c941750c347
Citations for lazy data structures, Haskell 'deriving', and logic programming
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 22 Apr 2012 16:25:22 -0400 |
| parents | 4b1242b277b2 |
| children | 05efde66559d |
line wrap: on
line diff
--- a/src/Coinductive.v Sun Apr 22 15:51:03 2012 -0400 +++ b/src/Coinductive.v Sun Apr 22 16:25:22 2012 -0400 @@ -18,7 +18,7 @@ (** %\chapter{Infinite Data and Proofs}% *) -(** In lazy functional programming languages like %\index{Haskell}%Haskell, infinite data structures are everywhere. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow. +(** In lazy functional programming languages like %\index{Haskell}%Haskell, infinite data structures are everywhere%~\cite{whyfp}%. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow. %\index{laziness}%Laziness is easy to implement in Haskell, where all the definitions in a program may be thought of as mutually recursive. In such an unconstrained setting, it is easy to implement an infinite loop when you really meant to build an infinite list, where any finite prefix of the list should be forceable in finite time. Haskell programmers learn how to avoid such slip-ups. In Coq, such a laissez-faire policy is not good enough.