1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module TypeLevel.Boolean ( True
, False
-- * Boolean operations
, Not
, notT
, And
, andT
, Or
, orT
, Xor
, xorT
) where
import TypeLevel.Reify
-- | Data type for truth
data True
-- | Data type for false.
data False
instance Show False where show _ = "False"
instance Show True where show _ = "True"
instance Reify True Bool where witness = Witness True
instance Reify False Bool where witness = Witness False
----------------------------------------------------------------
-- | Negation
type family Not a :: *
notT :: a -> Not a
notT _ = undefined
type instance Not False = True
type instance Not True = False
----------------------------------------------------------------
-- | And for boolean types
type family And a b :: *
andT :: a -> b -> And a b
andT _ _ = undefined
type instance And False False = False
type instance And False True = False
type instance And True False = False
type instance And True True = True
----------------------------------------------------------------
-- | Or for boolean types
type family Or a b :: *
orT :: a -> b -> Or a b
orT _ _ = undefined
type instance Or False False = True
type instance Or False True = True
type instance Or True False = True
type instance Or True True = False
----------------------------------------------------------------
-- | Exlusive or for boolean types
type family Xor a b :: *
xorT :: a -> b -> Xor a b
xorT _ _ = undefined
type instance Xor False False = False
type instance Xor False True = True
type instance Xor True False = True
type instance Xor True True = False
|
