{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE Trustworthy #-}
#endif
-------------------------------------------------------------------------------------------
-- |
-- Copyright 	: 2008-2016 Edward Kmett
-- License	: BSD
--
-- Maintainer	: Edward Kmett <[email protected]>
-- 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

import Control.Applicative
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) = forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan (a -> b
f 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 =
    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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst g (b, b)
k) (g b -> a
kya (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd g (b, b)
k))) ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h b
x 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 = forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan (forall a b. a -> b -> a
const a
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 =
    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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst g (b, b)
k) (g b -> a
kya (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd g (b, b)
k))) (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) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g b -> b
f (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 = forall a. Lan g h a -> f a
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f (u a) -> a
counit forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f b -> a
f (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) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan 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)) = forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan (f b -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g b -> b
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (o :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) x.
Composition o =>
f (g x) -> o f g x
compose) (forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan 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 = forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan forall a. a -> a
id
{-# INLINE glan #-}