module Proarrow.Category.Instance.Bool where
import Proarrow.Core (CAT, CategoryOf(..), Promonad(..), Profunctor(..), dimapDefault)
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..), leftUnitorProd, leftUnitorProdInv, rightUnitorProd, rightUnitorProdInv, associatorProd, associatorProdInv, swapProd)
import Proarrow.Object.Initial (HasInitialObject(..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..))
import Proarrow.Object.Exponential (Closed(..))
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal (..))
data BOOL = FLS | TRU
type Booleans :: CAT BOOL
data Booleans a b where
Fls :: Booleans FLS FLS
F2T :: Booleans FLS TRU
Tru :: Booleans TRU TRU
class IsBool (b :: BOOL) where boolId :: b ~> b
instance IsBool FLS where boolId :: 'FLS ~> 'FLS
boolId = 'FLS ~> 'FLS
Booleans 'FLS 'FLS
Fls
instance IsBool TRU where boolId :: 'TRU ~> 'TRU
boolId = 'TRU ~> 'TRU
Booleans 'TRU 'TRU
Tru
instance CategoryOf BOOL where
type (~>) = Booleans
type Ob b = IsBool b
instance Promonad Booleans where
id :: forall (a :: BOOL). Ob a => Booleans a a
id = a ~> a
Booleans a a
forall (b :: BOOL). IsBool b => b ~> b
boolId
Booleans b c
Fls . :: forall (b :: BOOL) (c :: BOOL) (a :: BOOL).
Booleans b c -> Booleans a b -> Booleans a c
. Booleans a b
Fls = Booleans a c
Booleans 'FLS 'FLS
Fls
Booleans b c
F2T . Booleans a b
Fls = Booleans a c
Booleans 'FLS 'TRU
F2T
Booleans b c
Tru . Booleans a b
F2T = Booleans a c
Booleans 'FLS 'TRU
F2T
Booleans b c
Tru . Booleans a b
Tru = Booleans a c
Booleans 'TRU 'TRU
Tru
instance Profunctor Booleans where
dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL).
(c ~> a) -> (b ~> d) -> Booleans a b -> Booleans c d
dimap = (c ~> a) -> (b ~> d) -> Booleans a b -> Booleans c d
Booleans c a -> Booleans b d -> Booleans a b -> Booleans c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
(Ob a, Ob b) => r
r \\ :: forall (a :: BOOL) (b :: BOOL) r.
((Ob a, Ob b) => r) -> Booleans a b -> r
\\ Booleans a b
Fls = r
(Ob a, Ob b) => r
r
(Ob a, Ob b) => r
r \\ Booleans a b
F2T = r
(Ob a, Ob b) => r
r
(Ob a, Ob b) => r
r \\ Booleans a b
Tru = r
(Ob a, Ob b) => r
r
instance HasTerminalObject BOOL where
type TerminalObject = TRU
terminate' :: forall (a :: BOOL). Obj a -> a ~> TerminalObject
terminate' Obj a
Booleans a a
Fls = a ~> TerminalObject
Booleans 'FLS 'TRU
F2T
terminate' Obj a
Booleans a a
Tru = a ~> TerminalObject
Booleans 'TRU 'TRU
Tru
instance HasBinaryProducts BOOL where
type TRU && TRU = TRU
type FLS && TRU = FLS
type TRU && FLS = FLS
type FLS && FLS = FLS
fst' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> (a && b) ~> a
fst' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = (a && b) ~> a
Booleans 'FLS 'FLS
Fls
fst' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = (a && b) ~> a
Booleans 'FLS 'FLS
Fls
fst' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = (a && b) ~> a
Booleans 'FLS 'TRU
F2T
fst' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = (a && b) ~> a
Booleans 'TRU 'TRU
Tru
snd' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> (a && b) ~> b
snd' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = (a && b) ~> b
Booleans 'FLS 'FLS
Fls
snd' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = (a && b) ~> b
Booleans 'FLS 'TRU
F2T
snd' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = (a && b) ~> b
Booleans 'FLS 'FLS
Fls
snd' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = (a && b) ~> b
Booleans 'TRU 'TRU
Tru
a ~> x
Booleans a x
Fls &&& :: forall (a :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
Booleans 'FLS y
Fls = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
a ~> x
Booleans a x
Fls &&& a ~> y
Booleans 'FLS y
F2T = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
a ~> x
Booleans a x
F2T &&& a ~> y
Booleans 'FLS y
Fls = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
a ~> x
Booleans a x
F2T &&& a ~> y
Booleans 'FLS y
F2T = a ~> (x && y)
Booleans 'FLS 'TRU
F2T
a ~> x
Booleans a x
Tru &&& a ~> y
Booleans 'TRU y
Tru = a ~> (x && y)
Booleans 'TRU 'TRU
Tru
instance HasInitialObject BOOL where
type InitialObject = FLS
initiate' :: forall (a :: BOOL). Obj a -> InitialObject ~> a
initiate' Obj a
Booleans a a
Fls = InitialObject ~> a
Booleans 'FLS 'FLS
Fls
initiate' Obj a
Booleans a a
Tru = InitialObject ~> a
Booleans 'FLS 'TRU
F2T
instance HasBinaryCoproducts BOOL where
type FLS || FLS = FLS
type FLS || TRU = TRU
type TRU || FLS = TRU
type TRU || TRU = TRU
lft' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> a ~> (a || b)
lft' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = a ~> (a || b)
Booleans 'FLS 'FLS
Fls
lft' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = a ~> (a || b)
Booleans 'FLS 'TRU
F2T
lft' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = a ~> (a || b)
Booleans 'TRU 'TRU
Tru
lft' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = a ~> (a || b)
Booleans 'TRU 'TRU
Tru
rgt' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> b ~> (a || b)
rgt' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = b ~> (a || b)
Booleans 'FLS 'FLS
Fls
rgt' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = b ~> (a || b)
Booleans 'TRU 'TRU
Tru
rgt' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = b ~> (a || b)
Booleans 'FLS 'TRU
F2T
rgt' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = b ~> (a || b)
Booleans 'TRU 'TRU
Tru
x ~> a
Booleans x a
Fls ||| :: forall (x :: BOOL) (a :: BOOL) (y :: BOOL).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
Booleans y 'FLS
Fls = (x || y) ~> a
Booleans 'FLS 'FLS
Fls
x ~> a
Booleans x a
F2T ||| y ~> a
Booleans y 'TRU
F2T = (x || y) ~> a
Booleans 'FLS 'TRU
F2T
x ~> a
Booleans x a
F2T ||| y ~> a
Booleans y 'TRU
Tru = (x || y) ~> a
Booleans 'TRU 'TRU
Tru
x ~> a
Booleans x a
Tru ||| y ~> a
Booleans y 'TRU
F2T = (x || y) ~> a
Booleans 'TRU 'TRU
Tru
x ~> a
Booleans x a
Tru ||| y ~> a
Booleans y 'TRU
Tru = (x || y) ~> a
Booleans 'TRU 'TRU
Tru
instance Monoidal BOOL where
type Unit = TerminalObject
type a ** b = a && b
a ~> b
f par :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL) (d :: BOOL).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
g = a ~> b
f (a ~> b) -> (c ~> d) -> (a && c) ~> (b && d)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** c ~> d
g
leftUnitor :: forall (a :: BOOL). Obj a -> (Unit ** a) ~> a
leftUnitor = (a ~> a) -> (Unit ** a) ~> a
(a ~> a) -> (TerminalObject && a) ~> a
forall k (a :: k).
HasProducts k =>
Obj a -> (TerminalObject && a) ~> a
leftUnitorProd
leftUnitorInv :: forall (a :: BOOL). Obj a -> a ~> (Unit ** a)
leftUnitorInv = (a ~> a) -> a ~> (Unit ** a)
(a ~> a) -> a ~> (TerminalObject && a)
forall k (a :: k).
HasProducts k =>
Obj a -> a ~> (TerminalObject && a)
leftUnitorProdInv
rightUnitor :: forall (a :: BOOL). Obj a -> (a ** Unit) ~> a
rightUnitor = (a ~> a) -> (a ** Unit) ~> a
(a ~> a) -> (a && TerminalObject) ~> a
forall k (a :: k).
HasProducts k =>
Obj a -> (a && TerminalObject) ~> a
rightUnitorProd
rightUnitorInv :: forall (a :: BOOL). Obj a -> a ~> (a ** Unit)
rightUnitorInv = (a ~> a) -> a ~> (a ** Unit)
(a ~> a) -> a ~> (a && TerminalObject)
forall k (a :: k).
HasProducts k =>
Obj a -> a ~> (a && TerminalObject)
rightUnitorProdInv
associator :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator = (a ~> a)
-> (b ~> b) -> (c ~> c) -> ((a ** b) ** c) ~> (a ** (b ** c))
(a ~> a)
-> (b ~> b) -> (c ~> c) -> ((a && b) && c) ~> (a && (b && c))
forall k (a :: k) (b :: k) (c :: k).
HasProducts k =>
Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c))
associatorProd
associatorInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ~> a)
-> (b ~> b) -> (c ~> c) -> (a ** (b ** c)) ~> ((a ** b) ** c)
(a ~> a)
-> (b ~> b) -> (c ~> c) -> (a && (b && c)) ~> ((a && b) && c)
forall k (a :: k) (b :: k) (c :: k).
HasProducts k =>
Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c)
associatorProdInv
instance SymMonoidal BOOL where
swap' :: forall (a :: BOOL) (b :: BOOL).
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' = (a ~> a) -> (b ~> b) -> (a ** b) ~> (b ** a)
(a ~> a) -> (b ~> b) -> (a && b) ~> (b && a)
forall {k} (a :: k) (b :: k).
HasBinaryProducts k =>
Obj a -> Obj b -> (a && b) ~> (b && a)
swapProd
instance Closed BOOL where
type FLS ~~> FLS = TRU
type FLS ~~> TRU = TRU
type TRU ~~> FLS = FLS
type TRU ~~> TRU = TRU
curry' :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
Fls = a ~> (b ~~> c)
Booleans 'FLS 'TRU
F2T
curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
F2T = a ~> (b ~~> c)
Booleans 'FLS 'TRU
F2T
curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru (a ** b) ~> c
Booleans 'FLS c
Fls = a ~> (b ~~> c)
Booleans 'FLS 'FLS
Fls
curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru (a ** b) ~> c
Booleans 'FLS c
F2T = a ~> (b ~~> c)
Booleans 'FLS 'TRU
F2T
curry' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
Fls = a ~> (b ~~> c)
Booleans 'TRU 'TRU
Tru
curry' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
F2T = a ~> (b ~~> c)
Booleans 'TRU 'TRU
Tru
curry' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru (a ** b) ~> c
Booleans 'TRU c
Tru = a ~> (b ~~> c)
Booleans 'TRU 'TRU
Tru
uncurry' :: forall (b :: BOOL) (c :: BOOL) (a :: BOOL).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Fls a ~> (b ~~> c)
Booleans a 'TRU
F2T = (a ** b) ~> c
Booleans 'FLS 'FLS
Fls
uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Fls a ~> (b ~~> c)
Booleans a 'TRU
Tru = (a ** b) ~> c
Booleans 'FLS 'FLS
Fls
uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
F2T = (a ** b) ~> c
Booleans 'FLS 'TRU
F2T
uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
Tru = (a ** b) ~> c
Booleans 'FLS 'TRU
F2T
uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Fls a ~> (b ~~> c)
Booleans a 'FLS
Fls = (a ** b) ~> c
Booleans 'FLS 'FLS
Fls
uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
F2T = (a ** b) ~> c
Booleans 'FLS 'TRU
F2T
uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
Tru = (a ** b) ~> c
Booleans 'TRU 'TRU
Tru
b ~> y
Booleans b y
Fls ^^^ :: forall (b :: BOOL) (y :: BOOL) (x :: BOOL) (a :: BOOL).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ x ~> a
Booleans x a
Fls = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
b ~> y
Booleans b y
Fls ^^^ x ~> a
Booleans x a
F2T = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'TRU
F2T
b ~> y
Booleans b y
Fls ^^^ x ~> a
Booleans x a
Tru = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'FLS
Fls
b ~> y
Booleans b y
F2T ^^^ x ~> a
Booleans x a
Fls = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
b ~> y
Booleans b y
F2T ^^^ x ~> a
Booleans x a
F2T = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'TRU
F2T
b ~> y
Booleans b y
F2T ^^^ x ~> a
Booleans x a
Tru = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'TRU
F2T
b ~> y
Booleans b y
Tru ^^^ x ~> a
Booleans x a
Fls = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
b ~> y
Booleans b y
Tru ^^^ x ~> a
Booleans x a
F2T = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
b ~> y
Booleans b y
Tru ^^^ x ~> a
Booleans x a
Tru = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru