module Pandora.Pattern.Functor.Contravariant where
import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Morphism ((!), (%))
import Pandora.Pattern.Category ((.))
infixl 4 >$<, $<, >$
class Contravariant (t :: * -> *) where
{-# MINIMAL (>$<) #-}
(>$<) :: (a -> b) -> t b -> t a
contramap :: (a -> b) -> t b -> t a
contramap a -> b
f t b
x = a -> b
f (a -> b) -> t b -> t a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$< t b
x
(>$) :: b -> t b -> t a
(>$) = (a -> b) -> t b -> t a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
contramap ((a -> b) -> t b -> t a) -> (b -> a -> b) -> b -> t b -> t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (!)
($<) :: t b -> b -> t a
($<) = (b -> t b -> t a) -> t b -> b -> t a
forall a b c. (a -> b -> c) -> b -> a -> c
(%) b -> t b -> t a
forall (t :: * -> *) b a. Contravariant t => b -> t b -> t a
(>$)
full :: t () -> t a
full t ()
x = () () -> t () -> t a
forall (t :: * -> *) b a. Contravariant t => b -> t b -> t a
>$ t ()
x
(>&<) :: t b -> (a -> b) -> t a
t b
x >&< a -> b
f = a -> b
f (a -> b) -> t b -> t a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$< t b
x
(>$$<) :: Contravariant u => (a -> b) -> t :. u := a -> t :. u := b
(>$$<) = (u b -> u a) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<) ((u b -> u a) -> ((t :. u) := a) -> (t :. u) := b)
-> ((a -> b) -> u b -> u a)
-> (a -> b)
-> ((t :. u) := a)
-> (t :. u) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> b) -> u b -> u a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<)
(>$$$<) :: (Contravariant u, Contravariant v)
=> (a -> b) -> t :. u :. v := b -> t :. u :. v := a
(>$$$<) = (u (v a) -> u (v b))
-> ((t :. (u :. v)) := b) -> (t :. (u :. v)) := a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<) ((u (v a) -> u (v b))
-> ((t :. (u :. v)) := b) -> (t :. (u :. v)) := a)
-> ((a -> b) -> u (v a) -> u (v b))
-> (a -> b)
-> ((t :. (u :. v)) := b)
-> (t :. (u :. v)) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (v b -> v a) -> u (v a) -> u (v b)
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<) ((v b -> v a) -> u (v a) -> u (v b))
-> ((a -> b) -> v b -> v a) -> (a -> b) -> u (v a) -> u (v b)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> b) -> v b -> v a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<)
(>$$$$<) :: (Contravariant u, Contravariant v, Contravariant w)
=> (a -> b) -> t :. u :. v :. w := a -> t :. u :. v :. w := b
(>$$$$<) = (u (v (w b)) -> u (v (w a)))
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<) ((u (v (w b)) -> u (v (w a)))
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b)
-> ((a -> b) -> u (v (w b)) -> u (v (w a)))
-> (a -> b)
-> ((t :. (u :. (v :. w))) := a)
-> (t :. (u :. (v :. w))) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (v (w a) -> v (w b)) -> u (v (w b)) -> u (v (w a))
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<) ((v (w a) -> v (w b)) -> u (v (w b)) -> u (v (w a)))
-> ((a -> b) -> v (w a) -> v (w b))
-> (a -> b)
-> u (v (w b))
-> u (v (w a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (w b -> w a) -> v (w a) -> v (w b)
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<) ((w b -> w a) -> v (w a) -> v (w b))
-> ((a -> b) -> w b -> w a) -> (a -> b) -> v (w a) -> v (w b)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> b) -> w b -> w a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
(>$<)
(>&&<) :: Contravariant 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.
(Contravariant t, Contravariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
>$$< (t :. u) := a
x
(>&&&<) :: (Contravariant u, Contravariant v)
=> t :. u :. v := b -> (a -> b) -> t :. u :. v := a
(t :. (u :. v)) := b
x >&&&< a -> b
f = a -> b
f (a -> b) -> ((t :. (u :. v)) := b) -> (t :. (u :. v)) := a
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Contravariant t, Contravariant u, Contravariant v) =>
(a -> b) -> ((t :. (u :. v)) := b) -> (t :. (u :. v)) := a
>$$$< (t :. (u :. v)) := b
x
(>&&&&<) :: (Contravariant u, Contravariant v, Contravariant 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.
(Contravariant t, Contravariant u, Contravariant v,
Contravariant w) =>
(a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
>$$$$< (t :. (u :. (v :. w))) := a
x