module UVMHS.Core.Classes.Comonad where

import UVMHS.Core.Init
import UVMHS.Core.Classes.Functors

infixr 1 =≫ 

class Extract (w ∷ ★ → ★) where extract ∷ w a → a
class Cobind (w ∷ ★ → ★) where (=≫) ∷ w a → (w a → b) → w b
class (Functor w,Extract w,Cobind w) ⇒ Comonad w

wextend ∷ (Cobind w) ⇒ (w a → b) → w a → w b
wextend :: forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
wextend w a -> b
f w a
xM = w a
xM w a -> (w a -> b) -> w b
forall a b. w a -> (w a -> b) -> w b
forall (w :: * -> *) a b. Cobind w => w a -> (w a -> b) -> w b
=≫ w a -> b
f

(%⋅) ∷ (Cobind w) ⇒ (w a → b) → w a → w b
%⋅ :: forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
(%⋅) = (w a -> b) -> w a -> w b
forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
wextend

(%$) ∷ (Cobind w) ⇒ (w a → b) → w a → w b
%$ :: forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
(%$) = (w a -> b) -> w a -> w b
forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
wextend

(%∘) ∷ (Cobind w) ⇒ (w b → c) → (w a → b) → (w a → c)
w b -> c
g %∘ :: forall (w :: * -> *) b c a.
Cobind w =>
(w b -> c) -> (w a -> b) -> w a -> c
%∘ w a -> b
f = w b -> c
g (w b -> c) -> (w a -> w b) -> w a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (w a -> b) -> w a -> w b
forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
wextend w a -> b
f

kextract ∷ (Extract w) ⇒ (a → b) → w a → b
kextract :: forall (w :: * -> *) a b. Extract w => (a -> b) -> w a -> b
kextract a -> b
f = a -> b
f (a -> b) -> (w a -> a) -> w a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ w a -> a
forall a. w a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract

kextract2 ∷ (Extract w) ⇒ (a → b → c) → w a → w b → c
kextract2 :: forall (w :: * -> *) a b c.
Extract w =>
(a -> b -> c) -> w a -> w b -> c
kextract2 a -> b -> c
f w a
xW w b
yW = a -> b -> c
f (w a -> a
forall a. w a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract w a
xW) (w b -> b
forall a. w a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract w b
yW)

siphon ∷ (Cobind w) ⇒ w a → b → w b
siphon :: forall (w :: * -> *) a b. Cobind w => w a -> b -> w b
siphon w a
xW b
y = w a
xW w a -> (w a -> b) -> w b
forall a b. w a -> (w a -> b) -> w b
forall (w :: * -> *) a b. Cobind w => w a -> (w a -> b) -> w b
=≫ \ w a
_ → b
y

submerge ∷ (Functor m,Comonad w) ⇒ w (m a) → m (w a)
submerge :: forall (m :: * -> *) (w :: * -> *) a.
(Functor m, Comonad w) =>
w (m a) -> m (w a)
submerge w (m a)
aMW = (a -> w a) -> m a -> m (w a)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (w (m a) -> a -> w a
forall (w :: * -> *) a b. Cobind w => w a -> b -> w b
siphon w (m a)
aMW) (w (m a) -> m a
forall a. w a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract w (m a)
aMW)

wmap ∷ (Comonad w) ⇒ (a → b) → w a → w b
wmap :: forall (w :: * -> *) a b. Comonad w => (a -> b) -> w a -> w b
wmap = (w a -> b) -> w a -> w b
forall (w :: * -> *) a b. Cobind w => (w a -> b) -> w a -> w b
wextend ((w a -> b) -> w a -> w b)
-> ((a -> b) -> w a -> b) -> (a -> b) -> w a -> w b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> b) -> w a -> b
forall (w :: * -> *) a b. Extract w => (a -> b) -> w a -> b
kextract