module Pandora.Pattern.Functor.Covariant where

import Pandora.Core.Functor (type (:.), type (:=), type (<-|))
import Pandora.Pattern.Category (Category ((.), ($)))

infixl 4 <$>, <$, $>
infixl 3 <$$>
infixl 2 <$$$>
infixl 1 <$$$$>

infixl 1 <&>
infixl 2 <&&>
infixl 3 <&&&>
infixl 4 <&&&&>

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

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

	-- | Prefix version of '<$>'
	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
	-- | Replace all locations in the input with the same value
	(<$) :: a -> t b -> t a
	(<$) = (b -> a) -> t b -> t a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
comap ((b -> a) -> t b -> t a) -> (a -> b -> a) -> a -> t b -> t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (\a
x b
_ -> a
x)
	-- | Flipped version of '<$'
	($>) :: 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
	-- | Discards the result of evaluation
	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
	-- | Computing a value from a structure of values
	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) -> a <-| t
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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)
	-- | Flipped infix version of 'comap'
	(<&>) :: 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

	-- | Infix versions of `comap` with various nesting levels
	(<$$>) :: Covariant u => (a -> b) -> t :. u := a -> t :. u := b
	(<$$>) = (u a -> u b) -> ((t :. u) := a) -> (t :. u) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>) ((u a -> u b) -> ((t :. u) := a) -> (t :. u) := b)
-> ((a -> b) -> u a -> u b)
-> (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 a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>)
	(<$$$>) :: (Covariant u, Covariant v)
		=> (a -> b) -> t :. u :. v := a -> t :. u :. v := 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
(<$>) ((u (v a) -> u (v b))
 -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b)
-> ((a -> b) -> u (v a) -> u (v b))
-> (a -> b)
-> ((t :. (u :. v)) := a)
-> (t :. (u :. v)) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (v a -> v b) -> u (v a) -> u (v b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>) ((v a -> v b) -> u (v a) -> u (v b))
-> ((a -> b) -> v a -> v b) -> (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 a -> v b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>)
	(<$$$$>) :: (Covariant u, Covariant v, Covariant w)
		=> (a -> b) -> t :. u :. v :. w := a -> t :. u :. v :. w := 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
(<$>) ((u (v (w a)) -> u (v (w b)))
 -> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b)
-> ((a -> b) -> u (v (w a)) -> u (v (w b)))
-> (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 a)) -> u (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)))
-> ((a -> b) -> v (w a) -> v (w b))
-> (a -> b)
-> u (v (w a))
-> u (v (w b))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (w a -> w b) -> v (w a) -> v (w b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>) ((w a -> w b) -> v (w a) -> v (w b))
-> ((a -> b) -> w a -> w b) -> (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 a -> w b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>)

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