module Pandora.Pattern.Functor.Covariant where
import Pandora.Core.Functor (type (:.), type (:=), type (<:=))
infixl 4 <$>, <$, $>
infixl 3 <$$>
infixl 2 <$$$>
infixl 1 <$$$$>
infixl 1 <&>
infixl 2 <&&>
infixl 3 <&&&>
infixl 4 <&&&&>
class Covariant (t :: * -> *) where
{-# MINIMAL (<$>) #-}
(<$>) :: (a -> b) -> t a -> t b
comap :: (a -> b) -> t a -> t b
comap a -> b
f t a
x = a -> b
f (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a
x
(<$) :: a -> t b -> t a
a
x <$ t b
z = (\b
_-> a
x) (b -> a) -> t b -> t a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t b
z
($>) :: t a -> b -> t b
t a
x $> b
v = b
v b -> t a -> t b
forall (t :: * -> *) a b. Covariant t => a -> t b -> t a
<$ t a
x
void :: t a -> t ()
void t a
x = () () -> t a -> t ()
forall (t :: * -> *) a b. Covariant t => a -> t b -> t a
<$ t a
x
loeb :: t (a <:= t) -> t a
loeb t (a <:= t)
tt = let fix :: (t -> t) -> t
fix t -> t
f = let x :: t
x = t -> t
f t
x in t
x in (t a -> t a) -> t a
forall t. (t -> t) -> t
fix (\t a
f -> (\a <:= t
g -> a <:= t
g t a
f) ((a <:= t) -> a) -> t (a <:= t) -> t a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t (a <:= t)
tt)
(<&>) :: t a -> (a -> b) -> t b
t a
x <&> a -> b
f = a -> b
f (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a
x
(<$$>) :: Covariant u => (a -> b) -> t :. u := a -> t :. u := b
a -> b
f <$$> (t :. u) := a
x = ((a -> b
f (a -> b) -> u a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (u a -> u b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t :. u) := a
x
(<$$$>) :: (Covariant u, Covariant v)
=> (a -> b) -> t :. u :. v := a -> t :. u :. v := b
a -> b
f <$$$> (t :. (u :. v)) := a
x = (((a -> b
f (a -> b) -> v a -> v b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (v a -> v b) -> u (v a) -> u (v b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (u (v a) -> u (v b))
-> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t :. (u :. v)) := a
x
(<$$$$>) :: (Covariant u, Covariant v, Covariant w)
=> (a -> b) -> t :. u :. v :. w := a -> t :. u :. v :. w := b
a -> b
f <$$$$> (t :. (u :. (v :. w))) := a
x = ((((a -> b
f (a -> b) -> w a -> w b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (w a -> w b) -> v (w a) -> v (w b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (v (w a) -> v (w b)) -> u (v (w a)) -> u (v (w b))
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (u (v (w a)) -> u (v (w b)))
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t :. (u :. (v :. w))) := a
x
(<&&>) :: Covariant u => t :. u := a -> (a -> b) -> t :. u := b
(t :. u) := a
x <&&> a -> b
f = a -> b
f (a -> b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (t :. u) := a
x
(<&&&>) :: (Covariant u, Covariant v)
=> t :. u :. v := a -> (a -> b) -> t :. u :. v := b
(t :. (u :. v)) := a
x <&&&> a -> b
f = a -> b
f (a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (t :. (u :. v)) := a
x
(<&&&&>) :: (Covariant u, Covariant v, Covariant w)
=> t :. u :. v :. w := a -> (a -> b) -> t :. u :. v :. w := b
(t :. (u :. (v :. w))) := a
x <&&&&> a -> b
f = a -> b
f (a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b.
(Covariant t, Covariant u, Covariant v, Covariant w) =>
(a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
<$$$$> (t :. (u :. (v :. w))) := a
x