(Strong) Promonoidal functors

Promonoidal.hs

{-# LANGUAGE TypeOperators, RankNTypes, TupleSections, GADTs, DeriveFunctor, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, TypeFamilies, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, UndecidableInstances #-}

import Data.Bifunctor
import Data.Functor.Kan.Lan
import Data.Kind (Type)
import Data.Void (Void, absurd)

type f ~> g = forall a. f a -> g a

class Bifunctor m => Tensor m where
  type U m :: Type
  leftUnit :: m (U m) a -> a
  leftUnitInv :: a -> m (U m) a
  rightUnit :: m a (U m) -> a
  rightUnitInv :: a -> m a (U m)

class (Functor f, Tensor m) => Monoidal m f where
  mult :: f a `m` f b -> f (a `m` b)
  unit :: U m -> f (U m)

class Monoidal m f => StrongMonoidal m f where
  unMult :: f (a `m` b) -> (f a `m` f b)
  unUnit :: f (U m) -> U m


instance Tensor Either where
  type U Either = Void
  leftUnit = either absurd id
  leftUnitInv = Right
  rightUnit = either id absurd
  rightUnitInv = Left

instance Tensor (,) where
  type U (,) = ()
  leftUnit = snd
  leftUnitInv = (() ,)
  rightUnit = fst
  rightUnitInv = (, ())

instance Applicative f => Monoidal (,) f where
  mult = uncurry (liftA2 (,))
  unit = pure


data Day p f g a = forall b c. Day (f b) (g c) (p (b, c) a)

class Profunctor2 p where
  dimap2 :: (d -> a) -> (e -> b) -> (c -> f) -> p (a, b) c -> p (d, e) f

class (Profunctor2 p, Functor (J p)) => Protensor p where
  type J p :: Type -> Type
  leftUnitP :: Day p (J p) ((->) a) b -> a -> b
  leftUnitInvP :: (a -> b) -> Day p (J p) ((->) a) b
  rightUnitP :: Day p ((->) a) (J p) b -> a -> b
  rightUnitInvP :: (a -> b) -> Day p ((->) a) (J p) b

class (Protensor p, Functor f) => Promonoidal p f where
  liftP :: p (a, b) c -> p (f a, f b) (f c)
  liftJ :: J p a -> J p (f a)

class Promonoidal p f => StrongPromonoidal p f where
  strongP :: p (f a, f b) ~> Lan f (p (a, b))
  strongJ :: J p ~> Lan f (J p)


data FromMonP m ab c where
  FromMonP :: { unFromMonP :: m a b -> c } -> FromMonP m (a, b) c
instance Bifunctor m => Profunctor2 (FromMonP m) where
  dimap2 f g h (FromMonP mab2c) = FromMonP (h . mab2c . bimap f g)

data FromMonJ m c where
  FromMonJ :: { unFromMonJ :: U m -> c } -> FromMonJ m c
  deriving Functor

instance Tensor m => Protensor (FromMonP m) where
  type J (FromMonP m) = FromMonJ m
  leftUnitP (Day (FromMonJ ux) ay (FromMonP yx2b)) = yx2b . bimap ux ay . leftUnitInv
  leftUnitInvP ab = Day (FromMonJ id) ab (FromMonP leftUnit)
  rightUnitP (Day ay (FromMonJ ux) (FromMonP xy2b)) = xy2b . bimap ay ux . rightUnitInv
  rightUnitInvP ab = Day ab (FromMonJ id) (FromMonP rightUnit)

instance Monoidal m f => Promonoidal (FromMonP m) f where
  liftP = FromMonP . (\f m -> f <$> mult m) . unFromMonP
  liftJ = FromMonJ . (\f u -> f <$> unit @m @f u) . unFromMonJ

instance StrongMonoidal m f => StrongPromonoidal (FromMonP m) f where
  strongP (FromMonP f) = Lan (f . unMult) $ FromMonP id
  strongJ (FromMonJ f) = Lan (f . unUnit @m @f) $ FromMonJ id


multLan :: StrongPromonoidal p h => Day p (Lan h f) (Lan h g) ~> Lan h (Day p f g)
multLan (Day (Lan h1 f) (Lan h2 g) x) = case strongP $ dimap2 h1 h2 id x of Lan w x' -> Lan w (Day f g x')

unitLan :: forall p h. StrongPromonoidal p h => J p ~> Lan h (J p)
unitLan = strongJ @p @h

unMultLan :: StrongPromonoidal p h => Lan h (Day p f g) ~> Day p (Lan h f) (Lan h g)
unMultLan (Lan w (Day f g x')) = Day (Lan id f) (Lan id g) $ dimap2 id id w $ liftP x'

unUnitLan :: forall p h. StrongPromonoidal p h => Lan h (J p) ~> J p
unUnitLan (Lan h x) = h <$> liftJ @p @h x