-- | The thin category of booleans: objects 'FLS' and 'TRU' with one non-identity arrow
-- @'FLS' '~>' 'TRU'@, the poset @False <= True@, a.k.a. the walking arrow. It is a core type.
-- Thin categories are enriched in it ("Proarrow.Category.Enriched.Thin"), so this module depends
-- on nothing but "Proarrow.Core". The further structure of @BOOL@ (conjunction as product and
-- tensor, disjunction as coproduct, closed, star-autonomous, (co)equalizers, pullbacks\/pushouts,
-- a parameterized NNO) is instantiated in the modules that define those classes.
module Proarrow.Category.Instance.Bool where

import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, type (+->))
import Prelude qualified as P

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

deriving instance P.Eq (Booleans a b)
deriving instance P.Show (Booleans a b)

-- | Type-level conditional on a 'BOOL'.
type If :: BOOL -> k -> k -> k
type family If c t e where
  If TRU t e = t
  If FLS t e = e

-- | Negation; the 'Proarrow.Category.Monoidal.Dialogue.Dual' of @BOOL@.
type family Not (b :: BOOL) :: BOOL where
  Not FLS = TRU
  Not TRU = FLS

-- | GHC's own type-level 'P.Bool' (as produced by e.g. @<=?@ on 'GHC.TypeNats.Nat'), as a 'BOOL'.
type family FromBool (b :: P.Bool) :: BOOL where
  FromBool 'P.True = TRU
  FromBool 'P.False = FLS

class (IsBool (Not b)) => 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

-- | The category of 2 objects and one arrow between them, a.k.a. the walking arrow.
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 :: CAT 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

-- | @a <= b@ on the walking arrow, as a 'BOOL' again: the hom of the walking arrow is its own
-- internal hom.
type family BoolLeq (a :: BOOL) (b :: BOOL) :: BOOL where
  BoolLeq TRU FLS = FLS
  BoolLeq a b = TRU

-- | The four non-trivial profunctors @BOOL '+->' BOOL@, indexed by a pair of 'BOOL's selecting
-- whether the @FLS->FLS@ and @TRU->TRU@ heteromorphisms are present. @FLS->TRU@ always is.
type NonTrivialProfunctor :: (BOOL, BOOL) -> BOOL +-> BOOL
data NonTrivialProfunctor ft a b where
  FF :: NonTrivialProfunctor '(TRU, tt) FLS FLS
  FT :: NonTrivialProfunctor ft FLS TRU
  TT :: NonTrivialProfunctor '(ff, TRU) TRU TRU

deriving instance P.Eq (NonTrivialProfunctor ft a b)
deriving instance P.Show (NonTrivialProfunctor ft a b)

instance Profunctor (NonTrivialProfunctor ft) where
  dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL).
(c ~> a)
-> (b ~> d)
-> NonTrivialProfunctor ft a b
-> NonTrivialProfunctor ft c d
dimap c ~> a
Booleans c a
Fls b ~> d
Booleans b d
Fls NonTrivialProfunctor ft a b
FF = NonTrivialProfunctor ft c d
NonTrivialProfunctor '( 'TRU, tt) 'FLS 'FLS
forall (ff :: BOOL). NonTrivialProfunctor '( 'TRU, ff) 'FLS 'FLS
FF
  dimap c ~> a
Booleans c a
Fls b ~> d
Booleans b d
F2T NonTrivialProfunctor ft a b
FF = NonTrivialProfunctor ft c d
NonTrivialProfunctor ft 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
  dimap c ~> a
Booleans c a
Fls b ~> d
Booleans b d
Tru NonTrivialProfunctor ft a b
FT = NonTrivialProfunctor ft c d
NonTrivialProfunctor ft 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
  dimap c ~> a
Booleans c a
F2T b ~> d
Booleans b d
Tru NonTrivialProfunctor ft a b
TT = NonTrivialProfunctor ft c d
NonTrivialProfunctor ft 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
  dimap c ~> a
Booleans c a
Tru b ~> d
Booleans b d
Tru NonTrivialProfunctor ft a b
TT = NonTrivialProfunctor ft c d
NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU
forall (ff :: BOOL). NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU
TT
  dimap c ~> a
Booleans c a
F2T b ~> d
Booleans b d
Fls NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  dimap c ~> a
Booleans c a
Tru b ~> d
Booleans b d
Fls NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  dimap c ~> a
Booleans c a
Tru b ~> d
Booleans b d
F2T NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  dimap c ~> a
Booleans c a
F2T b ~> d
Booleans b d
F2T NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  (Ob a, Ob b) => r
r \\ :: forall (a :: BOOL) (b :: BOOL) r.
((Ob a, Ob b) => r) -> NonTrivialProfunctor ft a b -> r
\\ NonTrivialProfunctor ft a b
FF = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ NonTrivialProfunctor ft a b
FT = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ NonTrivialProfunctor ft a b
TT = r
(Ob a, Ob b) => r
r

-- | Which heteromorphisms @'NonTrivialProfunctor' '(ff, tt)@ has.
type family NonTrivialHolds (ff :: BOOL) (tt :: BOOL) (a :: BOOL) (b :: BOOL) :: BOOL where
  NonTrivialHolds ff tt FLS FLS = ff
  NonTrivialHolds ff tt FLS TRU = TRU
  NonTrivialHolds ff tt TRU TRU = tt
  NonTrivialHolds ff tt TRU FLS = FLS