{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}


{-|
   A pseudo-inverse category is a category where every morphism has a pseudo-inverse.
-}


module Control.PseudoInverseCategory (
  -- * Classes
  ToHask (..)
  , HasHaskFunctors (..)
  , PseudoInverseCategory (..)
  , PIArrow (..)
  , piswap
  , piassoc
  -- * EndoIso
  , EndoIso (..)
  , pimap
  ) where


import qualified Control.Categorical.Functor as F
import           Control.Category            (Category (..))
import           Data.Bifunctor              (bimap, first, second)
import           Data.Functor.Identity       (Identity (..))
import           Data.Tuple                  (swap)
import           Prelude                     hiding (id, (.))


-- | A type satisfying this class is a functor from another category to Hask. Laws:
--
-- prop> piapply (f . g) = piapply f . piapply g
-- prop> piapply id = id
--
class Category a => ToHask a where
  piapply :: a x y -> x -> y


-- | For any type @a@ satisfying this class, we can lift endofunctors of Hask into @a@.
--   This mapping should constitute a functor from one monoidal category of endofunctors
--   to the other. That statement defines the applicable laws, which are, in other words:
--
--   prop> fmapA id = id
--   prop> fmapA (f >>> g) = fmapA f >>> fmapA g
class Category a => HasHaskFunctors a where
  fmapA :: Functor f => a x y -> a (f x) (f y)


-- | A pseudo-inverse category is a category where every morphism has a pseudo-inverse.
--  What this means is defined by the following laws (perhaps things can be removed
--  and perhaps things should be added):
--
-- prop> pipower 1 f = f
-- prop> pileft (pipower 0 f) = id
-- prop> piright (pipower 0 f) = id
-- prop> pipower (n+1) f = pileft f . pipower n f
-- prop> piinverse (piinverse f) = f
-- prop> f . piinverse f = piright (pipower 2 f)
-- prop> piinverse f . f = pileft (pipower 2 f)
-- prop> pileft (piright f) = piright (piright f) = piright f
-- prop> piright (pileft f) = pileft (pileft f) = pileft f
-- prop> piinverse (pileft f) = pileft f
-- prop> piinverse (piright f) = piright f
--
class Category a => PseudoInverseCategory a where
  -- | Apply a morphism /n/ times, /n/ >= 0.
  pipower :: Int -> a x y -> a x y

  -- | Change a morphism into an endomorphism of its domain.
  pileft :: a x y -> a x x

  -- | Change a morphism into an endomorphism of its codomain.
  piright :: a x y -> a y y

  -- | Pseudo-invert a morphism. The pseudo-inverse of a morphism may or may not
  --   be its inverse. @f@ is the inverse of @g@ means that @f.g = id = g.f@.
  --   If @f@ has an inverse, then @piinverse f@ may or may not be the inverse
  --   of @f@.
  piinverse :: a x y -> a y x


-- | An analogue of the Arrow typeclass for pseudo-inverse categories. Laws:
--
-- prop> piiso id id = id
-- prop> piendo id = id
-- prop> piiso (f . g) (h . i) = piiso f h . piiso g i
-- prop> piendo (f . h) = piendo f . piendo h
-- prop> pifirst (piiso f g) = piiso (first f) (first g)
-- prop> pifirst (piendo f) = piendo (first f)
-- prop> pifirst (f . g) = pifirst f . pifirst g
-- prop> pisplit id g . pifirst f = pifirst f . pisplit id g
-- prop> piassoc . first (first f) = first f . piassoc
-- prop> pisecond f = piswap . pifirst f . piswap
-- prop> pisplit f g = pifirst f . pisecond g
-- prop> pifan f g = piiso (\b -> (b,b)) fst . pisplit f g
-- prop> piinverse (piiso f g) = piiso g f
-- prop> piinverse (piendo f) = piendo f
-- prop> piapply (piiso f g) = f
-- prop> piapply (piinverse (piiso f g)) = g
-- prop> piapply (piendo f) = f
--
class PseudoInverseCategory a => PIArrow a where
  -- | Create an arrow from an isomorphism (restricted version of arr).
  piiso :: (b -> c) -> (c -> b) -> a b c

  -- | Create an arrow from an endomorphism (restricted version of arr).
  piendo :: (b -> b) -> a b b

  -- | Apply an arrow to the first coordinate of a tuple.
  pifirst :: a b c -> a (b, d) (c, d)

  -- | Apply an arrow to the second coordinate of a tuple.
  pisecond :: a b c -> a (d, b) (d, c)

  -- | Combine two arrows to work in parallel on a tuple.
  pisplit :: a b c -> a d e -> a (b, d) (c, e)

  -- | Combine two arrows on the same input to output a tuple.
  pifan :: a b c -> a b d -> a b (c, d)


-- | Every pseudo-inverse category has isomorphisms to swap the coordinates of a tuple.
piswap :: PIArrow a => a (b, c) (c, b)
piswap :: a (b, c) (c, b)
piswap = ((b, c) -> (c, b)) -> ((c, b) -> (b, c)) -> a (b, c) (c, b)
forall (a :: * -> * -> *) b c.
PIArrow a =>
(b -> c) -> (c -> b) -> a b c
piiso (b, c) -> (c, b)
forall a b. (a, b) -> (b, a)
swap (c, b) -> (b, c)
forall a b. (a, b) -> (b, a)
swap


-- | Every pseudo-inverse category has isomorphisms to change the associativity of a 3-tuple.
piassoc :: PIArrow a => a ((b,c),d) (b,(c,d))
piassoc :: a ((b, c), d) (b, (c, d))
piassoc = (((b, c), d) -> (b, (c, d)))
-> ((b, (c, d)) -> ((b, c), d)) -> a ((b, c), d) (b, (c, d))
forall (a :: * -> * -> *) b c.
PIArrow a =>
(b -> c) -> (c -> b) -> a b c
piiso (\((b
x,c
y),d
z) -> (b
x,(c
y,d
z))) (\(b
x,(c
y,d
z)) -> ((b
x,c
y),d
z))


-- | This is a pseudo-inverse category where a morphism is a composition of an endomorphism
--   on the domain and an isomorphism of the domain with the codomain.
--   The last two arguments are required to form an isomorphism, i.e. for all @EndoIso f g h@:
--
-- prop> g . h = id
-- prop> h . g = id
--
-- This category contains as objects all types in Hask and as morphisms all compositions
-- of endomorphisms and isomorphisms in Hask.
data EndoIso a b = EndoIso (a -> a) (a -> b) (b -> a)


instance Category EndoIso where
  id :: EndoIso a a
id = (a -> a) -> (a -> a) -> (a -> a) -> EndoIso a a
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

  EndoIso b -> b
i b -> c
j c -> b
k . :: EndoIso b c -> EndoIso a b -> EndoIso a c
. EndoIso a -> a
f a -> b
g b -> a
h = (a -> a) -> (a -> c) -> (c -> a) -> EndoIso a c
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso (a -> a
f (a -> a) -> (a -> a) -> a -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> a
h (b -> a) -> (a -> b) -> a -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> b
i (b -> b) -> (a -> b) -> a -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
g) (b -> c
j (b -> c) -> (a -> b) -> a -> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
g) (b -> a
h (b -> a) -> (c -> b) -> c -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c -> b
k)


instance F.Functor EndoIso (->) Identity where
  map :: EndoIso a b -> Identity a -> Identity b
map (EndoIso a -> a
f a -> b
g b -> a
_) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> (Identity a -> b) -> Identity a -> Identity b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
g (a -> b) -> (Identity a -> a) -> Identity a -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> a
f (a -> a) -> (Identity a -> a) -> Identity a -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Identity a -> a
forall a. Identity a -> a
runIdentity


instance ToHask EndoIso where
  piapply :: EndoIso x y -> x -> y
piapply (EndoIso x -> x
f x -> y
g y -> x
_) = x -> y
g(x -> y) -> (x -> x) -> x -> y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.x -> x
f


pimap :: F.Functor EndoIso EndoIso f => EndoIso a b -> f a -> f b
pimap :: EndoIso a b -> f a -> f b
pimap = (\(EndoIso f a -> f a
f f a -> f b
g f b -> f a
_) -> f a -> f b
g(f a -> f b) -> (f a -> f a) -> f a -> f b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.f a -> f a
f) (EndoIso (f a) (f b) -> f a -> f b)
-> (EndoIso a b -> EndoIso (f a) (f b))
-> EndoIso a b
-> f a
-> f b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. EndoIso a b -> EndoIso (f a) (f b)
forall α β (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β)
       (a :: α) (b :: α).
Functor s t f =>
s a b -> t (f a) (f b)
F.map


instance HasHaskFunctors EndoIso where
  fmapA :: EndoIso x y -> EndoIso (f x) (f y)
fmapA (EndoIso x -> x
f x -> y
g y -> x
h) = (f x -> f x) -> (f x -> f y) -> (f y -> f x) -> EndoIso (f x) (f y)
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso ((x -> x) -> f x -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> x
f) ((x -> y) -> f x -> f y
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> y
g) ((y -> x) -> f y -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap y -> x
h)


instance PseudoInverseCategory EndoIso where
  pipower :: Int -> EndoIso x y -> EndoIso x y
pipower Int
n (EndoIso x -> x
f x -> y
g y -> x
h)
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = [Char] -> EndoIso x y
forall a. HasCallStack => [Char] -> a
error [Char]
"pipower with n < 0"
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = let EndoIso x -> x
f' x -> y
_ y -> x
_ = Int -> EndoIso x y -> EndoIso x y
forall (a :: * -> * -> *) x y.
PseudoInverseCategory a =>
Int -> a x y -> a x y
pipower (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ((x -> x) -> (x -> y) -> (y -> x) -> EndoIso x y
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso x -> x
f x -> y
g y -> x
h) in (x -> x) -> (x -> y) -> (y -> x) -> EndoIso x y
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso (x -> x
f(x -> x) -> (x -> x) -> x -> x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.x -> x
f') x -> y
g y -> x
h
    | Bool
otherwise = (x -> x) -> (x -> y) -> (y -> x) -> EndoIso x y
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso x -> x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id x -> y
g y -> x
h
  pileft :: EndoIso x y -> EndoIso x x
pileft (EndoIso x -> x
f x -> y
_ y -> x
_) = (x -> x) -> (x -> x) -> (x -> x) -> EndoIso x x
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso x -> x
f x -> x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id x -> x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  piright :: EndoIso x y -> EndoIso y y
piright (EndoIso x -> x
f x -> y
g y -> x
h) = (y -> y) -> (y -> y) -> (y -> y) -> EndoIso y y
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso (x -> y
g(x -> y) -> (y -> x) -> y -> y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.x -> x
f(x -> x) -> (y -> x) -> y -> x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.y -> x
h) y -> y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id y -> y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  piinverse :: EndoIso x y -> EndoIso y x
piinverse (EndoIso x -> x
f x -> y
g y -> x
h) = (y -> y) -> (y -> x) -> (x -> y) -> EndoIso y x
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso (x -> y
g(x -> y) -> (y -> x) -> y -> y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.x -> x
f(x -> x) -> (y -> x) -> y -> x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.y -> x
h) y -> x
h x -> y
g


instance PIArrow EndoIso where
  piiso :: (b -> c) -> (c -> b) -> EndoIso b c
piiso = (b -> b) -> (b -> c) -> (c -> b) -> EndoIso b c
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso b -> b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  piendo :: (b -> b) -> EndoIso b b
piendo b -> b
f = (b -> b) -> (b -> b) -> (b -> b) -> EndoIso b b
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso b -> b
f b -> b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id b -> b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  pifirst :: EndoIso b c -> EndoIso (b, d) (c, d)
pifirst (EndoIso b -> b
f b -> c
g c -> b
h) = ((b, d) -> (b, d))
-> ((b, d) -> (c, d))
-> ((c, d) -> (b, d))
-> EndoIso (b, d) (c, d)
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso ((b -> b) -> (b, d) -> (b, d)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> b
f) ((b -> c) -> (b, d) -> (c, d)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> c
g) ((c -> b) -> (c, d) -> (b, d)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first c -> b
h)
  pisecond :: EndoIso b c -> EndoIso (d, b) (d, c)
pisecond (EndoIso b -> b
f b -> c
g c -> b
h) = ((d, b) -> (d, b))
-> ((d, b) -> (d, c))
-> ((d, c) -> (d, b))
-> EndoIso (d, b) (d, c)
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso ((b -> b) -> (d, b) -> (d, b)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> b
f) ((b -> c) -> (d, b) -> (d, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> c
g) ((c -> b) -> (d, c) -> (d, b)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second c -> b
h)
  pisplit :: EndoIso b c -> EndoIso d e -> EndoIso (b, d) (c, e)
pisplit (EndoIso b -> b
f b -> c
g c -> b
h) (EndoIso d -> d
i d -> e
j e -> d
k) = ((b, d) -> (b, d))
-> ((b, d) -> (c, e))
-> ((c, e) -> (b, d))
-> EndoIso (b, d) (c, e)
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso
    ((b -> b) -> (d -> d) -> (b, d) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap b -> b
f d -> d
i)
    ((b -> c) -> (d -> e) -> (b, d) -> (c, e)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap b -> c
g d -> e
j)
    ((c -> b) -> (e -> d) -> (c, e) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap c -> b
h e -> d
k)
  pifan :: EndoIso b c -> EndoIso b d -> EndoIso b (c, d)
pifan (EndoIso b -> b
f b -> c
g c -> b
h) (EndoIso b -> b
i b -> d
j d -> b
_) = (b -> b) -> (b -> (c, d)) -> ((c, d) -> b) -> EndoIso b (c, d)
forall a b. (a -> a) -> (a -> b) -> (b -> a) -> EndoIso a b
EndoIso
    (b -> b
f (b -> b) -> (b -> b) -> b -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> b
i)
    (\b
x -> (b -> c
g b
x, b -> d
j b
x))
    (\(c
x,d
_) -> c -> b
h c
x) -- it shouldn't matter which side we use to go back because we have isomorphisms