{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}

-- | A small but non-trivial example of category <-> comonad correspondence
module Control.Comonad.Travel.Boolean where

import Control.Category
import Control.Comonad
import Control.Comonad.Travel
import Data.Bool.Singletons
import Data.Kind (Type)
import Data.Singletons.Sigma
import Prelude hiding (id, (.))

data H r = H1 r | H2 r r
  deriving ((forall a b. (a -> b) -> H a -> H b)
-> (forall a b. a -> H b -> H a) -> Functor H
forall a b. a -> H b -> H a
forall a b. (a -> b) -> H a -> H b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> H a -> H b
fmap :: forall a b. (a -> b) -> H a -> H b
$c<$ :: forall a b. a -> H b -> H a
<$ :: forall a b. a -> H b -> H a
Functor)

instance Comonad H where
  extract :: forall a. H a -> a
extract (H1 a
r) = a
r
  extract (H2 a
r a
_) = a
r

  duplicate :: forall a. H a -> H (H a)
duplicate (H1 a
r0) = H a -> H (H a)
forall r. r -> H r
H1 (a -> H a
forall r. r -> H r
H1 a
r0)
  duplicate (H2 a
r1 a
r0) = H a -> H a -> H (H a)
forall r. r -> r -> H r
H2 (a -> a -> H a
forall r. r -> r -> H r
H2 a
r1 a
r0) (a -> H a
forall r. r -> H r
H1 a
r0)

-- | Boolean algebra {False, True} can be seen as a category:
--
--   > False ---> True
--   >   ↺         ↺
--
-- Note: Roughly speaking, there are only three values in
-- types @Implies b1 b2@, where @b1, b2@ are chosen from either @False@ or @True@.
--
-- @
-- ImpId :: Implies False False
-- ImpId :: Implies True True
-- ImpFT :: Implies False True
-- @
type Implies :: Bool -> Bool -> Type
data Implies x y where
  ImpId :: Implies x x
  ImpFT :: Implies False True

instance Category Implies where
  id :: forall (a :: Bool). Implies a a
id = Implies a a
forall (a :: Bool). Implies a a
ImpId
  Implies b c
ImpId . :: forall (b :: Bool) (c :: Bool) (a :: Bool).
Implies b c -> Implies a b -> Implies a c
. Implies a b
g = Implies a b
Implies a c
g
  Implies b c
ImpFT . Implies a b
ImpId = Implies a c
Implies 'False 'True
ImpFT

-- | 'Travel' 'Implies' is isomorphic to 'H', including its 'Comonad' instance.
toH :: Travel Implies r -> H r
toH :: forall r. Travel Implies r -> H r
toH (MkTravel Sing a
SBool a
STrue Sigma Bool (TyCon (Implies a)) -> r
k) = r -> H r
forall r. r -> H r
H1 (Sigma Bool (TyCon (Implies a)) -> r
k (Sing 'True
SBool 'True
STrue Sing 'True
-> (TyCon (Implies a) @@ 'True) -> Sigma Bool (TyCon (Implies a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyCon (Implies a) @@ 'True
Implies 'True 'True
forall (a :: Bool). Implies a a
ImpId))
toH (MkTravel Sing a
SBool a
SFalse Sigma Bool (TyCon (Implies a)) -> r
k) = r -> r -> H r
forall r. r -> r -> H r
H2 (Sigma Bool (TyCon (Implies a)) -> r
k (Sing 'False
SBool 'False
SFalse Sing 'False
-> (TyCon (Implies a) @@ 'False) -> Sigma Bool (TyCon (Implies a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyCon (Implies a) @@ 'False
Implies 'False 'False
forall (a :: Bool). Implies a a
ImpId)) (Sigma Bool (TyCon (Implies a)) -> r
k (Sing 'True
SBool 'True
STrue Sing 'True
-> (TyCon (Implies a) @@ 'True) -> Sigma Bool (TyCon (Implies a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyCon (Implies a) @@ 'True
Implies 'False 'True
ImpFT))

fromH :: H r -> Travel Implies r
fromH :: forall r. H r -> Travel Implies r
fromH (H1 r
r0) = Sing 'True
-> (Sigma Bool (TyCon (Implies 'True)) -> r) -> Travel Implies r
forall k (cat :: k -> k -> *) r (a :: k).
Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
MkTravel Sing 'True
SBool 'True
STrue \(Sing fst
_ :&: TyCon (Implies 'True) @@ fst
tt) -> case TyCon (Implies 'True) @@ fst
tt of
  TyCon (Implies 'True) @@ fst
Implies 'True fst
ImpId -> r
r0
fromH (H2 r
r1 r
r0) = Sing 'False
-> (Sigma Bool (TyCon (Implies 'False)) -> r) -> Travel Implies r
forall k (cat :: k -> k -> *) r (a :: k).
Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
MkTravel Sing 'False
SBool 'False
SFalse \(Sing fst
_ :&: TyCon (Implies 'False) @@ fst
fz) -> case TyCon (Implies 'False) @@ fst
fz of
  TyCon (Implies 'False) @@ fst
Implies 'False fst
ImpId -> r
r1
  TyCon (Implies 'False) @@ fst
Implies 'False fst
ImpFT -> r
r0