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.