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

Cory Knapp thestonetable at gmail.com
Sun Jan 18 12:03:06 EST 2009

```roconnor at theorem.ca wrote:
> 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.
>
> -- |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
> --
> -- In Haskell we call we define 'False' to be i(*) and 'True' to be
> j(*) -- 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).
> --
> -- From the commuting triangle in the diagram we see that
> -- (u+v)(i(*)) = u(*).