CoSemigroup

class CoSemigroup a where
    comult :: a -> (a,a)
    comult a = (projL a, projR a)
    
    projL :: a -> a
    projL = fst . comult
    
    projR :: a -> a
    projR = snd . comult
    
    -- Laws:
    --   projL . projL = projL
    --   projR . projR = projR
    --   porjL . projR = projR . projL

Finite sum of CoSemigroup is CoSemigroup again:

type (+) = Either

instance (CoSemigroup a, CoSemigroup b) => CoSemigroup (a + b) where
    comult (Left a) = bimap Left Left (comult a)
    comult (Right b) = bimap Right Right (comult b)

instance CoSemigroup Void where
    comult = absurd

There is a way to define CoSemigroup out of law-less pair of functions.

class Split c l r | c -> l r where
    toL :: c -> Maybe l
    toR :: c -> Maybe r

data CoSemi c l r = C c | L l | R r | Term

toL', toR' :: Split c l r => c -> CoSemi c l r
toL' = maybe Term L . toL
toR' = maybe Term R . toR

instance Split c l r => CoSemigroup (CoSemi c l r) where
    comult (C c) = (toL' c, toR' c)
    comult (L l) = (L l, Term)
    comult (R r) = (Term, R r)
    comult Term = (Term, Term)

Construction from Split is in some way canonical.

Any finite CoSemigroup A is isomorphic to sum

A ~ CoSemi C0 L0 R0 + CoSemi C1 L1 R1 + ... + CoSemi C_n L_n R_n

   (C0, C1, ... are instances of Split)

Proof: Let projLR = projL . projR.

projLR :: A -> A
projLR = projL . projR

Partition A to inverse images of projLR. comult is closed under each of the inverse images, so A is isomorphic to sum of these inverse images.

For each inverse images A_i = { a : A | projLR a = i }, partition A_i into four parts:

A_i = C_i + L_i + R_i + {i}
  where
    L_i = projL(A_i) \\ {i}
    R_i = projR(A_i) \\ {i}
    C_i = A_i \\ (L_i + R_i + {i})

Note that because projL(A_i) ∩ projR(A_i) == {i}, three sets L_i, R_i, {i} are disjoint each other.

When restricted to C_i, the range of projL and projR are included in L_i + {i} and R_i + {i}, respectively.

projL' :: C_i -> L_i + {i}
projL' = projL
projR' :: C_i -> R_i + {i}
projR' = projR

Using this function, Split C_i L_i R_i instance can be implemented.

instance Split C_i L_i R_i where
    toL :: C_i -> Maybe L_i
    toL c = case projL' c of
       l | l == i    -> Nothing
         | ohterwise -> Just l
    toR :: C_i -> Maybe R_i
    toR c = case projR' c of
       r | r == i    -> Nothing
         | ohterwise -> Just r

Then CoSemi C_i L_i R_i is isomorphic to A_i as CoSemigroup.

viercc/CoSemigroup.md