Haskell Constraint Adjoint

Trans.hs

module Constraint.Trans where

class (forall a. c a => d (f a))
  => CFunctor c d f | f -> c, f -> d where
    -- prop> cmap id = id
    -- prop> cmap (g . f) = cmap g . cmap f
    cmap :: (c a, c b) => (a -> b) -> f a -> f b

class CFunctor c d f
  => CTrans c d f where
    -- prop> cmap f . creturn = creturn . f
    creturn :: c a => a -> f a

class (CTrans c d f, forall a. d a => c a)
  => CMonad c d f where
    cjoin :: c a => f (f a) -> f a
    cjoin = cbind id
    cbind :: (c a, c b) => (a -> f b) -> f a -> f b
    cbind f a = cjoin (cmap f a)

class CFunctor c d f
  => CCotrans c d f where
    -- prop> cextract . cmap f = f . cextract
    cextract :: d a => f a -> a

class (CCotrans c d f, forall a. d a => c a)
  => CComonad c d f where
    cduplicate :: d a => f a -> f (f a)
    cduplicate = cextend id
    cextend :: (d a, d b) => (f a -> b) -> f a -> f b
    cextend f a = cmap f (cduplicate a)

{- | @CAdjoint c d f@ witnesses an adjunction
between forgetting `forall a. d a => c a`
and `f` the free `d` generated by a `c`.
-}
class (CMonad c d f, CComonad c d f)
  => CAdjoint c d f where
    -- prop> cram f . single = f
    -- prop> cbind = cram
    -- prop> cextract = cram id
    cram :: (c a, d b) => (a -> b) -> f a -> b

class (forall f. c f => d (t f))
  => C1Functor c d t | t -> c, t -> d where
    -- prop> hoist id = id
    -- prop> hoist (g . f) = hoist g . hoist f
    hoist
      :: (c f, c g)
      => (forall x. f x -> g x)
      -> t f a -> t g a

class C1Functor c d t
  => C1Trans c d t where
    -- prop> hoist f . lift = lift . f
    lift :: c f => f a -> t f a

class (C1Trans c d t, forall f. d f => c f)
  => C1Monad c d t where
    squash :: c f => t (t f) a -> t f a
    squash = embed id
    embed
      :: (c f, c g)
      => (forall x. f x -> t g x)
      -> t f a -> t g a
    embed f a = squash (hoist f a)

class C1Functor c d t
  => C1Cotrans c d t where
    -- prop> exhume . hoist f = f . exhume
    exhume :: d f => t f a -> f a

class (C1Cotrans c d t, forall f. d f => c f)
  => C1Comonad c d t where
    diagonal :: d f => t f a -> t (t f) a
    diagonal = expand id
    expand
      :: (d f, d g)
      => (forall x. t f x -> g x)
      -> t f a -> t g a
    expand f a = hoist f (diagonal a)

{- | @C1Adjoint c d t@ witnesses an adjunction
between forgetting `forall f. d f => c f`
and `t` the free `d` generated by a `c`.
-}
class (C1Monad c d t, C1Comonad c d t)
  => C1Adjoint c d t where
    -- prop> crush f . lift = f
    -- prop> embed = crush
    -- prop> exhume = crush id
    crush
      :: (c f, d g)
      => (forall x. f x -> g x)
      -> t f a -> g a