module Pandora.Pattern.Functor.Contravariant where

import Pandora.Core.Functor (type (:.), type (:=))

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
	b
x >$ t b
z = (\a
_ -> b
x) (a -> b) -> t b -> t a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$< t b
z
	-- | Flipped version of '>$'
	($<) :: t b -> b -> t a
	t b
x $< b
v = b
v b -> t b -> t a
forall (t :: * -> *) b a. Contravariant t => b -> t b -> t a
>$ t b
x
	-- | 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
	a -> b
f >$$< (t :. u) := a
x = ((a -> b
f (a -> b) -> u b -> u a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$<) (u b -> u a) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$<) (t :. u) := a
x
	(>$$$<) :: (Contravariant u, Contravariant v)
		=> (a -> b) -> t :. u :. v := b -> t :. u :. v := a
	a -> b
f >$$$< (t :. (u :. v)) := b
x = (((a -> b
f (a -> b) -> v b -> v a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$<) (v b -> v a) -> u (v a) -> u (v b)
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
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$<) (t :. (u :. v)) := b
x
	(>$$$$<) :: (Contravariant u, Contravariant v, Contravariant 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 b -> w a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$<) (w b -> w a) -> v (w a) -> v (w b)
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))
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
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$<) (t :. (u :. (v :. w))) := a
x

	-- | 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