
Yes, but we can also use a similar style of inductive reasoning in the face of infinite types, called Scott induction [1]. There is also a perspective that infinite types (or so called 'codata') should be reasoned with 'coinduction', although the proof principles there are a little more esoteric. Cheers, Edward [1] http://blog.ezyang.com/2010/12/no-one-expects-the-scott-induction/ Excerpts from Brandon Allbery's message of Wed Aug 22 11:04:48 -0400 2012:
On Wed, Aug 22, 2012 at 7:38 AM, Costello, Roger L.
wrote: But do you think you could provide a more "real world" example of an application of the "Holy Trinity" ideas?
A commonly cited real-world example that illustrates the first key idea (recursive data type) is a binary tree:
I'd have used lists, since in Haskell we make use of infinite lists quite a bit; a simple example being zipping some list against [0..] (a list comprising an infinitely ascending sequence of numbers) to pair each item with its index.