{-# LANGUAGE CPP #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE Trustworthy #-}
#endif
-------------------------------------------------------------------------------------------
-- |
-- Copyright 	: 2013-2016 Edward Kmett and Dan Doel
-- License	: BSD
--
-- Maintainer	: Edward Kmett <[email protected]>
-- Stability	: experimental
-- Portability	: rank N types
--
-- @'Day' f -| 'Curried' f@
--
-- @'Day' f ~ 'Compose' f@ when f preserves colimits / is a left adjoint. (Due in part to the
-- strength of all functors in Hask.)
--
-- So by the uniqueness of adjoints, when f is a left adjoint, @'Curried' f ~ 'Rift' f@
-------------------------------------------------------------------------------------------
module Data.Functor.Day.Curried
  (
  -- * Right Kan lifts
    Curried(..)
  , toCurried, fromCurried, applied, unapplied
  , adjointToCurried, curriedToAdjoint
  , composedAdjointToCurried, curriedToComposedAdjoint
  , liftCurried, lowerCurried, rap
  ) where

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Data.Functor.Adjunction
import Data.Functor.Day
import Data.Functor.Identity

newtype Curried g h a =
  Curried { forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a -> r) -> h r
runCurried :: forall r. g (a -> r) -> h r }

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

instance (Functor g, g ~ h) => Applicative (Curried g h) where
  pure :: forall a. a -> Curried g h a
pure a
a = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> a -> b
$ a
a))
  {-# INLINE pure #-}
  Curried forall r. g ((a -> b) -> r) -> h r
mf <*> :: forall a b. Curried g h (a -> b) -> Curried g h a -> Curried g h b
<*> Curried forall r. g (a -> r) -> h r
ma = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (forall r. g (a -> r) -> h r
ma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. g ((a -> b) -> r) -> h r
mf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
(.))
  {-# INLINE (<*>) #-}

-- | The natural isomorphism between @f@ and @Curried f f@.
-- @
-- 'lowerCurried' '.' 'liftCurried' ≡ 'id'
-- 'liftCurried' '.' 'lowerCurried' ≡ 'id'
-- @
--
-- @
-- 'lowerCurried' ('liftCurried' x)     -- definition
-- 'lowerCurried' ('Curried' ('<*>' x))   -- definition
-- ('<*>' x) ('pure' 'id')          -- beta reduction
-- 'pure' 'id' '<*>' x              -- Applicative identity law
-- x
-- @
liftCurried :: Applicative f => f a -> Curried f f a
liftCurried :: forall (f :: * -> *) a. Applicative f => f a -> Curried f f a
liftCurried f a
fa = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
fa)
{-# INLINE liftCurried #-}

-- | Lower 'Curried' by applying 'pure' 'id' to the continuation.
--
-- See 'liftCurried'.
lowerCurried :: Applicative f => Curried f g a -> g a
lowerCurried :: forall (f :: * -> *) (g :: * -> *) a.
Applicative f =>
Curried f g a -> g a
lowerCurried (Curried forall r. f (a -> r) -> g r
f) = forall r. f (a -> r) -> g r
f (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id)
{-# INLINE lowerCurried #-}

-- | Indexed applicative composition of right Kan lifts.
rap :: Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b
rap :: forall (f :: * -> *) (g :: * -> *) a b (h :: * -> *).
Functor f =>
Curried f g (a -> b) -> Curried g h a -> Curried f h b
rap (Curried forall r. f ((a -> b) -> r) -> g r
mf) (Curried forall r. g (a -> r) -> h r
ma) = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (forall r. g (a -> r) -> h r
ma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. f ((a -> b) -> r) -> g r
mf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
(.))
{-# INLINE rap #-}

-- | This is the counit of the @Day f -| Curried f@ adjunction
applied :: Functor f => Day f (Curried f g) a -> g a
applied :: forall (f :: * -> *) (g :: * -> *) a.
Functor f =>
Day f (Curried f g) a -> g a
applied (Day f b
fb (Curried forall r. f (c -> r) -> g r
fg) b -> c -> a
bca) = forall r. f (c -> r) -> g r
fg (b -> c -> a
bca forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
fb)
{-# INLINE applied #-}

-- | This is the unit of the @Day f -| Curried f@ adjunction
unapplied :: g a -> Curried f (Day f g) a
unapplied :: forall (g :: * -> *) a (f :: * -> *). g a -> Curried f (Day f g) a
unapplied g a
ga = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried forall a b. (a -> b) -> a -> b
$ \ f (a -> r)
fab -> forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day f (a -> r)
fab g a
ga forall a. a -> a
id
{-# INLINE unapplied #-}

-- | The universal property of 'Curried'
toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a
toCurried :: forall (g :: * -> *) (k :: * -> *) (h :: * -> *) a.
(forall x. Day g k x -> h x) -> k a -> Curried g h a
toCurried forall x. Day g k x -> h x
h k a
ka = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried forall a b. (a -> b) -> a -> b
$ \g (a -> r)
gar -> forall x. Day g k x -> h x
h (forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g (a -> r)
gar k a
ka forall a. a -> a
id)
{-# INLINE toCurried #-}

-- |
-- @
-- 'toCurried' . 'fromCurried' ≡ 'id'
-- 'fromCurried' . 'toCurried' ≡ 'id'
-- @
fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b
fromCurried :: forall (f :: * -> *) (k :: * -> *) (h :: * -> *) b.
Functor f =>
(forall a. k a -> Curried f h a) -> Day f k b -> h b
fromCurried forall a. k a -> Curried f h a
f (Day f b
fc k c
kd b -> c -> b
cdb) = forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a -> r) -> h r
runCurried (forall a. k a -> Curried f h a
f k c
kd) (b -> c -> b
cdb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
fc)
{-# INLINE fromCurried #-}

-- | @Curried f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
--
-- @
-- 'adjointToCurried' . 'curriedToAdjoint' ≡ 'id'
-- 'curriedToAdjoint' . 'adjointToCurried' ≡ 'id'
-- @
adjointToCurried :: Adjunction f u => u a -> Curried f Identity a
adjointToCurried :: forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
u a -> Curried f Identity a
adjointToCurried u a
ua = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> u a
ua))
{-# INLINE adjointToCurried #-}

-- | @Curried f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
curriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a
curriedToAdjoint :: forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
Curried f Identity a -> u a
curriedToAdjoint (Curried forall r. f (a -> r) -> Identity r
m) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. f (a -> r) -> Identity r
m) forall a. a -> a
id
{-# INLINE curriedToAdjoint #-}

-- | @Curried f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
--
-- @
-- 'curriedToComposedAdjoint' . 'composedAdjointToCurried' ≡ 'id'
-- 'composedAdjointToCurried' . 'curriedToComposedAdjoint' ≡ 'id'
-- @

curriedToComposedAdjoint :: Adjunction f u => Curried f h a -> u (h a)
curriedToComposedAdjoint :: forall (f :: * -> *) (u :: * -> *) (h :: * -> *) a.
Adjunction f u =>
Curried f h a -> u (h a)
curriedToComposedAdjoint (Curried forall r. f (a -> r) -> h r
m) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall r. f (a -> r) -> h r
m forall a. a -> a
id
{-# INLINE curriedToComposedAdjoint #-}

-- | @Curried f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
composedAdjointToCurried :: (Functor h, Adjunction f u) => u (h a) -> Curried f h a
composedAdjointToCurried :: forall (h :: * -> *) (f :: * -> *) (u :: * -> *) a.
(Functor h, Adjunction f u) =>
u (h a) -> Curried f h a
composedAdjointToCurried u (h a)
uha = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\a -> r
b -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> r
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> u (h a)
uha)
{-# INLINE composedAdjointToCurried #-}