{-# LANGUAGE Rank2Types, GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Trustworthy #-}
-------------------------------------------------------------------------------------------
-- |
-- Copyright 	: 2008-2016 Edward Kmett
-- License	: BSD
--
-- Maintainer	: Edward Kmett <ekmett@gmail.com>
-- Stability	: experimental
-- Portability	: rank 2 types
--
-- * Right Kan Extensions
-------------------------------------------------------------------------------------------
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

-- | The right Kan extension of a 'Functor' h along a 'Functor' g.
--
-- We can define a right Kan extension in several ways. The definition here is obtained by reading off
-- the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition
-- from the universal property.
--
-- Given a 'Functor' @h : C -> D@ and a 'Functor' @g : C -> C'@, we want to extend @h@ /back/ along @g@
-- to give @Ran g h : C' -> D@, such that the natural transformation @'gran' :: Ran g h (g a) -> h a@ exists.
--
-- In some sense this is trying to approximate the inverse of @g@ by using one of
-- its adjoints, because if the adjoint and the inverse both exist, they match!
--
-- > Hask -h-> Hask
-- >   |       +
-- >   g      /
-- >   |    Ran g h
-- >   v    /
-- > Hask -'
--
-- The Right Kan extension is unique (up to isomorphism) by taking this as its universal property.
--
-- That is to say given any @K : C' -> D@ such that we have a natural transformation from @k.g@ to @h@
-- @(forall x. k (g x) -> h x)@ there exists a canonical natural transformation from @k@ to @Ran g h@.
-- @(forall x. k x -> Ran g h x)@.
--
-- We could literally read this off as a valid Rank-3 definition for 'Ran':
--
-- @
-- data Ran' g h a = forall z. 'Functor' z => Ran' (forall x. z (g x) -> h x) (z a)
-- @
--
-- This definition is isomorphic the simpler Rank-2 definition we use below as witnessed by the
--
-- @
-- ranIso1 :: Ran g f x -> Ran' g f x
-- ranIso1 (Ran e) = Ran' e id
-- @
--
-- @
-- ranIso2 :: Ran' g f x -> Ran g f x
-- ranIso2 (Ran' h z) = Ran $ \\k -> h (k \<$\> z)
-- @
--
-- @
-- ranIso2 (ranIso1 (Ran e)) ≡ -- by definition
-- ranIso2 (Ran' e id) ≡       -- by definition
-- Ran $ \\k -> e (k \<$\> id)    -- by definition
-- Ran $ \\k -> e (k . id)      -- f . id = f
-- Ran $ \\k -> e k             -- eta reduction
-- Ran e
-- @
--
-- The other direction is left as an exercise for the reader.
newtype Ran g h a = Ran { forall {k} (g :: k -> *) (h :: k -> *) a.
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 :: forall a b. (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 -> forall (b :: k). (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 #-}

-- | The universal property of a right Kan extension.
toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b
toRan :: forall {k} (k :: * -> *) (g :: k -> *) (h :: k -> *) b.
Functor k =>
(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 a b. (a -> b) -> k a -> k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap k b
t)
{-# INLINE toRan #-}

-- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@
--
-- @
-- 'toRan' . 'fromRan' ≡ 'id'
-- 'fromRan' . 'toRan' ≡ 'id'
-- @
fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
fromRan :: forall {k} (k :: * -> *) (g :: k -> *) (h :: k -> *) (b :: k).
(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) -> forall (b :: k). (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' . 'decomposeRan' ≡ 'id'
-- 'decomposeRan' . 'composeRan' ≡ 'id'
-- @
composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a
composeRan :: forall (compose :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (h :: * -> *) a.
Composition compose =>
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) -> forall 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 -> forall b. (a -> f b) -> Ran g 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
r (compose f g b -> f (g b)
forall (f :: * -> *) (g :: * -> *) x. compose f g x -> f (g x)
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 :: forall (compose :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (h :: * -> *) a.
(Composition compose, Functor f) =>
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 -> forall b. (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 (f :: * -> *) (g :: * -> *) x. f (g x) -> compose f g x
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 a b. (a -> b) -> f a -> f 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' . 'ranToAdjoint' ≡ 'id'
-- 'ranToAdjoint' . 'adjointToRan' ≡ 'id'
-- @
adjointToRan :: Adjunction f g => f a -> Ran g Identity a
adjointToRan :: forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
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 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 :: forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
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 -> forall b. (a -> g b) -> Identity b
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 a. a -> g (f a)
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit)
{-# INLINE ranToAdjoint #-}

-- |
--
-- @
-- 'composedAdjointToRan' . 'ranToComposedAdjoint' ≡ 'id'
-- 'ranToComposedAdjoint' . 'composedAdjointToRan' ≡ 'id'
-- @
ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)
ranToComposedAdjoint :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
Adjunction f g =>
Ran g h a -> h (f a)
ranToComposedAdjoint Ran g h a
r = Ran g h a -> forall b. (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
r a -> g (f a)
forall a. 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 :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
(Adjunction f g, Functor h) =>
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 a b. (a -> b) -> h a -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> g b) -> f a -> b
forall 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) h (f a)
f)
{-# INLINE composedAdjointToRan #-}

-- | This is the natural transformation that defines a Right Kan extension.
gran :: Ran g h (g a) -> h a
gran :: forall {k} (g :: k -> *) (h :: k -> *) (a :: k).
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 :: forall (u :: * -> *) a.
Representable u =>
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 a. u a -> Rep u -> a
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 :: forall (u :: * -> *) a.
Representable u =>
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 a. (Rep u -> a) -> 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 :: forall (u :: * -> *) (h :: * -> *) a.
Representable u =>
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 a. (Rep u -> a) -> 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 :: forall (u :: * -> *) (h :: * -> *) a.
(Representable u, Functor h) =>
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 a b. (a -> b) -> h 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 a. u a -> Rep u -> a
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 #-}