    {-# 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 #-}