module Pandora.Pattern.Functor.Contravariant where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Morphism ((!), (%))
import Pandora.Pattern.Category ((.))

infixl 4 >$<, $<, >$

{- |
> When providing a new instance, you should ensure it satisfies the two laws:
> * Identity morphism: contramap identity ≡ identity
> * Interpreted of morphisms: contramap f . contramap g ≡ contramap (g . f)
-}

class Contravariant (t :: * -> *) where
	{-# MINIMAL (>$<) #-}
	-- | Infix version of 'contramap'
	(>$<) :: (a -> b) -> t b -> t a

	-- | Prefix version of '>$<'
	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
	-- | Replace all locations in the output with the same value
	(>$) :: 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
. (!)
	-- | Flipped version of '>$'
	($<) :: 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
(>$)
	-- | Fill the input of evaluation
	full :: t () -> t a
	full t ()
x = () () -> t () -> t a
forall (t :: * -> *) b a. Contravariant t => b -> t b -> t a
>$ t ()
x
	-- | Flipped infix version of 'contramap'
	(>&<) :: 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

	-- | Infix versions of `contramap` with various nesting levels
	(>$$<) :: 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
(>$<)

	-- | Infix flipped versions of `contramap` with various nesting levels
	(>&&<) :: 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