Constraint.hs

{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The thin category @CONSTRAINT@ of type class constraints, with entailment @(':-')@ as arrows:
-- @a ':-' b@ holds when @a@ implies @b@. Constraint conjunction is both the categorical product and
-- the tensor of a closed symmetric monoidal structure, with @()@ as unit and terminal object.
module Proarrow.Category.Instance.Constraint (CONSTRAINT (..), (:-) (..), (:=>) (..), reifyExp, eqIsSuperOrd, maybeLiftsSemigroup) where

import Data.Kind (Constraint)
import GHC.Exts (withDict)
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.BinaryProduct qualified as P
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Monoid (..))

type data CONSTRAINT = CNSTRNT Constraint

data (:-) a b where
  Entails :: {unEntails :: forall r. (a) => ((b) => r) -> r} -> CNSTRNT a :- CNSTRNT b

-- | The category of type class constraints. An arrow from constraint a to constraint b
-- means that a implies b, i.e. if a holds then b holds.
instance CategoryOf CONSTRAINT where
  type (~>) = (:-)
  type Ob a = (Is CNSTRNT a)

instance Promonad (:-) where
  id = Entails \r -> r
  Entails f . Entails g = Entails \r -> g (f r)

instance Profunctor (:-) where
  dimap = dimapDefault
  r \\ Entails{} = r

instance ThinProfunctor (:-) where
  type HasArrow (:-) a b = UN CNSTRNT a :=> UN CNSTRNT b
  arr @(CNSTRNT a) @(CNSTRNT b) = Entails \r -> unEntails (entails @a @b) r
  withArr p@Entails{} r = reifyExp p r

instance HasTerminalObject CONSTRAINT where
  type TerminalObject = CNSTRNT ()
  terminate = Entails \r -> r

instance HasBinaryProducts CONSTRAINT where
  type CNSTRNT l && CNSTRNT r = CNSTRNT (l, r)
  withObProd r = r
  fst = Entails \r -> r
  snd = Entails \r -> r
  Entails f &&& Entails g = Entails \r -> f (g r)

instance MonoidalProfunctor (:-) where
  one = id
  f ** g = f *** g

-- | Products as monoidal structure.
instance Monoidal CONSTRAINT where
  type Unit = TerminalObject
  type a ** b = a && b
  withOb2 r = r
  leftUnitor = P.leftUnitorProd
  leftUnitorInv = P.leftUnitorProdInv
  rightUnitor = P.rightUnitorProd
  rightUnitorInv = P.rightUnitorProdInv
  associator = P.associatorProd
  associatorInv = P.associatorProdInv

instance SymMonoidal CONSTRAINT where
  swap = Entails \r -> r

instance Monoid (CNSTRNT ()) where
  mempty = id
  mappend = Entails \r -> r

instance Comonoid (CNSTRNT a) where
  counit = Entails \r -> r
  comult = Entails \r -> r
instance CocommutativeComonoid (CNSTRNT a)
instance CopyDiscard CONSTRAINT

class b :=> c where
  entails :: CNSTRNT b :- CNSTRNT c
instance ((b) => c) => (b :=> c) where
  entails = Entails \r -> r

reifyExp :: forall b c r. CNSTRNT b :- CNSTRNT c -> ((b :=> c) => r) -> r
reifyExp = withDict @(b :=> c)

instance Closed CONSTRAINT where
  type a ~~> b = CNSTRNT (UN CNSTRNT a :=> UN CNSTRNT b)
  withObExp r = r
  curry @_ @(CNSTRNT b) (Entails @_ @c f) = Entails \r -> reifyExp (Entails @b @c f) r
  apply @(CNSTRNT a) @(CNSTRNT b) = Entails \r -> unEntails (entails @a @b) r

eqIsSuperOrd :: CNSTRNT (P.Ord a) :- CNSTRNT (P.Eq a)
eqIsSuperOrd = Entails \r -> r

maybeLiftsSemigroup :: CNSTRNT (P.Semigroup a) :- CNSTRNT (Monoid (P.Maybe a))
maybeLiftsSemigroup = Entails \r -> r