module Proarrow.Category.Instance.PointedHask where

import Data.Kind (Type)
import Prelude (Maybe (..), type (~), const, maybe, (>>=))

import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..))
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Data.Void (Void, absurd)
import Proarrow.Category.Monoidal (Monoidal(..), MonoidalProfunctor (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Functor (map)
import Proarrow.Category.Monoidal.Applicative (liftA2)

type data POINTED = P Type
type instance UN P (P a) = a

type Pointed :: CAT POINTED
data Pointed a b where
  P :: (Maybe a -> Maybe b) -> Pointed (P a) (P b)

instance Profunctor Pointed where
  dimap :: forall (c :: POINTED) (a :: POINTED) (b :: POINTED) (d :: POINTED).
(c ~> a) -> (b ~> d) -> Pointed a b -> Pointed c d
dimap = (c ~> a) -> (b ~> d) -> Pointed a b -> Pointed c d
Pointed c a -> Pointed b d -> Pointed a b -> Pointed 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 :: POINTED) (b :: POINTED) r.
((Ob a, Ob b) => r) -> Pointed a b -> r
\\ P{} = r
(Ob a, Ob b) => r
r
instance Promonad Pointed where
  id :: forall (a :: POINTED). Ob a => Pointed a a
id = (Maybe (UN P a) -> Maybe (UN P a))
-> Pointed (P (UN P a)) (P (UN P a))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P Maybe (UN P a) -> Maybe (UN P a)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  P Maybe a -> Maybe b
f . :: forall (b :: POINTED) (c :: POINTED) (a :: POINTED).
Pointed b c -> Pointed a b -> Pointed a c
. P Maybe a -> Maybe b
g = (Maybe a -> Maybe b) -> Pointed (P a) (P b)
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (Maybe a -> Maybe b
f (Maybe a -> Maybe b) -> (Maybe a -> Maybe a) -> Maybe a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Maybe a -> Maybe a
Maybe a -> Maybe b
g)
instance CategoryOf POINTED where
  type (~>) = Pointed
  type Ob a = (a ~ P (UN P a))

data These a b = This a | That b | These a b
instance HasBinaryProducts POINTED where
  type P a && P b = P (These a b)
  fst :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> a
fst = (Maybe (These (UN P a) (UN P b)) -> Maybe (UN P a))
-> Pointed (P (These (UN P a) (UN P b))) (P (UN P a))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (\case Maybe (These (UN P a) (UN P b))
Nothing -> Maybe (UN P a)
forall a. Maybe a
Nothing; Just (This UN P a
a) -> UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just UN P a
a; Just (That UN P b
_) -> Maybe (UN P a)
forall a. Maybe a
Nothing; Just (These UN P a
a UN P b
_) -> UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just UN P a
a)
  snd :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> b
snd = (Maybe (These (UN P a) (UN P b)) -> Maybe (UN P b))
-> Pointed (P (These (UN P a) (UN P b))) (P (UN P b))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (\case Maybe (These (UN P a) (UN P b))
Nothing -> Maybe (UN P b)
forall a. Maybe a
Nothing; Just (This UN P a
_) -> Maybe (UN P b)
forall a. Maybe a
Nothing; Just (That UN P b
b) -> UN P b -> Maybe (UN P b)
forall a. a -> Maybe a
Just UN P b
b; Just (These UN P a
_ UN P b
b) -> UN P b -> Maybe (UN P b)
forall a. a -> Maybe a
Just UN P b
b)
  P Maybe a -> Maybe b
f &&& :: forall (a :: POINTED) (x :: POINTED) (y :: POINTED).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& P Maybe a -> Maybe b
g = (Maybe a -> Maybe (These b b)) -> Pointed (P a) (P (These b b))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (\Maybe a
a -> case (Maybe a -> Maybe b
f Maybe a
a, Maybe a -> Maybe b
g Maybe a
Maybe a
a) of
    (Just b
a', Just b
b') -> These b b -> Maybe (These b b)
forall a. a -> Maybe a
Just (b -> b -> These b b
forall a b. a -> b -> These a b
These b
a' b
b')
    (Just b
a', Maybe b
Nothing) -> These b b -> Maybe (These b b)
forall a. a -> Maybe a
Just (b -> These b b
forall a b. a -> These a b
This b
a')
    (Maybe b
Nothing, Just b
b') -> These b b -> Maybe (These b b)
forall a. a -> Maybe a
Just (b -> These b b
forall a b. b -> These a b
That b
b')
    (Maybe b
Nothing, Maybe b
Nothing) -> Maybe (These b b)
forall a. Maybe a
Nothing)
instance HasTerminalObject POINTED where
  type TerminalObject = P Void
  terminate :: forall (a :: POINTED). Ob a => a ~> TerminalObject
terminate = (Maybe (UN P a) -> Maybe Void) -> Pointed (P (UN P a)) (P Void)
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (Maybe Void -> Maybe (UN P a) -> Maybe Void
forall a b. a -> b -> a
const Maybe Void
forall a. Maybe a
Nothing)

instance HasBinaryCoproducts POINTED where
  type P a || P b = P (a || b)
  lft :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => a ~> (a || b)
lft = (Maybe (UN P a) -> Maybe (Either (UN P a) (UN P b)))
-> Pointed (P (UN P a)) (P (Either (UN P a) (UN P b)))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P ((UN P a ~> Either (UN P a) (UN P b))
-> Maybe (UN P a) ~> Maybe (Either (UN P a) (UN P b))
forall a b. (a ~> b) -> Maybe a ~> Maybe b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map UN P a ~> Either (UN P a) (UN P b)
UN P a ~> (UN P a || UN P b)
forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
forall a b. (Ob a, Ob b) => a ~> (a || b)
lft)
  rgt :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => b ~> (a || b)
rgt = (Maybe (UN P b) -> Maybe (Either (UN P a) (UN P b)))
-> Pointed (P (UN P b)) (P (Either (UN P a) (UN P b)))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P ((UN P b ~> Either (UN P a) (UN P b))
-> Maybe (UN P b) ~> Maybe (Either (UN P a) (UN P b))
forall a b. (a ~> b) -> Maybe a ~> Maybe b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map UN P b ~> Either (UN P a) (UN P b)
UN P b ~> (UN P a || UN P b)
forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
forall a b. (Ob a, Ob b) => b ~> (a || b)
rgt)
  P Maybe a -> Maybe b
f ||| :: forall (x :: POINTED) (a :: POINTED) (y :: POINTED).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| P Maybe a -> Maybe b
g = (Maybe (Either a a) -> Maybe b) -> Pointed (P (Either a a)) (P b)
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (Maybe (Either a a) -> (Either a a -> Maybe b) -> Maybe b
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Maybe a -> Maybe b
f (Maybe a -> Maybe b) -> (a -> Maybe a) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> Maybe a
forall a. a -> Maybe a
Just (a ~> Maybe b) -> (a ~> Maybe b) -> (a || a) ~> Maybe b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Maybe a -> Maybe b
Maybe a -> Maybe b
g (Maybe a -> Maybe b) -> (a -> Maybe a) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> Maybe a
forall a. a -> Maybe a
Just))
instance HasInitialObject POINTED where
  type InitialObject = P Void
  initiate :: forall (a :: POINTED). Ob a => InitialObject ~> a
initiate = (Maybe Void -> Maybe (UN P a)) -> Pointed (P Void) (P (UN P a))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (Maybe (UN P a)
-> (Void -> Maybe (UN P a)) -> Maybe Void -> Maybe (UN P a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe (UN P a)
forall a. Maybe a
Nothing Void -> Maybe (UN P a)
forall a. Void -> a
absurd)

instance MonoidalProfunctor Pointed where
  par0 :: Pointed Unit Unit
par0 = (Maybe () -> Maybe ()) -> Pointed (P ()) (P ())
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P Maybe () -> Maybe ()
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  P Maybe a -> Maybe b
f par :: forall (x1 :: POINTED) (x2 :: POINTED) (y1 :: POINTED)
       (y2 :: POINTED).
Pointed x1 x2 -> Pointed y1 y2 -> Pointed (x1 ** y1) (x2 ** y2)
`par` P Maybe a -> Maybe b
g = (Maybe (a, a) -> Maybe (b, b)) -> Pointed (P (a, a)) (P (b, b))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (\case Maybe (a, a)
Nothing -> ((b && b) ~> (b, b)) -> (Maybe b && Maybe b) ~> Maybe (b, b)
forall a b c.
(Ob a, Ob b) =>
((a && b) ~> c) -> (Maybe a && Maybe b) ~> Maybe c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a && b) ~> c) -> (f a && f b) ~> f c
liftA2 (b && b) ~> (b, b)
(b, b) -> (b, b)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (Maybe a -> Maybe b
f Maybe a
forall a. Maybe a
Nothing, Maybe a -> Maybe b
g Maybe a
forall a. Maybe a
Nothing); Just (a
a, a
b) -> ((b && b) ~> (b, b)) -> (Maybe b && Maybe b) ~> Maybe (b, b)
forall a b c.
(Ob a, Ob b) =>
((a && b) ~> c) -> (Maybe a && Maybe b) ~> Maybe c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a && b) ~> c) -> (f a && f b) ~> f c
liftA2 (b && b) ~> (b, b)
(b, b) -> (b, b)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (Maybe a -> Maybe b
f (a -> Maybe a
forall a. a -> Maybe a
Just a
a), Maybe a -> Maybe b
g (a -> Maybe a
forall a. a -> Maybe a
Just a
b)))
instance Monoidal POINTED where
  type Unit = P ()
  type P a ** P b = P (a, b)
  leftUnitor :: forall (a :: POINTED). Ob a => (Unit ** a) ~> a
leftUnitor = (Maybe ((), UN P a) -> Maybe (UN P a))
-> Pointed (P ((), UN P a)) (P (UN P a))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P ((((), UN P a) ~> UN P a) -> Maybe ((), UN P a) ~> Maybe (UN P a)
forall a b. (a ~> b) -> Maybe a ~> Maybe b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((), UN P a) ~> UN P a
(() && UN P a) ~> UN P a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd)
  leftUnitorInv :: forall (a :: POINTED). Ob a => a ~> (Unit ** a)
leftUnitorInv = (Maybe (UN P a) -> Maybe ((), UN P a))
-> Pointed (P (UN P a)) (P ((), UN P a))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P ((UN P a ~> ((), UN P a)) -> Maybe (UN P a) ~> Maybe ((), UN P a)
forall a b. (a ~> b) -> Maybe a ~> Maybe b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((),))
  rightUnitor :: forall (a :: POINTED). Ob a => (a ** Unit) ~> a
rightUnitor = (Maybe (UN P a, ()) -> Maybe (UN P a))
-> Pointed (P (UN P a, ())) (P (UN P a))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (((UN P a, ()) ~> UN P a) -> Maybe (UN P a, ()) ~> Maybe (UN P a)
forall a b. (a ~> b) -> Maybe a ~> Maybe b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (UN P a, ()) ~> UN P a
(UN P a && ()) ~> UN P a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst)
  rightUnitorInv :: forall (a :: POINTED). Ob a => a ~> (a ** Unit)
rightUnitorInv = (Maybe (UN P a) -> Maybe (UN P a, ()))
-> Pointed (P (UN P a)) (P (UN P a, ()))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P ((UN P a ~> (UN P a, ())) -> Maybe (UN P a) ~> Maybe (UN P a, ())
forall a b. (a ~> b) -> Maybe a ~> Maybe b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (,()))
  associator :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (Maybe ((UN P a, UN P b), UN P c)
 -> Maybe (UN P a, (UN P b, UN P c)))
-> Pointed
     (P ((UN P a, UN P b), UN P c)) (P (UN P a, (UN P b, UN P c)))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (\case
    Maybe ((UN P a, UN P b), UN P c)
Nothing -> Maybe (UN P a, (UN P b, UN P c))
forall a. Maybe a
Nothing
    Just ((UN P a
a, UN P b
b), UN P c
c) -> (UN P a, (UN P b, UN P c)) -> Maybe (UN P a, (UN P b, UN P c))
forall a. a -> Maybe a
Just (UN P a
a, (UN P b
b, UN P c
c)))
  associatorInv :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (Maybe (UN P a, (UN P b, UN P c))
 -> Maybe ((UN P a, UN P b), UN P c))
-> Pointed
     (P (UN P a, (UN P b, UN P c))) (P ((UN P a, UN P b), UN P c))
forall a b. (Maybe a -> Maybe b) -> Pointed (P a) (P b)
P (\case
    Maybe (UN P a, (UN P b, UN P c))
Nothing -> Maybe ((UN P a, UN P b), UN P c)
forall a. Maybe a
Nothing
    Just (UN P a
a, (UN P b
b, UN P c
c)) -> ((UN P a, UN P b), UN P c) -> Maybe ((UN P a, UN P b), UN P c)
forall a. a -> Maybe a
Just ((UN P a
a, UN P b
b), UN P c
c))