Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
    
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
1  
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
2  
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

2 Answers 2

up vote 2 down vote accepted

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.

share|improve this answer

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.