Improved documentation for Bool (Was: [Haskell-cafe] Comments from OCaml Hacker Brian Hurt)

[Eugene Kirpichov]

2009/1/18 Daniel Fischer <daniel.is.fischer at web.de>:
> Am Sonntag, 18. Januar 2009 17:48 schrieb roconnor at theorem.ca:
>> On Sun, 18 Jan 2009, Ross Paterson wrote:
>> > Anyone can check out the darcs repos for the libraries, and post
>> > suggested improvements to the documentation to libraries at haskell.org
>> > (though you have to subscribe).  It doesn't even have to be a patch.
>> >
>> > Sure, it could be smoother, but there's hardly a flood of contributions.
>>
>> I noticed the Bool datatype isn't well documented.  Since Bool is not a
>> common English word, I figured it could use some haddock to help clarify
>> it for newcomers.
>
> Thanks. Really helpful. A few minor typos, though.
>
>>
>> -- |The Bool datatype is named after George Boole (1815-1864).
>> -- The Bool type is the coproduct of the terminal object with itself.
>> -- As a coproduct, it comes with two maps i : 1 -> 1+1 and j : 1 -> 1+1
>> -- such that for any Y and maps u: 1 -> Y and v: 1 -> Y, there is a unique
>> -- map (u+v): 1+1 -> Y such that (u+v) . i = u, and (u+v) . j = v
>> -- as shown in the diagram below.
>> --
>> --  1 -- u --> Y
>> --  ^         ^^
>> --  |        / |
>> --  i  u + v   v
>> --  | /        |
>> -- 1+1 - j --> 1
>
> You have the arrows i and j pointing in the wrong direction.
>
>> --
>> -- In Haskell we call we define 'False' to be i(*) and 'True' to be j(*)
>
> Delete "we call".
>
>> -- where *:1.
>> -- Furthermore, if Y is any type, and we are given a:Y and b:Y, then we
>> -- can define u(*) = a and v(*) = b.
>> -- From the above there is a unique map (u + v) : 1+1 -> Y,
>> -- or in other words, (u+v) : Bool -> Y.
>> -- Haskell has a built in syntax for this map:
>> -- @if z then a else b@ equals (u+v)(z).
Also, "equals (a+b)(z)" should be here.

>> --
>> -- From the commuting triangle in the diagram we see that
>> -- (u+v)(i(*)) = u(*).
>> --  Translated into Haskell notation, this law reads
>> -- @if True then a else b = a at .
>> -- Similarly from the other commuting triangle we see that
>> -- (u+v)(j(*)) = v(*), which means
>> -- @if False then a else b = b@
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>