[Haskell-beginners] The Holy Trinity of Functional Programming

Edward Z. Yang ezyang at MIT.EDU
Wed Aug 22 17:57:11 CEST 2012


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. <costello at mitre.org>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.
> 



More information about the Beginners mailing list