{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

{-# OPTIONS_GHC -Wall #-}

-- | Category of Isomorphisms.

module ConCat.Isomorphism where

import Prelude hiding (id, (.), const, curry,uncurry)  -- Coming from ConCat.AltCat.

import Data.Functor.Rep (Representable(..))
-- import Control.Applicative (liftA2)
-- import Data.Coerce (Coercible,coerce)
import Control.Newtype.Generics
import qualified GHC.Generics as G
import Data.Constraint (Dict(..),(:-)(..))

import ConCat.Misc ((:+),(:*),(:=>))
import ConCat.AltCat
import qualified ConCat.Category
import qualified ConCat.Rep as R

infix 0 :<->
data Iso k a b = (a `k` b) :<-> (b `k` a)

-- Helpful?
instance R.HasRep (Iso k a b) where
  type Rep (Iso k a b) = (a `k` b) :* (b `k` a)
  abst :: Rep (Iso k a b) -> Iso k a b
abst (k a b
f,k b a
f') = k a b
f k a b -> k b a -> Iso k a b
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k b a
f'
  repr :: Iso k a b -> Rep (Iso k a b)
repr (k a b
f :<-> k b a
f') = (k a b
f,k b a
f')

inv :: Iso k a b -> Iso k b a
inv :: forall (k :: * -> * -> *) a b. Iso k a b -> Iso k b a
inv (k a b
f :<-> k b a
f') = k b a
f' k b a -> k a b -> Iso k b a
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a b
f
{-# INLINE inv #-}

-- | Form an ivolution from a _self-inverse_ arrow.
involution :: (a `k` a) -> Iso k a a
involution :: forall (k :: * -> * -> *) a. k a a -> Iso k a a
involution k a a
f = k a a
f k a a -> k a a -> Iso k a a
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a a
f

instance Category k => Category (Iso k) where
  type Ok (Iso k) = Ok k
  id :: forall a. Ok (Iso k) a => Iso k a a
id = k a a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id k a a -> k a a -> Iso k a a
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  (k b c
g :<-> k c b
g') . :: forall b c a.
Ok3 (Iso k) a b c =>
Iso k b c -> Iso k a b -> Iso k a c
. (k a b
f :<-> k b a
f') = (k b c
g k b c -> k a b -> k a c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a b
f) k a c -> k c a -> Iso k a c
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> (k b a
f' k b a -> k c b -> k c a
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k c b
g')
  {- INLINE id #-}
  {- INLINE (.) #-}

instance AssociativePCat k => AssociativePCat (Iso k) where
  lassocP :: forall a b c.
Ok3 (Iso k) a b c =>
Iso
  k
  (Prod (Iso k) a (Prod (Iso k) b c))
  (Prod (Iso k) (Prod (Iso k) a b) c)
lassocP = k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
-> k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
-> Iso k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP
  rassocP :: forall a b c.
Ok3 (Iso k) a b c =>
Iso
  k
  (Prod (Iso k) (Prod (Iso k) a b) c)
  (Prod (Iso k) a (Prod (Iso k) b c))
rassocP = k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
-> k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
-> Iso k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP
  {- INLINE lassocP #-}
  {- INLINE rassocP #-}

instance BraidedPCat k => BraidedPCat (Iso k) where
  swapP :: forall a b.
Ok2 (Iso k) a b =>
Iso k (Prod (Iso k) a b) (Prod (Iso k) b a)
swapP = k (Prod k a b) (Prod k b a)
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP k (Prod k a b) (Prod k b a)
-> k (Prod k b a) (Prod k a b) -> Iso k (Prod k a b) (Prod k b a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Prod k b a) (Prod k a b)
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP
  {-# INLINE swapP #-}

instance MonoidalPCat k => MonoidalPCat (Iso k) where
  (k a c
f :<-> k c a
f') *** :: forall a b c d.
Ok4 (Iso k) a b c d =>
Iso k a c
-> Iso k b d -> Iso k (Prod (Iso k) a b) (Prod (Iso k) c d)
*** (k b d
g :<-> k d b
g') = (k a c
f k a c -> k b d -> k (Prod k a b) (Prod k c d)
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod k a b) (Prod k c d)
*** k b d
g) k (Prod k a b) (Prod k c d)
-> k (Prod k c d) (Prod k a b) -> Iso k (Prod k a b) (Prod k c d)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> (k c a
f' k c a -> k d b -> k (Prod k c d) (Prod k a b)
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod k a b) (Prod k c d)
*** k d b
g')
  {- INLINE (***) #-}

instance AssociativeSCat k => AssociativeSCat (Iso k) where
  lassocS :: forall a b c.
Oks (Iso k) '[a, b, c] =>
Iso
  k
  (Coprod (Iso k) a (Coprod (Iso k) b c))
  (Coprod (Iso k) (Coprod (Iso k) a b) c)
lassocS = k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
forall (k :: * -> * -> *) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
lassocS k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
-> k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
-> Iso k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
forall (k :: * -> * -> *) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
rassocS
  rassocS :: forall a b c.
Oks (Iso k) '[a, b, c] =>
Iso
  k
  (Coprod (Iso k) (Coprod (Iso k) a b) c)
  (Coprod (Iso k) a (Coprod (Iso k) b c))
rassocS = k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
forall (k :: * -> * -> *) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
rassocS k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
-> k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
-> Iso k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
forall (k :: * -> * -> *) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
lassocS
  {- INLINE lassocS #-}
  {- INLINE rassocS #-}

instance MonoidalSCat k => MonoidalSCat (Iso k) where
  (k c a
f :<-> k a c
f') +++ :: forall a b c d.
Ok4 (Iso k) a b c d =>
Iso k c a
-> Iso k d b -> Iso k (Coprod (Iso k) c d) (Coprod (Iso k) a b)
+++ (k d b
g :<-> k b d
g') = (k c a
f k c a -> k d b -> k (Coprod k c d) (Coprod k a b)
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod k c d) (Coprod k a b)
+++ k d b
g) k (Coprod k c d) (Coprod k a b)
-> k (Coprod k a b) (Coprod k c d)
-> Iso k (Coprod k c d) (Coprod k a b)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> (k a c
f' k a c -> k b d -> k (Coprod k a b) (Coprod k c d)
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod k c d) (Coprod k a b)
+++ k b d
g')
  {- INLINE (+++) #-}

instance BraidedSCat k => BraidedSCat (Iso k) where
  swapS :: forall a b.
Ok2 (Iso k) a b =>
Iso k (Coprod (Iso k) a b) (Coprod (Iso k) b a)
swapS = k (Coprod k a b) (Coprod k b a)
forall (k :: * -> * -> *) a b.
(BraidedSCat k, Ok2 k a b) =>
k (Coprod k a b) (Coprod k b a)
swapS k (Coprod k a b) (Coprod k b a)
-> k (Coprod k b a) (Coprod k a b)
-> Iso k (Coprod k a b) (Coprod k b a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Coprod k b a) (Coprod k a b)
forall (k :: * -> * -> *) a b.
(BraidedSCat k, Ok2 k a b) =>
k (Coprod k a b) (Coprod k b a)
swapS
  {-# INLINE swapS #-}

instance UnitCat k => UnitCat (Iso k) where
  lunit :: forall a. Ok (Iso k) a => Iso k a (Prod (Iso k) (Unit (Iso k)) a)
lunit   = k a (Prod k (Unit (Iso k)) a)
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k (Unit (Iso k)) a)
lunit   k a (Prod k (Unit (Iso k)) a)
-> k (Prod k (Unit (Iso k)) a) a
-> Iso k a (Prod k (Unit (Iso k)) a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Prod k (Unit (Iso k)) a) a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k (Unit (Iso k)) a) a
lcounit
  runit :: forall a. Ok (Iso k) a => Iso k a (Prod (Iso k) a (Unit (Iso k)))
runit   = k a (Prod k a (Unit (Iso k)))
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k a (Unit (Iso k)))
runit   k a (Prod k a (Unit (Iso k)))
-> k (Prod k a (Unit (Iso k))) a
-> Iso k a (Prod k a (Unit (Iso k)))
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Prod k a (Unit (Iso k))) a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k a (Unit (Iso k))) a
rcounit
  lcounit :: forall a. Ok (Iso k) a => Iso k (Prod (Iso k) (Unit (Iso k)) a) a
lcounit = k (Prod k (Unit (Iso k)) a) a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k (Unit (Iso k)) a) a
lcounit k (Prod k (Unit (Iso k)) a) a
-> k a (Prod k (Unit (Iso k)) a)
-> Iso k (Prod k (Unit (Iso k)) a) a
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a (Prod k (Unit (Iso k)) a)
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k (Unit (Iso k)) a)
lunit
  rcounit :: forall a. Ok (Iso k) a => Iso k (Prod (Iso k) a (Unit (Iso k))) a
rcounit = k (Prod k a (Unit (Iso k))) a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k a (Unit (Iso k))) a
rcounit k (Prod k a (Unit (Iso k))) a
-> k a (Prod k a (Unit (Iso k)))
-> Iso k (Prod k a (Unit (Iso k))) a
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a (Prod k a (Unit (Iso k)))
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k a (Unit (Iso k)))
runit
  {-# INLINE lunit #-}
  {-# INLINE runit #-}
  {-# INLINE lcounit #-}
  {-# INLINE rcounit #-}

-- instance OkFunctor k h => OkFunctor (Iso k) h where okFunctor = Entail (Sub Dict)

instance OkFunctor k h => OkFunctor (Iso k) h where
  okFunctor :: forall a. Ok' (Iso k) a |- Ok' (Iso k) (h a)
  okFunctor :: forall a. Ok' (Iso k) a |- Ok' (Iso k) (h a)
okFunctor = (Con (Sat (Ok k) a) :- Con (Sat (Ok k) (h a)))
-> Sat (Ok k) a |- Sat (Ok k) (h a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((Ok k a => Dict (Ok k (h a))) -> Ok k a :- Ok k (h a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (Ok k (h a))
Con (Sat (Ok k) (h a)) => Dict (Ok k (h a))
forall (a :: Constraint). a => Dict a
Dict (Con (Sat (Ok k) (h a)) => Dict (Ok k (h a)))
-> (Sat (Ok k) a |- Sat (Ok k) (h a)) -> Dict (Ok k (h a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) (h :: * -> *) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @h @a))
  {-# INLINE okFunctor #-}

instance (FunctorCat k h, ZipCat k h) => FunctorCat (Iso k) h where
  fmapC :: forall a b. Ok2 (Iso k) a b => Iso k a b -> Iso k (h a) (h b)
fmapC (k a b
f :<-> k b a
f') = k a b -> k (h a) (h b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC k a b
f k (h a) (h b) -> k (h b) (h a) -> Iso k (h a) (h b)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k b a -> k (h b) (h a)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC k b a
f'
  unzipC :: forall a b. Ok2 (Iso k) a b => Iso k (h (a :* b)) (h a :* h b)
unzipC = k (h (a :* b)) (h a :* h b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k (h (a :* b)) (h a :* h b)
unzipC k (h (a :* b)) (h a :* h b)
-> k (h a :* h b) (h (a :* b)) -> Iso k (h (a :* b)) (h a :* h b)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (h a :* h b) (h (a :* b))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC
  {-# INLINE fmapC #-}
  {-# INLINE unzipC #-}

instance (FunctorCat k h, ZipCat k h) => ZipCat (Iso k) h where
  zipC :: forall a b. Ok2 (Iso k) a b => Iso k (h a :* h b) (h (a :* b))
zipC = k (h a :* h b) (h (a :* b))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC k (h a :* h b) (h (a :* b))
-> k (h (a :* b)) (h a :* h b) -> Iso k (h a :* h b) (h (a :* b))
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (h (a :* b)) (h a :* h b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k (h (a :* b)) (h a :* h b)
unzipC
  {-# INLINE zipC #-}

-- pure'
-- liftA2'

isoFwd :: Iso k a b -> (a `k` b)
isoFwd :: forall (k :: * -> * -> *) a b. Iso k a b -> k a b
isoFwd (k a b
f :<-> k b a
_) = k a b
f

isoRev :: Iso k a b -> (b `k` a)
isoRev :: forall (k :: * -> * -> *) a b. Iso k a b -> k b a
isoRev (k a b
_ :<-> k b a
f') = k b a
f'

infix 0 <->
type (<->) = Iso (->)

-- | Apply one isomorphism via another
via :: (Category k, Ok2 k a b) => Iso k b b -> Iso k a b -> Iso k a a
(k b b
g :<-> k b b
g') `via` (k a b
ab :<-> k b a
ba) = k b a
ba k b a -> k a b -> k a a
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k b b
g k b b -> k a b -> k a b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a b
ab k a a -> k a a -> Iso k a a
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k b a
ba k b a -> k a b -> k a a
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k b b
g' k b b -> k a b -> k a b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a b
ab
{-# INLINE via #-}

-- Old notation
pattern Iso :: (a `k` b) -> (b `k` a) -> Iso k a b
pattern $mIso :: forall {r} {k :: * -> * -> *} {a} {b}.
Iso k a b -> (k a b -> k b a -> r) -> ((# #) -> r) -> r
$bIso :: forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
Iso f f' = f :<-> f'

newIso :: Newtype a => a <-> O a
newIso :: forall a. Newtype a => a <-> O a
newIso = a -> O a
forall n. Newtype n => n -> O n
unpack (a -> O a) -> (O a -> a) -> Iso (->) a (O a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> O a -> a
forall n. Newtype n => O n -> n
pack
{-# INLINE newIso #-}

hasrepIso :: R.HasRep a => a <-> R.Rep a
hasrepIso :: forall a. HasRep a => a <-> Rep a
hasrepIso = a -> Rep a
forall a. HasRep a => a -> Rep a
R.repr (a -> Rep a) -> (Rep a -> a) -> Iso (->) a (Rep a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> Rep a -> a
forall a. HasRep a => Rep a -> a
R.abst
{-# INLINE hasrepIso #-}

repIso :: Representable f => f a <-> (Rep f -> a)
repIso :: forall (f :: * -> *) a. Representable f => f a <-> (Rep f -> a)
repIso = f a -> Rep f -> a
forall a. f a -> Rep f -> a
forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index (f a -> Rep f -> a)
-> ((Rep f -> a) -> f a) -> Iso (->) (f a) (Rep f -> a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> (Rep f -> a) -> f a
forall a. (Rep f -> a) -> f a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate
{-# INLINE repIso #-}

reindex :: (Representable f, Representable g) => (Rep g <-> Rep f) -> (f <--> g)
reindex :: forall (f :: * -> *) (g :: * -> *).
(Representable f, Representable g) =>
(Rep g <-> Rep f) -> f <--> g
reindex Rep g <-> Rep f
h = Iso (->) (g a) (Rep g :=> a) -> Iso (->) (Rep g :=> a) (g a)
forall (k :: * -> * -> *) a b. Iso k a b -> Iso k b a
inv Iso (->) (g a) (Rep g :=> a)
forall (f :: * -> *) a. Representable f => f a <-> (Rep f -> a)
repIso Iso (->) (Rep g :=> a) (g a)
-> Iso (->) (f a) (Rep g :=> a) -> Iso (->) (f a) (g a)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Rep g <-> Rep f) -> Iso (->) (Rep f :=> a) (Rep g :=> a)
forall (k :: * -> * -> *) c a d.
(Closed k, Ok3 k c a d) =>
k d c -> k (c :=> a) (d :=> a)
dom Rep g <-> Rep f
h Iso (->) (Rep f :=> a) (Rep g :=> a)
-> Iso (->) (f a) (Rep f :=> a) -> Iso (->) (f a) (Rep g :=> a)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Iso (->) (f a) (Rep f :=> a)
forall (f :: * -> *) a. Representable f => f a <-> (Rep f -> a)
repIso
{-# INLINE reindex #-}

#if 0

h  :: Rep g <-> Rep f

repIso     :: f a          <-> (Rep f -> a)
dom h      :: (Rep f -> a) <-> (Rep g -> a)
inv repIso :: (Rep g -> a) <-> g a

#endif

reindexId :: forall f g. (Representable f, Representable g, Rep f ~ Rep g) => (f <--> g)
reindexId :: forall (f :: * -> *) (g :: * -> *).
(Representable f, Representable g, Rep f ~ Rep g) =>
f <--> g
reindexId = -- reindex id
            -- inv repIso . dom id . repIso
            -- inv repIso . id . repIso
            Iso (->) (g a) (Rep g -> a) -> Iso (->) (Rep g -> a) (g a)
forall (k :: * -> * -> *) a b. Iso k a b -> Iso k b a
inv Iso (->) (g a) (Rep g -> a)
forall (f :: * -> *) a. Representable f => f a <-> (Rep f -> a)
repIso Iso (->) (Rep g -> a) (g a)
-> Iso (->) (f a) (Rep g -> a) -> Iso (->) (f a) (g a)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. f a <-> (Rep f -> a)
Iso (->) (f a) (Rep g -> a)
forall (f :: * -> *) a. Representable f => f a <-> (Rep f -> a)
repIso

-- coerceIso :: Coercible a b => a <-> b
-- coerceIso = coerce :<-> coerce

coerceIso :: (CoerceCat k a b, CoerceCat k b a) => Iso k a b
coerceIso :: forall (k :: * -> * -> *) a b.
(CoerceCat k a b, CoerceCat k b a) =>
Iso k a b
coerceIso = k a b
forall (k :: * -> * -> *) a b. CoerceCat k a b => k a b
coerceC k a b -> k b a -> Iso k a b
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k b a
forall (k :: * -> * -> *) a b. CoerceCat k a b => k a b
coerceC

genericIso :: G.Generic a => (a <-> G.Rep a x)
genericIso :: forall a x. Generic a => a <-> Rep a x
genericIso = a -> Rep a x
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
G.from (a -> Rep a x) -> (Rep a x -> a) -> Iso (->) a (Rep a x)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> Rep a x -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
G.to

generic1Iso :: G.Generic1 f => (f <--> G.Rep1 f)
generic1Iso :: forall (f :: * -> *). Generic1 f => f <--> Rep1 f
generic1Iso = f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
G.from1 (f a -> Rep1 f a) -> (Rep1 f a -> f a) -> Iso (->) (f a) (Rep1 f a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> Rep1 f a -> f a
forall a. Rep1 f a -> f a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
G.to1

{--------------------------------------------------------------------
    Experiment
--------------------------------------------------------------------}

infixr 8 ^^^
class (Category k, OkExp k) => Closed k where
  (^^^) :: Ok4 k a b c d => (d `k` c) -> (a `k` b) -> ((c :=> a) `k` (d :=> b))

dom :: (Closed k, Ok3 k c a d) => (d `k` c) -> ((c :=> a) `k` (d :=> a))
dom :: forall (k :: * -> * -> *) c a d.
(Closed k, Ok3 k c a d) =>
k d c -> k (c :=> a) (d :=> a)
dom k d c
f = k d c
f k d c -> k a a -> k (c :=> a) (d :=> a)
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ k a a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id

cod :: (Closed k, Ok3 k c a b) => (a `k` b) -> ((c :=> a) `k` (c :=> b))
cod :: forall (k :: * -> * -> *) c a b.
(Closed k, Ok3 k c a b) =>
k a b -> k (c :=> a) (c :=> b)
cod k a b
g = k c c
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id k c c -> k a b -> k (c :=> a) (c :=> b)
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ k a b
g

foo1, foo2 :: forall k a b c d a' c'.
              (Closed k, Ok k c, Ok k a, Ok k d, Ok k c', Ok k b, Ok k a')
           => (d `k` c') -> (c' `k` c) -> (a `k` a') -> (a' `k` b)
           -> ((c :=> a) `k` (d :=> b))
foo1 :: forall (k :: * -> * -> *) a b c d a' c'.
(Closed k, Ok k c, Ok k a, Ok k d, Ok k c', Ok k b, Ok k a') =>
k d c' -> k c' c -> k a a' -> k a' b -> k (c :=> a) (d :=> b)
foo1 k d c'
f k c' c
g k a a'
h k a' b
k = (k d c'
f k d c' -> k a' b -> k (c' -> a') (d -> b)
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ k a' b
k) k (c' -> a') (d -> b)
-> k (c :=> a) (c' -> a') -> k (c :=> a) (d -> b)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (k c' c
g k c' c -> k a a' -> k (c :=> a) (c' -> a')
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ k a a'
h)
             (Con (Sat (Ok k) (c :=> a)) => k (c :=> a) (d -> b))
-> ((Sat (Ok k) c && Sat (Ok k) a) |- Sat (Ok k) (c :=> a))
-> k (c :=> a) (d -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkExp k =>
(Ok' k a && Ok' k b) |- Ok' k (Exp k a b)
okExp @k @c  @a
             (Con (Sat (Ok k) (c' -> a')) => k (c :=> a) (d -> b))
-> ((Sat (Ok k) c' && Sat (Ok k) a') |- Sat (Ok k) (c' -> a'))
-> k (c :=> a) (d -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkExp k =>
(Ok' k a && Ok' k b) |- Ok' k (Exp k a b)
okExp @k @c' @a'
             (Con (Sat (Ok k) (d -> b)) => k (c :=> a) (d -> b))
-> ((Sat (Ok k) d && Sat (Ok k) b) |- Sat (Ok k) (d -> b))
-> k (c :=> a) (d -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkExp k =>
(Ok' k a && Ok' k b) |- Ok' k (Exp k a b)
okExp @k @d  @b
foo2 :: forall (k :: * -> * -> *) a b c d a' c'.
(Closed k, Ok k c, Ok k a, Ok k d, Ok k c', Ok k b, Ok k a') =>
k d c' -> k c' c -> k a a' -> k a' b -> k (c :=> a) (d :=> b)
foo2 k d c'
f k c' c
g k a a'
h k a' b
k = (k c' c
g k c' c -> k d c' -> k d c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k d c'
f) k d c -> k a b -> k (c :=> a) (d :=> b)
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ (k a' b
k k a' b -> k a a' -> k a b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a a'
h)

-- {-# RULES
-- "(^^^)/(.)" forall f g h k. (f ^^^ k) . (g ^^^ h) = (g . f) ^^^ (k . h)
-- #-}

instance Closed (->) where
  (d -> c
f ^^^ :: forall a b c d.
Ok4 (->) a b c d =>
(d -> c) -> (a -> b) -> (c :=> a) -> (d :=> b)
^^^ a -> b
h) c :=> a
g = a -> b
h (a -> b) -> (d -> a) -> d -> b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. c :=> a
g (c :=> a) -> (d -> c) -> d -> a
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. d -> c
f

instance Closed k => Closed (Iso k) where
  (k d c
f :<-> k c d
f') ^^^ :: forall a b c d.
Ok4 (Iso k) a b c d =>
Iso k d c -> Iso k a b -> Iso k (c :=> a) (d :=> b)
^^^ (k a b
h :<-> k b a
h') = (k d c
f k d c -> k a b -> k (c :=> a) (d :=> b)
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ k a b
h) k (c :=> a) (d :=> b)
-> k (d :=> b) (c :=> a) -> Iso k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> (k c d
f' k c d -> k b a -> k (d :=> b) (c :=> a)
forall a b c d.
Ok4 k a b c d =>
k d c -> k a b -> k (c :=> a) (d :=> b)
forall (k :: * -> * -> *) a b c d.
(Closed k, Ok4 k a b c d) =>
k d c -> k a b -> k (c :=> a) (d :=> b)
^^^ k b a
h')

#if 0

p  :: d `k` c
p' :: c `k` d

q  :: a `k` b
q' :: b `k` a

p  ^^^ q  :: (c :=> a) `k` (d :=> b)
p' ^^^ q' :: (d :=> b) `k` (c :=> a)

#endif

{--------------------------------------------------------------------
    Generic isomorphism-based homomorphisms
--------------------------------------------------------------------}

-- | Natural isomorphism
infix 0 <-->
type f <--> g = forall a. f a <-> g a

fmapIso :: Functor f => (f <--> g) -> (a -> b) -> (g a -> g b)
fmapIso :: forall (f :: * -> *) (g :: * -> *) a b.
Functor f =>
(f <--> g) -> (a -> b) -> g a -> g b
fmapIso f <--> g
fg a -> b
h = Iso (->) (f b) (g b) -> f b -> g b
forall (k :: * -> * -> *) a b. Iso k a b -> k a b
isoFwd Iso (->) (f b) (g b)
f <--> g
fg (f b -> g b) -> (g a -> f b) -> g a -> g b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h (f a -> f b) -> (g a -> f a) -> g a -> f b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Iso (->) (f a) (g a) -> g a -> f a
forall (k :: * -> * -> *) a b. Iso k a b -> k b a
isoRev Iso (->) (f a) (g a)
f <--> g
fg

-- Don't pattern match fg, since we need two type instantiations.
-- For instance, the following doesn't type-check:
-- 
--   fmapIso (fg :<-> gf) h = fg . fmap h . gf

pureIso :: Applicative f => (f <--> g) -> a -> g a
pureIso :: forall (f :: * -> *) (g :: * -> *) a.
Applicative f =>
(f <--> g) -> a -> g a
pureIso f <--> g
fg a
a = Iso (->) (f a) (g a) -> f a -> g a
forall (k :: * -> * -> *) a b. Iso k a b -> k a b
isoFwd Iso (->) (f a) (g a)
f <--> g
fg (a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)

appIso :: Applicative f => (f <--> g) -> g (a -> b) -> g a -> g b
appIso :: forall (f :: * -> *) (g :: * -> *) a b.
Applicative f =>
(f <--> g) -> g (a -> b) -> g a -> g b
appIso f <--> g
fg g (a -> b)
hs g a
xs = Iso (->) (f b) (g b) -> f b -> g b
forall (k :: * -> * -> *) a b. Iso k a b -> k a b
isoFwd Iso (->) (f b) (g b)
f <--> g
fg (Iso (->) (f (a -> b)) (g (a -> b)) -> g (a -> b) -> f (a -> b)
forall (k :: * -> * -> *) a b. Iso k a b -> k b a
isoRev Iso (->) (f (a -> b)) (g (a -> b))
f <--> g
fg g (a -> b)
hs f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Iso (->) (f a) (g a) -> g a -> f a
forall (k :: * -> * -> *) a b. Iso k a b -> k b a
isoRev Iso (->) (f a) (g a)
f <--> g
fg g a
xs)

memptyIso :: Monoid a => (a <-> b) -> b
memptyIso :: forall a b. Monoid a => (a <-> b) -> b
memptyIso (a -> b
ab :<-> b -> a
_) = a -> b
ab a
forall a. Monoid a => a
mempty

mappendIso :: Monoid a => (a <-> b) -> (b -> b -> b)
mappendIso :: forall a b. Monoid a => (a <-> b) -> b -> b -> b
mappendIso (a -> b
ab :<-> b -> a
ba) b
b b
b' = a -> b
ab (b -> a
ba b
b a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` b -> a
ba b
b')

-- mappendIso (ab :<-> ba) (ab a) (ab a') = ab (a `mappend` a')

joinIso :: (MCoproductCat k, Ok3 k a c d) 
        => (c `k` a) :* (d `k` a) <-> ((c :+ d) `k` a)
joinIso :: forall (k :: * -> * -> *) a c d.
(MCoproductCat k, Ok3 k a c d) =>
(k c a :* k d a) <-> k (c :+ d) a
joinIso = (k c a :* k d a) -> k (Coprod k c d) a
forall (k :: * -> * -> *) a c d.
(MCoproductCat k, Ok3 k a c d) =>
(k c a :* k d a) -> k (Coprod k c d) a
join ((k c a :* k d a) -> k (Coprod k c d) a)
-> (k (Coprod k c d) a -> (k c a :* k d a))
-> Iso (->) (k c a :* k d a) (k (Coprod k c d) a)
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k (Coprod k c d) a -> (k c a :* k d a)
forall (k :: * -> * -> *) a c d.
(CoproductCat k, Ok3 k a c d) =>
k (Coprod k c d) a -> k c a :* k d a
unjoin

forkIso :: (MProductCat k, Ok3 k a c d)
        => (a `k` c) :* (a `k` d) <-> (a `k` (c :* d))
forkIso :: forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
(k a c :* k a d) <-> k a (c :* d)
forkIso = (k a c :* k a d) -> k a (Prod k c d)
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
(k a c :* k a d) -> k a (Prod k c d)
fork ((k a c :* k a d) -> k a (Prod k c d))
-> (k a (Prod k c d) -> (k a c :* k a d))
-> Iso (->) (k a c :* k a d) (k a (Prod k c d))
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a (Prod k c d) -> (k a c :* k a d)
forall (k :: * -> * -> *) a c d.
(ProductCat k, Ok3 k a c d) =>
k a (Prod k c d) -> k a c :* k a d
unfork

curryIso :: (ClosedCat k, Ok3 k a b c)
         => ((a :* b) `k` c) <-> (a `k` (b -> c))
curryIso :: forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (a :* b) c <-> k a (b -> c)
curryIso = k (Prod k a b) c -> k a (Exp k b c)
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry (k (Prod k a b) c -> k a (Exp k b c))
-> (k a (Exp k b c) -> k (Prod k a b) c)
-> Iso (->) (k (Prod k a b) c) (k a (Exp k b c))
forall (k :: * -> * -> *) a b. k a b -> k b a -> Iso k a b
:<-> k a (Exp k b c) -> k (Prod k a b) c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry