-- | The category of __pointed types__: objects are Haskell types with an added point (wrapped in
-- 'P'), and a morphism is a point-preserving function, represented as @a -> Maybe b@ ('Pt'). The
-- binary product is 'These' (each component present or the point) with @Void@ as terminal object,
-- and the coproduct identifies the two points (a wedge sum).
module Proarrow.Category.Instance.PointedHask where

import Control.Monad ((>=>))
import Data.Kind (Type)
import Data.Map.Lazy qualified as Map
import Data.Map.Merge.Lazy qualified as Map
import Data.Maybe qualified as P
import Data.Void (Void, absurd)
import GHC.Generics (Generic)
import Prelude (Eq, Maybe (..), Ord, Show, const, ($), (>>=), type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Applicative (Applicative (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Copower (Copowered (..))
import Proarrow.Colimit.Initial (HasInitialObject (..), HasZeroObject (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Functor (Functor (..))
import Proarrow.Limit.BinaryProduct (FromProd (..), HasBinaryProducts (..), Prod (..))
import Proarrow.Limit.Power (Powered (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Monoid (..))

type data POINTED = P Type

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 :: 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 :: 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 -> Maybe b
g (a -> Maybe b) -> (b -> Maybe b) -> a -> Maybe b
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> 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
  deriving (These a b -> These a b -> Bool
(These a b -> These a b -> Bool)
-> (These a b -> These a b -> Bool) -> Eq (These a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => These a b -> These a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => These a b -> These a b -> Bool
== :: These a b -> These a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => These a b -> These a b -> Bool
/= :: These a b -> These a b -> Bool
Eq, Int -> These a b -> ShowS
[These a b] -> ShowS
These a b -> String
(Int -> These a b -> ShowS)
-> (These a b -> String)
-> ([These a b] -> ShowS)
-> Show (These a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> These a b -> ShowS
forall a b. (Show a, Show b) => [These a b] -> ShowS
forall a b. (Show a, Show b) => These a b -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> These a b -> ShowS
showsPrec :: Int -> These a b -> ShowS
$cshow :: forall a b. (Show a, Show b) => These a b -> String
show :: These a b -> String
$cshowList :: forall a b. (Show a, Show b) => [These a b] -> ShowS
showList :: [These a b] -> ShowS
Show, (forall x. These a b -> Rep (These a b) x)
-> (forall x. Rep (These a b) x -> These a b)
-> Generic (These a b)
forall x. Rep (These a b) x -> These a b
forall x. These a b -> Rep (These a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (These a b) x -> These a b
forall a b x. These a b -> Rep (These a b) x
$cfrom :: forall a b x. These a b -> Rep (These a b) x
from :: forall x. These a b -> Rep (These a b) x
$cto :: forall a b x. Rep (These a b) x -> These a b
to :: forall x. Rep (These a b) x -> These a b
Generic)
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 :: CAT 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 :: CAT 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
  one :: Pointed Unit Unit
one = (() -> 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 ** :: forall (x1 :: POINTED) (x2 :: POINTED) (y1 :: POINTED)
       (y2 :: POINTED).
Pointed x1 x2 -> Pointed y1 y2 -> Pointed (x1 ** y1) (x2 ** y2)
** 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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)

-- No 'Proarrow.Category.Monoidal.Closed.Closed' instance, though pointed sets are closed under the
-- smash product (<https://ncatlab.org/nlab/show/pointed+object#ClosedMonoidalStructure>): the
-- internal hom would need a type @x@ with @Maybe x ≅ (a -> Maybe b)@, the functions other than
-- @const Nothing@, and that is no Haskell type. @a -> Maybe b@ itself is too big by that one
-- function.

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

instance Copowered Type POINTED where
  type n *. P a = P (n, a)
  withObCopower :: forall (a :: POINTED) n r. (Ob a, Ob n) => (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 ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type 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 ~> HomObj Type a b
n -> Pointed (P (UN P a)) (P (UN P b))
f n
n) UN P a
a
  uncopower :: forall (a :: POINTED) n (b :: POINTED).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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)
instance CocommutativeComonoid (P x)
instance CopyDiscard POINTED

-- | Categories with a zero object can be seen as categories enriched in Pointed.
underlyingPt :: (HasZeroObject k) => (a :: k) ~> b -> Unit ~> P (a ~> b)
underlyingPt :: forall k (a :: k) (b :: k).
HasZeroObject k =>
(a ~> b) -> Unit ~> P (a ~> b)
underlyingPt a ~> b
f = (() -> Maybe (a ~> b)) -> Pointed (P ()) (P (a ~> b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \() -> (a ~> b) -> Maybe (a ~> b)
forall a. a -> Maybe a
Just a ~> b
f

enrichedPt :: (Ob (a :: k), Ob b, HasZeroObject k) => Unit ~> P (a ~> b) -> a ~> b
enrichedPt :: forall k (a :: k) (b :: k).
(Ob a, Ob b, HasZeroObject k) =>
(Unit ~> P (a ~> b)) -> a ~> b
enrichedPt (Pt a -> Maybe b
f) = b -> Maybe b -> b
forall a. a -> Maybe a -> a
P.fromMaybe b
a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
forall k (a :: k) (b :: k). (HasZeroObject k, Ob a, Ob b) => a ~> b
zero (a -> Maybe b
f ())

compPt :: (Ob (a :: k), Ob b, Ob c, HasZeroObject k) => P (b ~> c) ** P (a ~> b) ~> P (a ~> c)
compPt :: forall k (a :: k) (b :: k) (c :: k).
(Ob a, Ob b, Ob c, HasZeroObject k) =>
(P (b ~> c) ** P (a ~> b)) ~> P (a ~> c)
compPt = ((b ~> c, a ~> b) -> Maybe (a ~> c))
-> Pointed (P (b ~> c, a ~> b)) (P (a ~> c))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \(b ~> c
bc, a ~> b
ab) -> (a ~> c) -> Maybe (a ~> c)
forall a. a -> Maybe a
Just (b ~> c
bc (b ~> c) -> (a ~> b) -> a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
ab)

type FromPointed :: (Type -> Type) -> (POINTED -> Type)
data FromPointed f a where
  FromPointed :: {forall (f :: Type -> Type) a. FromPointed f (P a) -> f a
unFromPointed :: f a} -> FromPointed f (P a)

type Filterable f = Functor (FromPointed f)

mapMaybe :: (Filterable f) => (a -> Maybe b) -> f a -> f b
mapMaybe :: forall (f :: Type -> Type) a b.
Filterable f =>
(a -> Maybe b) -> f a -> f b
mapMaybe a -> Maybe b
f = FromPointed f (P b) -> f b
forall (f :: Type -> Type) a. FromPointed f (P a) -> f a
unFromPointed (FromPointed f (P b) -> f b)
-> (f a -> FromPointed f (P b)) -> f a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (P a ~> P b) -> FromPointed f (P a) ~> FromPointed f (P b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: POINTED) (b :: POINTED).
(a ~> b) -> FromPointed f a ~> FromPointed f b
map ((a -> Maybe b) -> Pointed (P a) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt a -> Maybe b
f) (FromPointed f (P a) -> FromPointed f (P b))
-> (f a -> FromPointed f (P a)) -> f a -> FromPointed f (P b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f a -> FromPointed f (P a)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed

instance Functor (FromPointed []) where
  map :: forall (a :: POINTED) (b :: POINTED).
(a ~> b) -> FromPointed [] a ~> FromPointed [] b
map (Pt a -> Maybe b
f) (FromPointed [a]
as) = [b] -> FromPointed [] (P b)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed ((a -> Maybe b) -> [a] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
P.mapMaybe a -> Maybe b
f [a]
[a]
as)

instance Functor (FromPointed (Map.Map k)) where
  map :: forall (a :: POINTED) (b :: POINTED).
(a ~> b) -> FromPointed (Map k) a ~> FromPointed (Map k) b
map (Pt a -> Maybe b
f) (FromPointed Map k a
m) = Map k b -> FromPointed (Map k) (P b)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed ((a -> Maybe b) -> Map k a -> Map k b
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe a -> Maybe b
f Map k a
Map k a
m)

-- | Not quite Align from the semialign package.
-- This requires being able to dynamically decide per position if it is included in the result.
-- So more like @merge@ from Data.Map.
type Align f = Applicative (FromProd (FromPointed f))

alignWith :: (Align f) => (These a b -> Maybe c) -> f a -> f b -> f c
alignWith :: forall (f :: Type -> Type) a b c.
Align f =>
(These a b -> Maybe c) -> f a -> f b -> f c
alignWith These a b -> Maybe c
f f a
fa f b
fb = FromPointed f (P c) -> f c
forall (f :: Type -> Type) a. FromPointed f (P a) -> f a
unFromPointed (FromPointed f (P c) -> f c) -> FromPointed f (P c) -> f c
forall a b. (a -> b) -> a -> b
$ FromProd (FromPointed f) (PR (P c)) -> FromPointed f (P c)
forall {k} (f :: k -> Type) (a :: k). FromProd f (PR a) -> f a
unFromProd (FromProd (FromPointed f) (PR (P c)) -> FromPointed f (P c))
-> FromProd (FromPointed f) (PR (P c)) -> FromPointed f (P c)
forall a b. (a -> b) -> a -> b
$ ((PR (P a) ** PR (P b)) ~> PR (P c))
-> (FromProd (FromPointed f) (PR (P a))
    ** FromProd (FromPointed f) (PR (P b)))
   ~> FromProd (FromPointed f) (PR (P 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
forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED).
(Ob a, Ob b) =>
((a ** b) ~> c)
-> (FromProd (FromPointed f) a ** FromProd (FromPointed f) b)
   ~> FromProd (FromPointed f) c
liftA2 (Pointed (P (These a b)) (P c)
-> Prod Pointed (PR (P (These a b))) (PR (P c))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((These a b -> Maybe c) -> Pointed (P (These a b)) (P c)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt These a b -> Maybe c
f)) (FromPointed f (P a) -> FromProd (FromPointed f) (PR (P a))
forall {k} (f :: k -> Type) (a1 :: k). f a1 -> FromProd f (PR a1)
FromProd (f a -> FromPointed f (P a)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed f a
fa), FromPointed f (P b) -> FromProd (FromPointed f) (PR (P b))
forall {k} (f :: k -> Type) (a1 :: k). f a1 -> FromProd f (PR a1)
FromProd (f b -> FromPointed f (P b)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed f b
fb))

nil :: (Align f) => f a
nil :: forall (f :: Type -> Type) a. Align f => f a
nil = FromPointed f (P a) -> f a
forall (f :: Type -> Type) a. FromPointed f (P a) -> f a
unFromPointed (FromPointed f (P a) -> f a) -> FromPointed f (P a) -> f a
forall a b. (a -> b) -> a -> b
$ FromProd (FromPointed f) (PR (P a)) -> FromPointed f (P a)
forall {k} (f :: k -> Type) (a :: k). FromProd f (PR a) -> f a
unFromProd (FromProd (FromPointed f) (PR (P a)) -> FromPointed f (P a))
-> FromProd (FromPointed f) (PR (P a)) -> FromPointed f (P a)
forall a b. (a -> b) -> a -> b
$ (Unit ~> PR (P a)) -> Unit ~> FromProd (FromPointed f) (PR (P a))
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
forall (a :: PROD POINTED).
(Unit ~> a) -> Unit ~> FromProd (FromPointed f) a
pure (Pointed (P Void) (P a) -> Prod Pointed (PR (P Void)) (PR (P a))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((Void -> Maybe a) -> Pointed (P Void) (P a)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Maybe a -> Void -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing))) ()

instance Applicative (FromProd (FromPointed [])) where
  pure :: forall (a :: PROD POINTED).
(Unit ~> a) -> Unit ~> FromProd (FromPointed []) a
pure Unit ~> a
a () = FromPointed [] (P (UN P (UN PR a)))
-> FromProd (FromPointed []) (PR (P (UN P (UN PR a))))
forall {k} (f :: k -> Type) (a1 :: k). f a1 -> FromProd f (PR a1)
FromProd ([UN P (UN PR a)] -> FromPointed [] (P (UN P (UN PR a)))
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed []) ((Ob (PR (P Void)), Ob a) => FromProd (FromPointed []) a)
-> Prod Pointed (PR (P Void)) a -> FromProd (FromPointed []) a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: PROD POINTED) (b :: PROD POINTED) r.
((Ob a, Ob b) => r) -> Prod Pointed a b -> r
\\ Unit ~> a
Prod Pointed (PR (P Void)) a
a
  liftA2 :: forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED).
(Ob a, Ob b) =>
((a ** b) ~> c)
-> (FromProd (FromPointed []) a ** FromProd (FromPointed []) b)
   ~> FromProd (FromPointed []) c
liftA2 (Prod (Pt a -> Maybe b
f)) (FromProd (FromPointed [a]
fa), FromProd (FromPointed [a]
fb)) = FromPointed [] (P b) -> FromProd (FromPointed []) (PR (P b))
forall {k} (f :: k -> Type) (a1 :: k). f a1 -> FromProd f (PR a1)
FromProd ([b] -> FromPointed [] (P b)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed ([a] -> [a] -> [b]
merge [a]
fa [a]
fb))
    where
      merge :: [a] -> [a] -> [b]
merge [a]
as [] = (a -> Maybe b) -> [a] -> [b]
forall (f :: Type -> Type) a b.
Filterable f =>
(a -> Maybe b) -> f a -> f b
mapMaybe (a -> Maybe b
These (UN P (UN PR a)) (UN P (UN PR b)) -> Maybe b
f (These (UN P (UN PR a)) (UN P (UN PR b)) -> Maybe b)
-> (UN P (UN PR a) -> These (UN P (UN PR a)) (UN P (UN PR b)))
-> UN P (UN PR a)
-> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN P (UN PR a) -> These (UN P (UN PR a)) (UN P (UN PR b))
forall a b. a -> These a b
This) [a]
as
      merge [] [a]
bs = (a -> Maybe b) -> [a] -> [b]
forall (f :: Type -> Type) a b.
Filterable f =>
(a -> Maybe b) -> f a -> f b
mapMaybe (a -> Maybe b
These (UN P (UN PR a)) (UN P (UN PR b)) -> Maybe b
f (These (UN P (UN PR a)) (UN P (UN PR b)) -> Maybe b)
-> (UN P (UN PR b) -> These (UN P (UN PR a)) (UN P (UN PR b)))
-> UN P (UN PR b)
-> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN P (UN PR b) -> These (UN P (UN PR a)) (UN P (UN PR b))
forall a b. b -> These a b
That) [a]
bs
      merge (a
a : [a]
as) (a
b : [a]
bs) = case a -> Maybe b
f (a -> a -> These a a
forall a b. a -> b -> These a b
These a
a a
b) of
        Maybe b
Nothing -> [a] -> [a] -> [b]
merge [a]
as [a]
bs
        Just b
c -> b
c b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [b]
merge [a]
as [a]
bs

instance (Ord k) => Applicative (FromProd (FromPointed (Map.Map k))) where
  pure :: forall (a :: PROD POINTED).
(Unit ~> a) -> Unit ~> FromProd (FromPointed (Map k)) a
pure Unit ~> a
a () = FromPointed (Map k) (P (UN P (UN PR a)))
-> FromProd (FromPointed (Map k)) (PR (P (UN P (UN PR a))))
forall {k} (f :: k -> Type) (a1 :: k). f a1 -> FromProd f (PR a1)
FromProd (Map k (UN P (UN PR a)) -> FromPointed (Map k) (P (UN P (UN PR a)))
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed Map k (UN P (UN PR a))
forall k a. Map k a
Map.empty) ((Ob (PR (P Void)), Ob a) => FromProd (FromPointed (Map k)) a)
-> Prod Pointed (PR (P Void)) a -> FromProd (FromPointed (Map k)) a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: PROD POINTED) (b :: PROD POINTED) r.
((Ob a, Ob b) => r) -> Prod Pointed a b -> r
\\ Unit ~> a
Prod Pointed (PR (P Void)) a
a
  liftA2 :: forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED).
(Ob a, Ob b) =>
((a ** b) ~> c)
-> (FromProd (FromPointed (Map k)) a
    ** FromProd (FromPointed (Map k)) b)
   ~> FromProd (FromPointed (Map k)) c
liftA2 (Prod (Pt a -> Maybe b
f)) (FromProd (FromPointed Map k a
fa), FromProd (FromPointed Map k a
fb)) = FromPointed (Map k) (P b)
-> FromProd (FromPointed (Map k)) (PR (P b))
forall {k} (f :: k -> Type) (a1 :: k). f a1 -> FromProd f (PR a1)
FromProd (Map k b -> FromPointed (Map k) (P b)
forall (f :: Type -> Type) a. f a -> FromPointed f (P a)
FromPointed (Map k a -> Map k a -> Map k b
merge Map k a
fa Map k a
fb))
    where
      merge :: Map k a -> Map k a -> Map k b
merge =
        SimpleWhenMissing k a b
-> SimpleWhenMissing k a b
-> SimpleWhenMatched k a a b
-> Map k a
-> Map k a
-> Map k b
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
Map.merge
          ((k -> a -> Maybe b) -> SimpleWhenMissing k a b
forall (f :: Type -> Type) k x y.
Applicative f =>
(k -> x -> Maybe y) -> WhenMissing f k x y
Map.mapMaybeMissing \k
_ a
a -> a -> Maybe b
f (a -> These a (UN P (UN PR b))
forall a b. a -> These a b
This a
a))
          ((k -> a -> Maybe b) -> SimpleWhenMissing k a b
forall (f :: Type -> Type) k x y.
Applicative f =>
(k -> x -> Maybe y) -> WhenMissing f k x y
Map.mapMaybeMissing \k
_ a
b -> a -> Maybe b
f (a -> These (UN P (UN PR a)) a
forall a b. b -> These a b
That a
b))
          ((k -> a -> a -> Maybe b) -> SimpleWhenMatched k a a b
forall (f :: Type -> Type) k x y z.
Applicative f =>
(k -> x -> y -> Maybe z) -> WhenMatched f k x y z
Map.zipWithMaybeMatched \k
_ a
a a
b -> a -> Maybe b
f (a -> a -> These a a
forall a b. a -> b -> These a b
These a
a a
b))