# How is that three-place logic operator called?

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.

-
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. – William Sep 21 '11 at 7:15
Can you add the definition of bool for the benefit of those of us not familiar with the AwesomePrelude? – Rahul Sep 21 '11 at 7:16
Although I'm guessing it's like the ternary conditional operator (which is the same as the if-then-else in Haskell) with arguments in a funny order. – Rahul Sep 21 '11 at 7:17
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 ... – martini Sep 21 '11 at 7:26
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. – Yrogirg Sep 21 '11 at 8:51

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.

-

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.

-