module Proarrow.Category.Instance.PointedHask where

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

import Data.Void (Void, absurd)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Applicative (liftA2)
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Copower (Copowered (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Power (Powered (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))

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

type Pointed :: CAT POINTED
data Pointed a b where
  Pt :: {forall a b. Pointed (P a) (P b) -> a -> Maybe b
unPt :: a -> Maybe b} -> Pointed (P a) (P b)

toHask :: P a ~> P b -> (Maybe a -> Maybe b)
toHask :: forall a b. (P a ~> P b) -> Maybe a -> Maybe b
toHask (Pt a -> Maybe b
f) = (Maybe 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
>>= a -> Maybe b
f)

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 :: 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
\\ Pt{} = r
(Ob a, Ob b) => r
r
instance Promonad Pointed where
  id :: forall (a :: POINTED). Ob a => Pointed a a
id = (UN P a -> Maybe (UN P a)) -> Pointed (P (UN P a)) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just
  Pt a -> Maybe b
f . :: forall (b :: POINTED) (c :: POINTED) (a :: POINTED).
Pointed b c -> Pointed a b -> Pointed a c
. Pt a -> Maybe b
g = (a -> Maybe b) -> Pointed (P a) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\a
a -> a -> Maybe b
g a
a Maybe b -> (b -> 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
>>= a -> Maybe b
b -> Maybe b
f)

-- | The category of types with an added point and point-preserving morphisms.
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)
  withObProd :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> a
fst = (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. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\case This UN P a
a -> UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just UN P a
a; That UN P b
_ -> Maybe (UN P a)
forall a. Maybe a
Nothing; 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 = (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. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\case This UN P a
_ -> Maybe (UN P b)
forall a. Maybe a
Nothing; That UN P b
b -> UN P b -> Maybe (UN P b)
forall a. a -> Maybe a
Just UN P b
b; 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)
  Pt a -> Maybe b
f &&& :: forall (a :: POINTED) (x :: POINTED) (y :: POINTED).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Pt a -> Maybe b
g =
    (a -> Maybe (These b b)) -> Pointed (P a) (P (These b b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt
      ( \a
a -> case (a -> Maybe b
f a
a, a -> Maybe b
g a
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 = (UN P a -> Maybe Void) -> Pointed (P (UN P a)) (P Void)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Maybe Void -> 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)
  withObCoprod :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => a ~> (a || b)
lft = (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. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b))
forall a. a -> Maybe a
Just (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b)))
-> (UN P a -> Either (UN P a) (UN P b))
-> UN P a
-> Maybe (Either (UN P a) (UN P b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN P a ~> (UN P a || UN P b)
UN P a -> Either (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 = (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. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b))
forall a. a -> Maybe a
Just (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b)))
-> (UN P b -> Either (UN P a) (UN P b))
-> UN P b
-> Maybe (Either (UN P a) (UN P b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN P b ~> (UN P a || UN P b)
UN P b -> Either (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)
  Pt a -> Maybe b
f ||| :: forall (x :: POINTED) (a :: POINTED) (y :: POINTED).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Pt a -> Maybe b
g = (Either a a -> Maybe b) -> Pointed (P (Either a a)) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (a ~> Maybe b
a -> Maybe b
f (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
||| a ~> Maybe b
a -> Maybe b
g)
instance HasInitialObject POINTED where
  type InitialObject = P Void
  initiate :: forall (a :: POINTED). Ob a => InitialObject ~> a
initiate = (Void -> Maybe (UN P a)) -> Pointed (P Void) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt Void -> Maybe (UN P a)
forall a. Void -> a
absurd

instance MonoidalProfunctor Pointed where
  par0 :: Pointed Unit Unit
par0 = (() -> Maybe ()) -> Pointed (P ()) (P ())
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt () -> Maybe ()
forall a. a -> Maybe a
Just
  Pt 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` Pt a -> Maybe b
g = ((a, a) -> Maybe (b, b)) -> Pointed (P (a, a)) (P (b, b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\(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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (a -> Maybe b
f a
a, a -> Maybe b
g a
b))

-- | The smash product of pointed sets.
-- Monoids relative to the smash product are absorption monoids.
instance Monoidal POINTED where
  type Unit = P ()
  type P a ** P b = P (a, b)
  withOb2 :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: POINTED). Ob a => (Unit ** a) ~> a
leftUnitor = (((), UN P a) -> Maybe (UN P a))
-> Pointed (P ((), UN P a)) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just (UN P a -> Maybe (UN P a))
-> (((), UN P a) -> UN P a) -> ((), UN P a) -> Maybe (UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (() && 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 = (UN P a -> Maybe ((), UN P a))
-> Pointed (P (UN P a)) (P ((), UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (((), UN P a) -> Maybe ((), UN P a)
forall a. a -> Maybe a
Just (((), UN P a) -> Maybe ((), UN P a))
-> (UN P a -> ((), UN P a)) -> UN P a -> Maybe ((), UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((),))
  rightUnitor :: forall (a :: POINTED). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN P a, ()) -> Maybe (UN P a))
-> Pointed (P (UN P a, ())) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just (UN P a -> Maybe (UN P a))
-> ((UN P a, ()) -> UN P a) -> (UN P a, ()) -> Maybe (UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (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 = (UN P a -> Maybe (UN P a, ()))
-> Pointed (P (UN P a)) (P (UN P a, ()))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt ((UN P a, ()) -> Maybe (UN P a, ())
forall a. a -> Maybe a
Just ((UN P a, ()) -> Maybe (UN P a, ()))
-> (UN P a -> (UN P a, ())) -> UN P a -> Maybe (UN P a, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (,()))
  associator :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (((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. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\((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 = ((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. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\(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))

instance SymMonoidal POINTED where
  swap :: forall (a :: POINTED) (b :: POINTED).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = ((UN P a, UN P b) -> Maybe (UN P b, UN P a))
-> Pointed (P (UN P a, UN P b)) (P (UN P b, UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt ((UN P b, UN P a) -> Maybe (UN P b, UN P a)
forall a. a -> Maybe a
Just ((UN P b, UN P a) -> Maybe (UN P b, UN P a))
-> ((UN P a, UN P b) -> (UN P b, UN P a))
-> (UN P a, UN P b)
-> Maybe (UN P b, UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (UN P a ** UN P b) ~> (UN P b ** UN P a)
(UN P a, UN P b) -> (UN P b, UN P a)
forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall a b. (Ob a, Ob b) => (a ** b) ~> (b ** a)
swap)
instance Closed POINTED where
  type P a ~~> P b = P (a -> Maybe b)
  withObExp :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Pt a -> Maybe b
f) = (UN P a -> Maybe (UN P b -> Maybe b))
-> Pointed (P (UN P a)) (P (UN P b -> Maybe b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\UN P a
a -> (UN P b -> Maybe b) -> Maybe (UN P b -> Maybe b)
forall a. a -> Maybe a
Just (\UN P b
b -> a -> Maybe b
f (UN P a
a, UN P b
b)))
  uncurry :: forall (b :: POINTED) (c :: POINTED) (a :: POINTED).
(Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (Pt a -> Maybe b
f) = ((a, UN P b) -> Maybe (UN P c))
-> Pointed (P (a, UN P b)) (P (UN P c))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\(a
a, UN P b
b) -> a -> Maybe b
f a
a Maybe b -> (b -> Maybe (UN P c)) -> Maybe (UN P c)
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
>>= ((UN P b -> Maybe (UN P c)) -> UN P b -> Maybe (UN P c)
forall a b. (a -> b) -> a -> b
$ UN P b
b))

instance Powered POINTED where
  type P a ^ n = P (n -> Maybe a)
  withObPower :: forall (a :: POINTED) n r. Ob a => (Ob (a ^ n) => r) -> r
withObPower Ob (a ^ n) => r
r = r
Ob (a ^ n) => r
r
  power :: forall (a :: POINTED) (b :: POINTED) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power n -> a ~> b
f = (UN P a -> Maybe (n -> Maybe (UN P b)))
-> Pointed (P (UN P a)) (P (n -> Maybe (UN P b)))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\UN P a
a -> (n -> Maybe (UN P b)) -> Maybe (n -> Maybe (UN P b))
forall a. a -> Maybe a
Just \n
n -> Pointed (P (UN P a)) (P (UN P b)) -> UN P a -> Maybe (UN P b)
forall a b. Pointed (P a) (P b) -> a -> Maybe b
unPt (n -> a ~> b
f n
n) UN P a
a)
  unpower :: forall (b :: POINTED) (a :: POINTED) n.
Ob b =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower (Pt a -> Maybe b
f) n
n = (a -> Maybe (UN P b)) -> Pointed (P a) (P (UN P b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \a
a -> a -> Maybe b
f a
a Maybe b -> (b -> Maybe (UN P b)) -> Maybe (UN P 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
>>= ((n -> Maybe (UN P b)) -> n -> Maybe (UN P b)
forall a b. (a -> b) -> a -> b
$ n
n)

instance Copowered POINTED where
  type n *. P a = P (n, a)
  withObCopower :: forall (a :: POINTED) n r. Ob a => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: POINTED) (b :: POINTED) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower n -> a ~> b
f = ((n, UN P a) -> Maybe (UN P b))
-> Pointed (P (n, UN P a)) (P (UN P b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \(n
n, UN P a
a) -> Pointed (P (UN P a)) (P (UN P b)) -> UN P a -> Maybe (UN P b)
forall a b. Pointed (P a) (P b) -> a -> Maybe b
unPt (n -> a ~> b
f n
n) UN P a
a
  uncopower :: forall (a :: POINTED) n (b :: POINTED).
Ob a =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (Pt a -> Maybe b
f) n
n = (UN P a -> Maybe b) -> Pointed (P (UN P a)) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \UN P a
a -> a -> Maybe b
f (n
n, UN P a
a)

instance Monoid (P Void) where
  mempty :: Unit ~> P Void
mempty = (() -> Maybe Void) -> Pointed (P ()) (P Void)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Maybe Void -> () -> Maybe Void
forall a b. a -> b -> a
const Maybe Void
forall a. Maybe a
Nothing)
  mappend :: (P Void ** P Void) ~> P Void
mappend = ((Void, Void) -> Maybe Void) -> Pointed (P (Void, Void)) (P Void)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Void -> Maybe Void
forall a. a -> Maybe a
Just (Void -> Maybe Void)
-> ((Void, Void) -> Void) -> (Void, Void) -> Maybe Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Void && Void) ~> Void
(Void, Void) -> Void
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)

-- | Lift Hask monoids.
memptyDefault :: (Monoid a) => Unit ~> P a
memptyDefault :: forall a. Monoid a => Unit ~> P a
memptyDefault = (() -> Maybe a) -> Pointed (P ()) (P a)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (() -> a) -> () -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> a
() -> a
forall {k} (m :: k). Monoid m => Unit ~> m
mempty)

mappendDefault :: (Monoid a) => P a ** P a ~> P a
mappendDefault :: forall a. Monoid a => (P a ** P a) ~> P a
mappendDefault = ((a, a) -> Maybe a) -> Pointed (P (a, a)) (P a)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> ((a, a) -> a) -> (a, a) -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** a) ~> a
(a, a) -> a
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend)

-- | Conjunction with False = Nothing, True = Just ()
instance Monoid (P ()) where
  mempty :: Unit ~> P ()
mempty = Unit ~> P ()
forall a. Monoid a => Unit ~> P a
memptyDefault
  mappend :: (P () ** P ()) ~> P ()
mappend = (P () ** P ()) ~> P ()
forall a. Monoid a => (P a ** P a) ~> P a
mappendDefault

instance Monoid (P [a]) where
  mempty :: Unit ~> P [a]
mempty = Unit ~> P [a]
forall a. Monoid a => Unit ~> P a
memptyDefault
  mappend :: (P [a] ** P [a]) ~> P [a]
mappend = (P [a] ** P [a]) ~> P [a]
forall a. Monoid a => (P a ** P a) ~> P a
mappendDefault

instance Comonoid (P x) where
  counit :: P x ~> Unit
counit = (x -> Maybe ()) -> Pointed (P x) (P ())
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (() -> Maybe ()
forall a. a -> Maybe a
Just (() -> Maybe ()) -> (x -> ()) -> x -> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> Unit
x -> ()
forall {k} (c :: k). Comonoid c => c ~> Unit
counit)
  comult :: P x ~> (P x ** P x)
comult = (x -> Maybe (x, x)) -> Pointed (P x) (P (x, x))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt ((x, x) -> Maybe (x, x)
forall a. a -> Maybe a
Just ((x, x) -> Maybe (x, x)) -> (x -> (x, x)) -> x -> Maybe (x, x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> (x ** x)
x -> (x, x)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult)