-- | 

module MonusWeightedSearch.Examples.Categorical where

import Data.Monus

-- import Control.Comonad.Trans.Cofree
-- import Control.Monad.Trans.Free
import Control.Arrow ((&&&), (|||))
import Data.Functor.Compose
import Control.Comonad
import Control.Monad
import Data.List.NonEmpty (NonEmpty(..), nonEmpty, toList)

type (+) = Either
type (*) = (,)
type (.) = Compose

-- newtype CofreeT f w a = CofreeT { runCofreeT :: w (a * f (CofreeT f w a)) }
-- newtype   FreeT f m a =   FreeT { runFreeT   :: m (a + f (  FreeT f w a)) }

-- type CoHeap w = CofreeT [] ((,) w)
-- type   Heap w =   FreeT ((,) w) []

newtype CofreeF f a k = CofreeF { forall {k} (f :: k -> Type) a (k :: k). CofreeF f a k -> a * f k
runCofreeF :: a * f k }
newtype   FreeF f a k =   FreeF { forall {k} (f :: k -> Type) a (k :: k). FreeF f a k -> a + f k
runFreeF :: a + f k }

type CofreeTF f w a = w . CofreeF f a
type CofreeT  f w a = Fix (CofreeTF f w a)

pattern CofreeT :: w (CofreeF f a (CofreeT f w a)) -> CofreeT f w a
pattern $bCofreeT :: forall (w :: Type -> Type) (f :: Type -> Type) a.
w (CofreeF f a (CofreeT f w a)) -> CofreeT f w a
$mCofreeT :: forall {r} {w :: Type -> Type} {f :: Type -> Type} {a}.
CofreeT f w a
-> (w (CofreeF f a (CofreeT f w a)) -> r) -> (Void# -> r) -> r
CofreeT {forall (w :: Type -> Type) (f :: Type -> Type) a.
CofreeT f w a -> w (CofreeF f a (CofreeT f w a))
runCofreeT} = Fix (Compose runCofreeT)
{-# COMPLETE CofreeT #-}

pattern FreeT :: m (FreeF f a (FreeT f m a)) -> FreeT f m a
pattern $bFreeT :: forall (m :: Type -> Type) (f :: Type -> Type) a.
m (FreeF f a (FreeT f m a)) -> FreeT f m a
$mFreeT :: forall {r} {m :: Type -> Type} {f :: Type -> Type} {a}.
FreeT f m a
-> (m (FreeF f a (FreeT f m a)) -> r) -> (Void# -> r) -> r
FreeT {forall (m :: Type -> Type) (f :: Type -> Type) a.
FreeT f m a -> m (FreeF f a (FreeT f m a))
runFreeT} = Fix (Compose runFreeT)
{-# COMPLETE FreeT #-}


type FreeTF f m a = m . FreeF f a
type FreeT  f m a = Fix (FreeTF f m a)

type CoHeapF w a = CofreeTF [] ((,) w) a
type   HeapF w a =   FreeTF ((,) w) [] a

type CoHeap w a = CofreeT [] ((,) w) a
type   Heap w a =   FreeT ((,) w) [] a

traceT :: (Comonad w, Functor f) => (w a -> b) -> (w a -> f (w a)) -> w a -> CofreeT f w b
traceT :: forall (w :: Type -> Type) (f :: Type -> Type) a b.
(Comonad w, Functor f) =>
(w a -> b) -> (w a -> f (w a)) -> w a -> CofreeT f w b
traceT w a -> b
f w a -> f (w a)
c w a
xs = w (CofreeF f b (CofreeT f w b)) -> CofreeT f w b
forall (w :: Type -> Type) (f :: Type -> Type) a.
w (CofreeF f a (CofreeT f w a)) -> CofreeT f w a
CofreeT ((b * f (CofreeT f w b)) -> CofreeF f b (CofreeT f w b)
forall {k} (f :: k -> Type) a (k :: k). (a * f k) -> CofreeF f a k
CofreeF ((b * f (CofreeT f w b)) -> CofreeF f b (CofreeT f w b))
-> (w a -> b * f (CofreeT f w b))
-> w a
-> CofreeF f b (CofreeT f w b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (w a -> b
f (w a -> b)
-> (w a -> f (CofreeT f w b)) -> w a -> b * f (CofreeT f w b)
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (w a -> CofreeT f w b) -> f (w a) -> f (CofreeT f w b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((w a -> b) -> (w a -> f (w a)) -> w a -> CofreeT f w b
forall (w :: Type -> Type) (f :: Type -> Type) a b.
(Comonad w, Functor f) =>
(w a -> b) -> (w a -> f (w a)) -> w a -> CofreeT f w b
traceT w a -> b
f w a -> f (w a)
c) (f (w a) -> f (CofreeT f w b))
-> (w a -> f (w a)) -> w a -> f (CofreeT f w b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w a -> f (w a)
c) (w a -> CofreeF f b (CofreeT f w b))
-> w a -> w (CofreeF f b (CofreeT f w b))
forall (w :: Type -> Type) a b.
Comonad w =>
(w a -> b) -> w a -> w b
<<= w a
xs)

evalT :: (Functor f, Monad m) => (a -> m b) -> (f (m b) -> m b) -> FreeT f m a -> m b
evalT :: forall (f :: Type -> Type) (m :: Type -> Type) a b.
(Functor f, Monad m) =>
(a -> m b) -> (f (m b) -> m b) -> FreeT f m a -> m b
evalT a -> m b
f f (m b) -> m b
a = ((a -> m b)
-> (f (FreeT f m a) -> m b) -> Either a (f (FreeT f m a)) -> m b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> m b
f (f (m b) -> m b
a (f (m b) -> m b)
-> (f (FreeT f m a) -> f (m b)) -> f (FreeT f m a) -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FreeT f m a -> m b) -> f (FreeT f m a) -> f (m b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> m b) -> (f (m b) -> m b) -> FreeT f m a -> m b
forall (f :: Type -> Type) (m :: Type -> Type) a b.
(Functor f, Monad m) =>
(a -> m b) -> (f (m b) -> m b) -> FreeT f m a -> m b
evalT a -> m b
f f (m b) -> m b
a)) (Either a (f (FreeT f m a)) -> m b)
-> (FreeF f a (FreeT f m a) -> Either a (f (FreeT f m a)))
-> FreeF f a (FreeT f m a)
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeF f a (FreeT f m a) -> Either a (f (FreeT f m a))
forall {k} (f :: k -> Type) a (k :: k). FreeF f a k -> a + f k
runFreeF) (FreeF f a (FreeT f m a) -> m b)
-> (FreeT f m a -> m (FreeF f a (FreeT f m a)))
-> FreeT f m a
-> m b
forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< FreeT f m a -> m (FreeF f a (FreeT f m a))
forall (m :: Type -> Type) (f :: Type -> Type) a.
FreeT f m a -> m (FreeF f a (FreeT f m a))
runFreeT

pattern Root :: w -> a -> [CoHeap w a] -> CoHeap w a
pattern $bRoot :: forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
$mRoot :: forall {r} {w} {a}.
CoHeap w a -> (w -> a -> [CoHeap w a] -> r) -> (Void# -> r) -> r
Root w x xs = Fix (Compose (w, CofreeF (x, xs)))
{-# COMPLETE Root #-}

pattern RootF :: w -> a -> [CoHeap w a] -> CoHeapF w a (CoHeap w a)
pattern $bRootF :: forall w a. w -> a -> [CoHeap w a] -> CoHeapF w a (CoHeap w a)
$mRootF :: forall {r} {w} {a}.
CoHeapF w a (CoHeap w a)
-> (w -> a -> [CoHeap w a] -> r) -> (Void# -> r) -> r
RootF w x xs = Compose (w, CofreeF (x, xs))
{-# COMPLETE RootF #-}

newtype Fix f = Fix { forall (f :: Type -> Type). Fix f -> f (Fix f)
unFix :: f (Fix f) }

apo :: Functor f => (a -> f (Fix f + a)) -> a -> Fix f
apo :: forall (f :: Type -> Type) a.
Functor f =>
(a -> f (Fix f + a)) -> a -> Fix f
apo a -> f (Fix f + a)
f = f (Fix f) -> Fix f
forall (f :: Type -> Type). f (Fix f) -> Fix f
Fix (f (Fix f) -> Fix f) -> (a -> f (Fix f)) -> a -> Fix f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Fix f + a) -> Fix f) -> f (Fix f + a) -> f (Fix f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Fix f -> Fix f
forall a. a -> a
id (Fix f -> Fix f) -> (a -> Fix f) -> (Fix f + a) -> Fix f
forall (a :: Type -> Type -> Type) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| (a -> f (Fix f + a)) -> a -> Fix f
forall (f :: Type -> Type) a.
Functor f =>
(a -> f (Fix f + a)) -> a -> Fix f
apo a -> f (Fix f + a)
f) (f (Fix f + a) -> f (Fix f))
-> (a -> f (Fix f + a)) -> a -> f (Fix f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f (Fix f + a)
f

cata :: Functor f => (f a -> a) -> Fix f -> a
cata :: forall (f :: Type -> Type) a. Functor f => (f a -> a) -> Fix f -> a
cata f a -> a
f = f a -> a
f (f a -> a) -> (Fix f -> f a) -> Fix f -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Fix f -> a) -> f (Fix f) -> f a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> a) -> Fix f -> a
forall (f :: Type -> Type) a. Functor f => (f a -> a) -> Fix f -> a
cata f a -> a
f) (f (Fix f) -> f a) -> (Fix f -> f (Fix f)) -> Fix f -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fix f -> f (Fix f)
forall (f :: Type -> Type). Fix f -> f (Fix f)
unFix

para :: Functor f => (f (Fix f * a) -> a) -> Fix f -> a
para :: forall (f :: Type -> Type) a.
Functor f =>
(f (Fix f * a) -> a) -> Fix f -> a
para f (Fix f * a) -> a
f = f (Fix f * a) -> a
f (f (Fix f * a) -> a) -> (Fix f -> f (Fix f * a)) -> Fix f -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Fix f -> Fix f * a) -> f (Fix f) -> f (Fix f * a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Fix f -> Fix f
forall a. a -> a
id (Fix f -> Fix f) -> (Fix f -> a) -> Fix f -> Fix f * a
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (f (Fix f * a) -> a) -> Fix f -> a
forall (f :: Type -> Type) a.
Functor f =>
(f (Fix f * a) -> a) -> Fix f -> a
para f (Fix f * a) -> a
f) (f (Fix f) -> f (Fix f * a))
-> (Fix f -> f (Fix f)) -> Fix f -> f (Fix f * a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fix f -> f (Fix f)
forall (f :: Type -> Type). Fix f -> f (Fix f)
unFix

ana :: Functor f => (a -> f a) -> a -> Fix f
ana :: forall (f :: Type -> Type) a. Functor f => (a -> f a) -> a -> Fix f
ana a -> f a
f = f (Fix f) -> Fix f
forall (f :: Type -> Type). f (Fix f) -> Fix f
Fix (f (Fix f) -> Fix f) -> (a -> f (Fix f)) -> a -> Fix f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Fix f) -> f a -> f (Fix f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> f a) -> a -> Fix f
forall (f :: Type -> Type) a. Functor f => (a -> f a) -> a -> Fix f
ana a -> f a
f) (f a -> f (Fix f)) -> (a -> f a) -> a -> f (Fix f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
f

type NEListF w a = (,) w . CofreeF Maybe a

type Pairing w a = Maybe (CoHeap w a) -> Maybe (CoHeap w a)

pcons :: Monus w => CoHeap w a -> Pairing w a -> Pairing w a
pcons :: forall w a. Monus w => CoHeap w a -> Pairing w a -> Pairing w a
pcons CoHeap w a
x  Pairing w a
k Maybe (CoHeap w a)
Nothing   = Pairing w a
k (CoHeap w a -> Maybe (CoHeap w a)
forall a. a -> Maybe a
Just CoHeap w a
x)
pcons CoHeap w a
x2 Pairing w a
k (Just CoHeap w a
x1) = CoHeap w a -> Maybe (CoHeap w a)
forall a. a -> Maybe a
Just (CoHeap w a
-> (CoHeap w a -> CoHeap w a) -> Maybe (CoHeap w a) -> CoHeap w a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CoHeap w a
x1 CoHeap w a -> CoHeap w a -> CoHeap w a
forall w a. Monus w => CoHeap w a -> CoHeap w a -> CoHeap w a
<+> CoHeap w a
x2) ((CoHeap w a
x1 CoHeap w a -> CoHeap w a -> CoHeap w a
forall w a. Monus w => CoHeap w a -> CoHeap w a -> CoHeap w a
<+> CoHeap w a
x2) CoHeap w a -> CoHeap w a -> CoHeap w a
forall w a. Monus w => CoHeap w a -> CoHeap w a -> CoHeap w a
<+>) (Pairing w a
k Maybe (CoHeap w a)
forall a. Maybe a
Nothing))

pnil :: Pairing w a
pnil :: forall w a. Pairing w a
pnil = Maybe (CoHeap w a) -> Maybe (CoHeap w a)
forall a. a -> a
id

prun :: Pairing w a -> Maybe (CoHeap w a)
prun :: forall w a. Pairing w a -> Maybe (CoHeap w a)
prun Pairing w a
xs = Pairing w a
xs Maybe (CoHeap w a)
forall a. Maybe a
Nothing

popMin :: Monus w => CoHeap w a -> NEListF w a (CoHeap w a)
popMin :: forall w a. Monus w => CoHeap w a -> NEListF w a (CoHeap w a)
popMin = (w, CofreeF Maybe a (CoHeap w a))
-> Compose ((,) w) (CofreeF Maybe a) (CoHeap w a)
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((w, CofreeF Maybe a (CoHeap w a))
 -> Compose ((,) w) (CofreeF Maybe a) (CoHeap w a))
-> (CoHeap w a -> (w, CofreeF Maybe a (CoHeap w a)))
-> CoHeap w a
-> Compose ((,) w) (CofreeF Maybe a) (CoHeap w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CofreeF [] a (CoHeap w a) -> CofreeF Maybe a (CoHeap w a))
-> (w, CofreeF [] a (CoHeap w a))
-> (w, CofreeF Maybe a (CoHeap w a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap  ((a * Maybe (CoHeap w a)) -> CofreeF Maybe a (CoHeap w a)
forall {k} (f :: k -> Type) a (k :: k). (a * f k) -> CofreeF f a k
CofreeF ((a * Maybe (CoHeap w a)) -> CofreeF Maybe a (CoHeap w a))
-> (CofreeF [] a (CoHeap w a) -> a * Maybe (CoHeap w a))
-> CofreeF [] a (CoHeap w a)
-> CofreeF Maybe a (CoHeap w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([CoHeap w a] -> Maybe (CoHeap w a))
-> (a, [CoHeap w a]) -> a * Maybe (CoHeap w a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pairing w a -> Maybe (CoHeap w a)
forall w a. Pairing w a -> Maybe (CoHeap w a)
prun (Pairing w a -> Maybe (CoHeap w a))
-> ([CoHeap w a] -> Pairing w a)
-> [CoHeap w a]
-> Maybe (CoHeap w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoHeap w a -> Pairing w a -> Pairing w a)
-> Pairing w a -> [CoHeap w a] -> Pairing w a
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr CoHeap w a -> Pairing w a -> Pairing w a
forall w a. Monus w => CoHeap w a -> Pairing w a -> Pairing w a
pcons Pairing w a
forall w a. Pairing w a
pnil) ((a, [CoHeap w a]) -> a * Maybe (CoHeap w a))
-> (CofreeF [] a (CoHeap w a) -> (a, [CoHeap w a]))
-> CofreeF [] a (CoHeap w a)
-> a * Maybe (CoHeap w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CofreeF [] a (CoHeap w a) -> (a, [CoHeap w a])
forall {k} (f :: k -> Type) a (k :: k). CofreeF f a k -> a * f k
runCofreeF) ((w, CofreeF [] a (CoHeap w a))
 -> (w, CofreeF Maybe a (CoHeap w a)))
-> (CoHeap w a -> (w, CofreeF [] a (CoHeap w a)))
-> CoHeap w a
-> (w, CofreeF Maybe a (CoHeap w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose ((,) w) (CofreeF [] a) (CoHeap w a)
-> (w, CofreeF [] a (CoHeap w a))
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose ((,) w) (CofreeF [] a) (CoHeap w a)
 -> (w, CofreeF [] a (CoHeap w a)))
-> (CoHeap w a -> Compose ((,) w) (CofreeF [] a) (CoHeap w a))
-> CoHeap w a
-> (w, CofreeF [] a (CoHeap w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoHeap w a -> Compose ((,) w) (CofreeF [] a) (CoHeap w a)
forall (f :: Type -> Type). Fix f -> f (Fix f)
unFix

(<+>) :: Monus w => CoHeap w a -> CoHeap w a -> CoHeap w a
Root w
xw a
x [CoHeap w a]
xs <+> :: forall w a. Monus w => CoHeap w a -> CoHeap w a -> CoHeap w a
<+> Root w
yw a
y [CoHeap w a]
ys
  | w
xw w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
yw  = w -> a -> [CoHeap w a] -> CoHeap w a
forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
Root w
xw a
x (w -> a -> [CoHeap w a] -> CoHeap w a
forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
Root (w
yw w -> w -> w
forall a. Monus a => a -> a -> a
|-| w
xw) a
y [CoHeap w a]
ys CoHeap w a -> [CoHeap w a] -> [CoHeap w a]
forall a. a -> [a] -> [a]
: [CoHeap w a]
xs)
  | Bool
otherwise = w -> a -> [CoHeap w a] -> CoHeap w a
forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
Root w
yw a
y (w -> a -> [CoHeap w a] -> CoHeap w a
forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
Root (w
xw w -> w -> w
forall a. Monus a => a -> a -> a
|-| w
yw) a
x [CoHeap w a]
xs CoHeap w a -> [CoHeap w a] -> [CoHeap w a]
forall a. a -> [a] -> [a]
: [CoHeap w a]
ys)


-- Action   :: m -> a -> a
-- coaction :: a -> (m, a)

-- | A class for things that can be decomposed in a coassiciative way.
--
-- split x == (y :| []) ==> x == y
-- all unital (unfoldr split x) where unital x = snd x == Nothing
    
class Comonoid a where
  split :: a -> (a, Maybe a)
  
class Comonoid' a where
  split' :: a -> NonEmpty a

instance Comonoid (NonEmpty a) where
  split :: NonEmpty a -> (NonEmpty a, Maybe (NonEmpty a))
split (a
x :| [a]
xs) = (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [], [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [a]
xs)
  
instance Comonoid' (NonEmpty a) where
  split' :: NonEmpty a -> NonEmpty (NonEmpty a)
split' = (a -> NonEmpty a) -> NonEmpty a -> NonEmpty (NonEmpty a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> NonEmpty a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure

instance Comonoid Word where
  split :: Word -> (Word, Maybe Word)
split Word
0 = (Word
0, Maybe Word
forall a. Maybe a
Nothing)
  split Word
n = (Word
0, Word -> Maybe Word
forall a. a -> Maybe a
Just (Word
nWord -> Word -> Word
forall a. Num a => a -> a -> a
-Word
1))
  
instance Comonoid' Word where
  split' :: Word -> NonEmpty Word
split' Word
n = Word
0 Word -> [Word] -> NonEmpty Word
forall a. a -> [a] -> NonEmpty a
:| Int -> Word -> [Word]
forall a. Int -> a -> [a]
replicate (Word -> Int
forall a. Enum a => a -> Int
fromEnum Word
n) Word
0


instance Comonoid (CoHeap w a) where
  split :: CoHeap w a -> (CoHeap w a, Maybe (CoHeap w a))
split (Root w
w a
x [CoHeap w a]
xs) = (w -> a -> [CoHeap w a] -> CoHeap w a
forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
Root w
w a
x [], [CoHeap w a] -> Maybe (CoHeap w a)
forall {w} {a}. [CoHeap w a] -> Maybe (CoHeap w a)
go [CoHeap w a]
xs)
    where
      go :: [CoHeap w a] -> Maybe (CoHeap w a)
go [] = Maybe (CoHeap w a)
forall a. Maybe a
Nothing
      go (Root w
w a
x [CoHeap w a]
xs : [CoHeap w a]
xss) = CoHeap w a -> Maybe (CoHeap w a)
forall a. a -> Maybe a
Just (w -> a -> [CoHeap w a] -> CoHeap w a
forall w a. w -> a -> [CoHeap w a] -> CoHeap w a
Root w
w a
x ([CoHeap w a]
xs [CoHeap w a] -> [CoHeap w a] -> [CoHeap w a]
forall a. [a] -> [a] -> [a]
++ [CoHeap w a]
xss))
  
-- instance Comonoid' (CoHeap w a) where
--   split' (Root w x xs) = Root w x [] :| xs

-- -- instance Comonoid [a] where
-- --   split (x1:x2:xs) = ([x1], Just (x2:xs))
-- --   split xs = (xs, Nothing)

-- law :: (Comonoid' a, Eq a) => a -> Either Bool ()
-- law xs = either id (const False) $ do
--     (y1,y2:| ys) <- split'' xs
    
    
--   where
--     split'' x = case split' x of
--       (y :| []) -> Left (x == y)
--       (y1 :| y2 : ys) -> Right (y1, y2 :| ys)