| Copyright | (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and KTH's SAM group |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | alfonso.acosta@gmail.com |
| Stability | experimental (MPTC, non-standarad instances) |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell98 |
Data.TypeLevel.Bool
Description
Type-level Booleans.
- class BoolI b => Bool b
- toBool :: BoolI b => b -> Bool
- data False
- false :: False
- data True
- true :: True
- reifyBool :: Bool -> (forall b. Bool b => b -> r) -> r
- class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1
- not :: Not b1 b2 => b1 -> b2
- class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3
- (&&) :: And b1 b2 b3 => b1 -> b2 -> b3
- class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3
- (||) :: Or b1 b2 b3 => b1 -> b2 -> b3
- class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3
- xor :: Xor b1 b2 b3 => b1 -> b2 -> b3
- class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3
- imp :: Imp b1 b2 b3 => b1 -> b2 -> b3
- class (BoolI b1, BoolI b2, BoolI b3) => Eq b1 b2 b3 | b1 b2 -> b3
- eq :: Eq b1 b2 b3 => b1 -> b2 -> b3
Type-level boolean values
False type-level value
Instances
True type-level value
Instances
reifyBool :: Bool -> (forall b. Bool b => b -> r) -> r Source
Reification function. In CPS style (best possible solution)
Type-level boolean operations
class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1 Source
Boolean negation type-level relation. Not b1 b2 establishes that
not b1 = b2
class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3 Source
And type-level relation. And b1 b2 b3 establishes that
b1 && b2 = b3
(&&) :: And b1 b2 b3 => b1 -> b2 -> b3 infixr 3 Source
value-level reflection function for the And type-level relation
class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3 Source
Or type-level relation. Or b1 b2 b3 establishes that
b1 || b2 = b3
(||) :: Or b1 b2 b3 => b1 -> b2 -> b3 infixr 2 Source
value-level reflection function for the Or type-level relation
class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3 Source
Exclusive or type-level relation. Xor b1 b2 b3 establishes that
xor b1 b2 = b3
xor :: Xor b1 b2 b3 => b1 -> b2 -> b3 infixl 6 Source
value-level reflection function for the Xor type-level relation
class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3 Source
Implication type-level relation. Imp b1 b2 b3 establishes that
b1 =>b2 = b3
imp :: Imp b1 b2 b3 => b1 -> b2 -> b3 Source
value-level reflection function for the Imp type-level relation