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