    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE PolyKinds #-}
    -------------------------------------------------------------------------------------------
    -- |
    -- Copyright 	: 2008-2016 Edward Kmett
    -- License	: BSD
    --
    -- Maintainer	: Edward Kmett <ekmett@gmail.com>
    -- Stability	: experimental
    -- Portability	: rank 2 types
    --
    -- Left Kan Extensions
    -------------------------------------------------------------------------------------------
    module Data.Functor.Kan.Lan
      (
      -- * Left Kan Extensions
        Lan(..)
      , toLan, fromLan
      , glan
      , composeLan, decomposeLan
      , adjointToLan, lanToAdjoint
      , composedAdjointToLan, lanToComposedAdjoint
      ) where

    #if !(MIN_VERSION_base(4,18,0))
    import Control.Applicative
    #endif
    import Data.Functor.Adjunction
    import Data.Functor.Apply
    import Data.Functor.Composition
    import Data.Functor.Identity

    -- | The left Kan extension of a 'Functor' @h@ along a 'Functor' @g@.
    data Lan g h a where
      Lan :: (g b -> a) -> h b -> Lan g h a

    instance Functor (Lan f g) where
      fmap :: forall a b. (a -> b) -> Lan f g a -> Lan f g b
    fmap a -> b
    f (Lan f b -> a
    g g b
    h) = (f b -> b) -> g b -> Lan f g b
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan (a -> b
    f (a -> b) -> (f b -> a) -> f b -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f b -> a
    g) g b
    h
      {-# INLINE fmap #-}

    instance (Functor g, Apply h) => Apply (Lan g h) where
      Lan g b -> a -> b
    kxf h b
    x <.> :: forall a b. Lan g h (a -> b) -> Lan g h a -> Lan g h b
    <.> Lan g b -> a
    kya h b
    y =
        (g (b, b) -> b) -> h (b, b) -> Lan g h b
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan (\g (b, b)
    k -> g b -> a -> b
    kxf (((b, b) -> b) -> g (b, b) -> g b
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b, b) -> b
    forall a b. (a, b) -> a
    fst g (b, b)
    k) (g b -> a
    kya (((b, b) -> b) -> g (b, b) -> g b
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b, b) -> b
    forall a b. (a, b) -> b
    snd g (b, b)
    k))) ((,) (b -> b -> (b, b)) -> h b -> h (b -> (b, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> h b
    x h (b -> (b, b)) -> h b -> h (b, b)
    forall a b. h (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
    <.> h b
    y)
      {-# INLINE (<.>) #-}

    instance (Functor g, Applicative h) => Applicative (Lan g h) where
      pure :: forall a. a -> Lan g h a
    pure a
    a = (g () -> a) -> h () -> Lan g h a
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan (a -> g () -> a
    forall a b. a -> b -> a
    const a
    a) (() -> h ()
    forall a. a -> h a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ())
      {-# INLINE pure #-}
      Lan g b -> a -> b
    kxf h b
    x <*> :: forall a b. Lan g h (a -> b) -> Lan g h a -> Lan g h b
    <*> Lan g b -> a
    kya h b
    y =
        (g (b, b) -> b) -> h (b, b) -> Lan g h b
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan (\g (b, b)
    k -> g b -> a -> b
    kxf (((b, b) -> b) -> g (b, b) -> g b
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b, b) -> b
    forall a b. (a, b) -> a
    fst g (b, b)
    k) (g b -> a
    kya (((b, b) -> b) -> g (b, b) -> g b
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b, b) -> b
    forall a b. (a, b) -> b
    snd g (b, b)
    k))) ((b -> b -> (b, b)) -> h b -> h b -> h (b, b)
    forall a b c. (a -> b -> c) -> h a -> h b -> h c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (,) h b
    x h b
    y)
      {-# INLINE (<*>) #-}

    -- | The universal property of a left Kan extension.
    toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b
    toLan :: forall {k} (f :: * -> *) (h :: k -> *) (g :: k -> *) b.
    Functor f =>
    (forall (a :: k). h a -> f (g a)) -> Lan g h b -> f b
    toLan forall (a :: k). h a -> f (g a)
    s (Lan g b -> b
    f h b
    v) = (g b -> b) -> f (g b) -> f b
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap g b -> b
    f (h b -> f (g b)
    forall (a :: k). h a -> f (g a)
    s h b
    v)
    {-# INLINE toLan #-}

    -- | 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@
    --
    -- @
    -- 'toLan' . 'fromLan' ≡ 'id'
    -- 'fromLan' . 'toLan' ≡ 'id'
    -- @
    fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)
    fromLan :: forall {k} (g :: k -> *) (h :: k -> *) (f :: * -> *) (b :: k).
    (forall a. Lan g h a -> f a) -> h b -> f (g b)
    fromLan forall a. Lan g h a -> f a
    s = Lan g h (g b) -> f (g b)
    forall a. Lan g h a -> f a
    s (Lan g h (g b) -> f (g b))
    -> (h b -> Lan g h (g b)) -> h b -> f (g b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . h b -> Lan g h (g b)
    forall {k} (h :: k -> *) (a :: k) (g :: k -> *).
    h a -> Lan g h (g a)
    glan
    {-# INLINE fromLan #-}

    -- |
    --
    -- @
    -- 'adjointToLan' . 'lanToAdjoint' ≡ 'id'
    -- 'lanToAdjoint' . 'adjointToLan' ≡ 'id'
    -- @
    adjointToLan :: Adjunction f g => g a -> Lan f Identity a
    adjointToLan :: forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    g a -> Lan f Identity a
    adjointToLan = (f (g a) -> a) -> Identity (g a) -> Lan f Identity a
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan f (g a) -> a
    forall a. f (g a) -> a
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f (u a) -> a
    counit (Identity (g a) -> Lan f Identity a)
    -> (g a -> Identity (g a)) -> g a -> Lan f Identity a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g a -> Identity (g a)
    forall a. a -> Identity a
    Identity
    {-# INLINE adjointToLan #-}

    lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a
    lanToAdjoint :: forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    Lan f Identity a -> g a
    lanToAdjoint (Lan f b -> a
    f Identity b
    v) = (f b -> a) -> b -> g a
    forall a b. (f a -> b) -> a -> g b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct f b -> a
    f (Identity b -> b
    forall a. Identity a -> a
    runIdentity Identity b
    v)
    {-# INLINE lanToAdjoint #-}

    -- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@
    --
    -- @
    -- 'composedAdjointToLan' . 'lanToComposedAdjoint' ≡ 'id'
    -- 'lanToComposedAdjoint' . 'composedAdjointToLan' ≡ 'id'
    -- @
    lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)
    lanToComposedAdjoint :: forall (h :: * -> *) (f :: * -> *) (g :: * -> *) a.
    (Functor h, Adjunction f g) =>
    Lan f h a -> h (g a)
    lanToComposedAdjoint (Lan f b -> a
    f h b
    v) = (b -> g a) -> h b -> h (g a)
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((f b -> a) -> b -> g a
    forall a b. (f a -> b) -> a -> g b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct f b -> a
    f) h b
    v
    {-# INLINE lanToComposedAdjoint #-}

    composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a
    composedAdjointToLan :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    Adjunction f g =>
    h (g a) -> Lan f h a
    composedAdjointToLan = (f (g a) -> a) -> h (g a) -> Lan f h a
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan f (g a) -> a
    forall a. f (g a) -> a
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f (u a) -> a
    counit
    {-# INLINE composedAdjointToLan #-}

    -- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@
    --
    -- @
    -- 'composeLan' . 'decomposeLan' ≡ 'id'
    -- 'decomposeLan' . 'composeLan' ≡ 'id'
    -- @
    composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a
    composeLan :: forall (compose :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
           (g :: * -> *) (h :: * -> *) a.
    (Composition compose, Functor f) =>
    Lan f (Lan g h) a -> Lan (compose f g) h a
    composeLan (Lan f b -> a
    f (Lan g b -> b
    g h b
    h)) = (compose f g b -> a) -> h b -> Lan (compose f g) h a
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan (f b -> a
    f (f b -> a) -> (compose f g b -> f b) -> compose f g b -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (g b -> b) -> f (g b) -> f b
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap g b -> b
    g (f (g b) -> f b)
    -> (compose f g b -> f (g b)) -> compose f g b -> f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . 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) h b
    h
    {-# INLINE composeLan #-}

    decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a
    decomposeLan :: forall (compose :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
           (g :: * -> *) (h :: * -> *) a.
    Composition compose =>
    Lan (compose f g) h a -> Lan f (Lan g h) a
    decomposeLan (Lan compose f g b -> a
    f h b
    h) = (f (g b) -> a) -> Lan g h (g b) -> Lan f (Lan g h) a
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan (compose f g b -> a
    f (compose f g b -> a) -> (f (g b) -> compose f g b) -> f (g b) -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . 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) ((g b -> g b) -> h b -> Lan g h (g b)
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan g b -> g b
    forall a. a -> a
    id h b
    h)
    {-# INLINE decomposeLan #-}

    -- | This is the natural transformation that defines a Left Kan extension.
    glan :: h a -> Lan g h (g a)
    glan :: forall {k} (h :: k -> *) (a :: k) (g :: k -> *).
    h a -> Lan g h (g a)
    glan = (g a -> g a) -> h a -> Lan g h (g a)
    forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
    (g b -> a) -> h b -> Lan g h a
    Lan g a -> g a
    forall a. a -> a
    id
    {-# INLINE glan #-}