{-# LANGUAGE Rank2Types, GADTs #-}
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
module Data.Functor.Kan.Ran
(
Ran(..)
, toRan, fromRan
, gran
, composeRan, decomposeRan
, adjointToRan, ranToAdjoint
, composedAdjointToRan, ranToComposedAdjoint
, repToRan, ranToRep
, composedRepToRan, ranToComposedRep
) where
import Data.Functor.Adjunction
import Data.Functor.Composition
import Data.Functor.Identity
import Data.Functor.Rep
newtype Ran g h a = Ran { Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan :: forall b. (a -> g b) -> h b }
instance Functor (Ran g h) where
fmap :: (a -> b) -> Ran g h a -> Ran g h b
fmap a -> b
f Ran g h a
m = (forall (b :: k). (b -> g b) -> h b) -> Ran g h b
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (\b -> g b
k -> Ran g h a -> (a -> g b) -> h b
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan Ran g h a
m (b -> g b
k (b -> g b) -> (a -> b) -> a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f))
{-# INLINE fmap #-}
toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b
toRan :: (forall (a :: k). k (g a) -> h a) -> k b -> Ran g h b
toRan forall (a :: k). k (g a) -> h a
s k b
t = (forall (b :: k). (b -> g b) -> h b) -> Ran g h b
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (k (g b) -> h b
forall (a :: k). k (g a) -> h a
s (k (g b) -> h b) -> ((b -> g b) -> k (g b)) -> (b -> g b) -> h b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> g b) -> k b -> k (g b)) -> k b -> (b -> g b) -> k (g b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (b -> g b) -> k b -> k (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap k b
t)
{-# INLINE toRan #-}
fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
fromRan forall a. k a -> Ran g h a
s k (g b)
kgb = Ran g h (g b) -> (g b -> g b) -> h b
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan (k (g b) -> Ran g h (g b)
forall a. k a -> Ran g h a
s k (g b)
kgb) g b -> g b
forall a. a -> a
id
{-# INLINE fromRan #-}
composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a
composeRan :: Ran f (Ran g h) a -> Ran (compose f g) h a
composeRan Ran f (Ran g h) a
r = (forall b. (a -> compose f g b) -> h b) -> Ran (compose f g) h a
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (\a -> compose f g b
f -> Ran g h (g b) -> (g b -> g b) -> h b
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan (Ran f (Ran g h) a -> (a -> f (g b)) -> Ran g h (g b)
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan Ran f (Ran g h) a
r (compose f g b -> f (g b)
forall (o :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) x.
Composition o =>
o f g x -> f (g x)
decompose (compose f g b -> f (g b)) -> (a -> compose f g b) -> a -> f (g b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> compose f g b
f)) g b -> g b
forall a. a -> a
id)
{-# INLINE composeRan #-}
decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a
decomposeRan :: Ran (compose f g) h a -> Ran f (Ran g h) a
decomposeRan Ran (compose f g) h a
r = (forall b. (a -> f b) -> Ran g h b) -> Ran f (Ran g h) a
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (\a -> f b
f -> (forall b. (b -> g b) -> h b) -> Ran g h b
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (\b -> g b
g -> Ran (compose f g) h a -> (a -> compose f g b) -> h b
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan Ran (compose f g) h a
r (f (g b) -> compose f g b
forall (o :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) x.
Composition o =>
f (g x) -> o f g x
compose (f (g b) -> compose f g b) -> (a -> f (g b)) -> a -> compose f g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> g b) -> f b -> f (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> g b
g (f b -> f (g b)) -> (a -> f b) -> a -> f (g b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f)))
{-# INLINE decomposeRan #-}
adjointToRan :: Adjunction f g => f a -> Ran g Identity a
adjointToRan :: f a -> Ran g Identity a
adjointToRan f a
f = (forall b. (a -> g b) -> Identity b) -> Ran g Identity a
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (\a -> g b
a -> b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> b -> Identity b
forall a b. (a -> b) -> a -> b
$ (a -> g b) -> f a -> b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct a -> g b
a f a
f)
{-# INLINE adjointToRan #-}
ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a
ranToAdjoint :: Ran g Identity a -> f a
ranToAdjoint Ran g Identity a
r = Identity (f a) -> f a
forall a. Identity a -> a
runIdentity (Ran g Identity a -> (a -> g (f a)) -> Identity (f a)
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan Ran g Identity a
r a -> g (f a)
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit)
{-# INLINE ranToAdjoint #-}
ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)
ranToComposedAdjoint :: Ran g h a -> h (f a)
ranToComposedAdjoint Ran g h a
r = Ran g h a -> (a -> g (f a)) -> h (f a)
forall k (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan Ran g h a
r a -> g (f a)
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit
{-# INLINE ranToComposedAdjoint #-}
composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a
composedAdjointToRan :: h (f a) -> Ran g h a
composedAdjointToRan h (f a)
f = (forall b. (a -> g b) -> h b) -> Ran g h a
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran (\a -> g b
a -> (f a -> b) -> h (f a) -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> g b) -> f a -> b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct a -> g b
a) h (f a)
f)
{-# INLINE composedAdjointToRan #-}
gran :: Ran g h (g a) -> h a
gran :: Ran g h (g a) -> h a
gran (Ran forall (b :: k). (g a -> g b) -> h b
f) = (g a -> g a) -> h a
forall (b :: k). (g a -> g b) -> h b
f g a -> g a
forall a. a -> a
id
{-# INLINE gran #-}
repToRan :: Representable u => Rep u -> a -> Ran u Identity a
repToRan :: Rep u -> a -> Ran u Identity a
repToRan Rep u
e a
a = (forall b. (a -> u b) -> Identity b) -> Ran u Identity a
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran ((forall b. (a -> u b) -> Identity b) -> Ran u Identity a)
-> (forall b. (a -> u b) -> Identity b) -> Ran u Identity a
forall a b. (a -> b) -> a -> b
$ \a -> u b
k -> b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> b -> Identity b
forall a b. (a -> b) -> a -> b
$ u b -> Rep u -> b
forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index (a -> u b
k a
a) Rep u
e
{-# INLINE repToRan #-}
ranToRep :: Representable u => Ran u Identity a -> (Rep u, a)
ranToRep :: Ran u Identity a -> (Rep u, a)
ranToRep (Ran forall b. (a -> u b) -> Identity b
f) = Identity (Rep u, a) -> (Rep u, a)
forall a. Identity a -> a
runIdentity (Identity (Rep u, a) -> (Rep u, a))
-> Identity (Rep u, a) -> (Rep u, a)
forall a b. (a -> b) -> a -> b
$ (a -> u (Rep u, a)) -> Identity (Rep u, a)
forall b. (a -> u b) -> Identity b
f (\a
a -> (Rep u -> (Rep u, a)) -> u (Rep u, a)
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate ((Rep u -> (Rep u, a)) -> u (Rep u, a))
-> (Rep u -> (Rep u, a)) -> u (Rep u, a)
forall a b. (a -> b) -> a -> b
$ \Rep u
e -> (Rep u
e, a
a))
{-# INLINE ranToRep #-}
ranToComposedRep :: Representable u => Ran u h a -> h (Rep u, a)
ranToComposedRep :: Ran u h a -> h (Rep u, a)
ranToComposedRep (Ran forall b. (a -> u b) -> h b
f) = (a -> u (Rep u, a)) -> h (Rep u, a)
forall b. (a -> u b) -> h b
f (\a
a -> (Rep u -> (Rep u, a)) -> u (Rep u, a)
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate ((Rep u -> (Rep u, a)) -> u (Rep u, a))
-> (Rep u -> (Rep u, a)) -> u (Rep u, a)
forall a b. (a -> b) -> a -> b
$ \Rep u
e -> (Rep u
e, a
a))
{-# INLINE ranToComposedRep #-}
composedRepToRan :: (Representable u, Functor h) => h (Rep u, a) -> Ran u h a
composedRepToRan :: h (Rep u, a) -> Ran u h a
composedRepToRan h (Rep u, a)
hfa = (forall b. (a -> u b) -> h b) -> Ran u h a
forall k (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran ((forall b. (a -> u b) -> h b) -> Ran u h a)
-> (forall b. (a -> u b) -> h b) -> Ran u h a
forall a b. (a -> b) -> a -> b
$ \a -> u b
k -> ((Rep u, a) -> b) -> h (Rep u, a) -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Rep u
e, a
a) -> u b -> Rep u -> b
forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index (a -> u b
k a
a) Rep u
e) h (Rep u, a)
hfa
{-# INLINE composedRepToRan #-}