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

roconnor at theorem.ca roconnor at theorem.ca
Sun Jan 18 11:48:40 EST 2009


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(*).
--  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@

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''


More information about the Haskell-Cafe mailing list