    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Control.Comonad.Density
    -- Copyright   :  (C) 2008-2016 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable (GADTs, MPTCs)
    --
    -- The 'Density' 'Comonad' for a 'Functor' (aka the 'Comonad generated by a 'Functor')
    -- The 'Density' term dates back to Dubuc''s 1974 thesis. The term
    -- 'Monad' generated by a 'Functor' dates back to 1972 in Street''s
    -- ''Formal Theory of Monads''.
    --
    -- The left Kan extension of a 'Functor' along itself (@'Lan' f f@) forms a 'Comonad'. This is
    -- that 'Comonad'.
    ----------------------------------------------------------------------------
    module Control.Comonad.Density
      ( Density(..)
      , liftDensity
      , densityToAdjunction, adjunctionToDensity
      , densityToLan, lanToDensity
      ) where

    #if !(MIN_VERSION_base(4,18,0))
    import Control.Applicative
    #endif
    import Control.Comonad
    import Control.Comonad.Trans.Class
    import Data.Functor.Apply
    import Data.Functor.Adjunction
    import Data.Functor.Extend
    import Data.Functor.Kan.Lan

    data Density k a where
      Density :: (k b -> a) -> k b -> Density k a

    instance Functor (Density f) where
      fmap :: forall a b. (a -> b) -> Density f a -> Density f b
    fmap a -> b
    f (Density f b -> a
    g f b
    h) = (f b -> b) -> f b -> Density f b
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density (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) f b
    h
      {-# INLINE fmap #-}

    instance Extend (Density f) where
      duplicated :: forall a. Density f a -> Density f (Density f a)
    duplicated (Density f b -> a
    f f b
    ws) = (f b -> Density f a) -> f b -> Density f (Density f a)
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density ((f b -> a) -> f b -> Density f a
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density f b -> a
    f) f b
    ws
      {-# INLINE duplicated #-}

    instance Comonad (Density f) where
      duplicate :: forall a. Density f a -> Density f (Density f a)
    duplicate (Density f b -> a
    f f b
    ws) = (f b -> Density f a) -> f b -> Density f (Density f a)
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density ((f b -> a) -> f b -> Density f a
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density f b -> a
    f) f b
    ws
      {-# INLINE duplicate #-}
      extract :: forall a. Density f a -> a
    extract (Density f b -> a
    f f b
    a) = f b -> a
    f f b
    a
      {-# INLINE extract #-}

    instance ComonadTrans Density where
      lower :: forall (w :: * -> *) a. Comonad w => Density w a -> w a
    lower (Density w b -> a
    f w b
    c) = (w b -> a) -> w b -> w a
    forall a b. (w a -> b) -> w a -> w b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend w b -> a
    f w b
    c
      {-# INLINE lower #-}

    instance Apply f => Apply (Density f) where
      Density f b -> a -> b
    kxf f b
    x <.> :: forall a b. Density f (a -> b) -> Density f a -> Density f b
    <.> Density f b -> a
    kya f b
    y =
        (f (b, b) -> b) -> f (b, b) -> Density f b
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density (\f (b, b)
    k -> f b -> a -> b
    kxf (((b, b) -> b) -> f (b, 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 (b, b) -> b
    forall a b. (a, b) -> a
    fst f (b, b)
    k) (f b -> a
    kya (((b, b) -> b) -> f (b, 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 (b, b) -> b
    forall a b. (a, b) -> b
    snd f (b, b)
    k))) ((,) (b -> b -> (b, b)) -> f b -> f (b -> (b, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f b
    x f (b -> (b, b)) -> f b -> f (b, b)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
    <.> f b
    y)
      {-# INLINE (<.>) #-}

    instance Applicative f => Applicative (Density f) where
      pure :: forall a. a -> Density f a
    pure a
    a = (f () -> a) -> f () -> Density f a
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density (a -> f () -> a
    forall a b. a -> b -> a
    const a
    a) (() -> f ()
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ())
      {-# INLINE pure #-}
      Density f b -> a -> b
    kxf f b
    x <*> :: forall a b. Density f (a -> b) -> Density f a -> Density f b
    <*> Density f b -> a
    kya f b
    y =
        (f (b, b) -> b) -> f (b, b) -> Density f b
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density (\f (b, b)
    k -> f b -> a -> b
    kxf (((b, b) -> b) -> f (b, 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 (b, b) -> b
    forall a b. (a, b) -> a
    fst f (b, b)
    k) (f b -> a
    kya (((b, b) -> b) -> f (b, 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 (b, b) -> b
    forall a b. (a, b) -> b
    snd f (b, b)
    k))) ((b -> b -> (b, b)) -> f b -> f b -> f (b, b)
    forall a b c. (a -> b -> c) -> f a -> f b -> f c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (,) f b
    x f b
    y)
      {-# INLINE (<*>) #-}

    -- | The natural transformation from a @'Comonad' w@ to the 'Comonad' generated by @w@ (forwards).
    --
    -- This is merely a right-inverse (section) of 'lower', rather than a full inverse.
    --
    -- @
    -- 'lower' . 'liftDensity' ≡ 'id'
    -- @
    liftDensity :: Comonad w => w a -> Density w a
    liftDensity :: forall (w :: * -> *) a. Comonad w => w a -> Density w a
    liftDensity = (w a -> a) -> w a -> Density w a
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density w a -> a
    forall a. w a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract
    {-# INLINE liftDensity #-}

    -- | The Density 'Comonad' of a left adjoint is isomorphic to the 'Comonad' formed by that 'Adjunction'.
    --
    -- This isomorphism is witnessed by 'densityToAdjunction' and 'adjunctionToDensity'.
    --
    -- @
    -- 'densityToAdjunction' . 'adjunctionToDensity' ≡ 'id'
    -- 'adjunctionToDensity' . 'densityToAdjunction' ≡ 'id'
    -- @
    densityToAdjunction :: Adjunction f g => Density f a -> f (g a)
    densityToAdjunction :: forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    Density f a -> f (g a)
    densityToAdjunction (Density f b -> a
    f f b
    v) = (b -> g a) -> f b -> f (g a)
    forall a b. (a -> b) -> f a -> f 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) f b
    v
    {-# INLINE densityToAdjunction #-}

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

    -- | The 'Density' 'Comonad' of a 'Functor' @f@ is obtained by taking the left Kan extension
    -- ('Lan') of @f@ along itself. This isomorphism is witnessed by 'lanToDensity' and 'densityToLan'
    --
    -- @
    -- 'lanToDensity' . 'densityToLan' ≡ 'id'
    -- 'densityToLan' . 'lanToDensity' ≡ 'id'
    -- @
    lanToDensity :: Lan f f a -> Density f a
    lanToDensity :: forall {k} (f :: k -> *) a. Lan f f a -> Density f a
    lanToDensity (Lan f b -> a
    f f b
    v) = (f b -> a) -> f b -> Density f a
    forall {k} (k :: k -> *) (b :: k) a.
    (k b -> a) -> k b -> Density k a
    Density f b -> a
    f f b
    v
    {-# INLINE lanToDensity #-}

    densityToLan :: Density f a -> Lan f f a
    densityToLan :: forall {k} (f :: k -> *) a. Density f a -> Lan f f a
    densityToLan (Density f b -> a
    f f b
    v) = (f b -> a) -> f b -> Lan f f 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
    v
    {-# INLINE densityToLan #-}