1
$\begingroup$

In the sources of Haskell's AwesomePrelude there is a 'bool' function with which all other operators can be defined (provided true and false are given):

x /\ y = bool false y x  x \/ y = bool y true x  not = bool true false 

Where I can read just a bit more about it, it's name if there is one? Wikipedia article will suffice.

  • 0
    How is bool defined? Try evaluation bool on all $2^3$ 3-tuple of True and False. With the truth table, you may be able to give a better description of bool.2011-09-21
  • 1
    Can you add the definition of `bool` for the benefit of those of us not familiar with the AwesomePrelude?2011-09-21
  • 3
    Although I'm guessing it's like the [ternary conditional operator](http://en.wikipedia.org/wiki/%3F:) (which is the same as the `if`-`then`-`else` in Haskell) with arguments in a funny order.2011-09-21
  • 0
    [Bool.hs](https://github.com/tomlokhorst/AwesomePrelude/blob/master/src/Generic/Data/Bool.hs) for all of you who want to read the definition he mentioned. By the definition of `if'` there you can see that it is, as @Rahul guessed - the conditional operator with arguments in funny order ...2011-09-21
  • 0
    Rahul Narain, bool there is a method of the BoolC typeclass with no default implementation. And it seems there no instances for which to look the implementation. Well, yes it seems to be connected to if then else, I'll better read a blog post about Awesome Prelude, maybe it is explained there.2011-09-21

2 Answers 2

2

This seems to be just an if expression with its arguments reversed and wrapped up in a typeclass, i.e. if p x y = bool y x p with x, y and p of suitable type.

1

All usual theories in mathematics (the theory of groups, the theory of rings, the theory of modules, etc., etc.) has axioms. Because axioms of BoolC are not given, it actually has not semantics. But I can guess axioms. :)

IMHO it has nothing to do with logic. Methods of BoolC resemble the constructors and the destructor of Bool. Then read about Church encoding, especially about Church booleans. We have similar things for other datatypes, e.g. Nothing, Just are the constructors and maybe is the destructor of base.Data.Maybe.Maybe.

Let me describe it in the context of category theory. Bool in Haskell is $1+1$ in category theory. $+$ is a colimit, thus $1+1$ also is, but it can be defined by equations:

  • operations:
    • injections:
      • $\iota_0: 1\to 1+1$;
      • $\iota_1: 1\to 1+1$;
    • sum of morphisms: $[-, -]: (1\to a)\times(1\to a)\to(1+1\to a)$;
  • axioms:
    • $[f_0, f_1]\circ\iota_0 = f_0$;
    • $[f_0, f_1]\circ\iota_1 = f_1$;
    • $[f\circ\iota_0, f\circ\iota_1] = f$.

This formulation is linked with Bool and BoolC via the renaming table below and well-known isomorphisms in CCC.

Bool | BoolC | $1+1$

False | false | $\iota_0$

True | true | $\iota_1$

case t of … where t::Bool | bool | $[-, -]$

e.g.

\f t x -> case x of {False -> f; True -> t} :: a -> a -> Bool -> a

bool :: BoolC j => j a -> j a -> j Bool -> j a

$[-, -]: (1\to a)\times(1\to a)\to(1+1\to a)$

The most striking difference is that we replace $1+1, a$ in category theory with j Bool, j a in BoolC. What j is and what j does I do not know.