How is that three-place logic operator called?

Question

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.

Answer 1

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.

Answer 2

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.