{-# 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 <ekmett@gmail.com>
-- 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 { 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 :: (a -> b) -> Curried g h a -> Curried g h b
fmap a -> b
f (Curried forall r. g (a -> r) -> h r
g) = (forall r. g (b -> r) -> h r) -> Curried g h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (g (a -> r) -> h r
forall r. g (a -> r) -> h r
g (g (a -> r) -> h r)
-> (g (b -> r) -> g (a -> r)) -> g (b -> r) -> h r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> r) -> a -> r) -> g (b -> r) -> g (a -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> r) -> (a -> b) -> a -> r
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 :: a -> Curried g h a
pure a
a = (forall r. g (a -> r) -> h r) -> Curried g h a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (((a -> r) -> r) -> h (a -> r) -> h r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> r) -> a -> r
forall a b. (a -> b) -> a -> b
$ a
a))
  {-# INLINE pure #-}
  Curried forall r. g ((a -> b) -> r) -> h r
mf <*> :: Curried g h (a -> b) -> Curried g h a -> Curried g h b
<*> Curried forall r. g (a -> r) -> h r
ma = (forall r. g (b -> r) -> h r) -> Curried g h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (g (a -> r) -> h r
forall r. g (a -> r) -> h r
ma (g (a -> r) -> h r)
-> (g (b -> r) -> g (a -> r)) -> g (b -> r) -> h r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g ((a -> b) -> a -> r) -> h (a -> r)
forall r. g ((a -> b) -> r) -> h r
mf (g ((a -> b) -> a -> r) -> h (a -> r))
-> (g (b -> r) -> g ((a -> b) -> a -> r))
-> g (b -> r)
-> h (a -> r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> r) -> (a -> b) -> a -> r)
-> g (b -> r) -> g ((a -> b) -> a -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> r) -> (a -> b) -> a -> r
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 :: f a -> Curried f f a
liftCurried f a
fa = (forall r. f (a -> r) -> f r) -> Curried f f a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (f (a -> r) -> f a -> f r
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 :: Curried f g a -> g a
lowerCurried (Curried forall r. f (a -> r) -> g r
f) = f (a -> a) -> g a
forall r. f (a -> r) -> g r
f ((a -> a) -> f (a -> a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> a
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 :: 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 r. f (b -> r) -> h r) -> Curried f h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (g (a -> r) -> h r
forall r. g (a -> r) -> h r
ma (g (a -> r) -> h r)
-> (f (b -> r) -> g (a -> r)) -> f (b -> r) -> h r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ((a -> b) -> a -> r) -> g (a -> r)
forall r. f ((a -> b) -> r) -> g r
mf (f ((a -> b) -> a -> r) -> g (a -> r))
-> (f (b -> r) -> f ((a -> b) -> a -> r))
-> f (b -> r)
-> g (a -> r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> r) -> (a -> b) -> a -> r)
-> f (b -> r) -> f ((a -> b) -> a -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> r) -> (a -> b) -> a -> r
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 :: 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) = f (c -> a) -> g a
forall r. f (c -> r) -> g r
fg (b -> c -> a
bca (b -> c -> a) -> f b -> f (c -> a)
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 :: g a -> Curried f (Day f g) a
unapplied g a
ga = (forall r. f (a -> r) -> Day f g r) -> Curried f (Day f g) a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried ((forall r. f (a -> r) -> Day f g r) -> Curried f (Day f g) a)
-> (forall r. f (a -> r) -> Day f g r) -> Curried f (Day f g) a
forall a b. (a -> b) -> a -> b
$ \ f (a -> r)
fab -> f (a -> r) -> g a -> ((a -> r) -> a -> r) -> Day f g r
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 (a -> r) -> a -> r
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 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 r. g (a -> r) -> h r) -> Curried g h a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried ((forall r. g (a -> r) -> h r) -> Curried g h a)
-> (forall r. g (a -> r) -> h r) -> Curried g h a
forall a b. (a -> b) -> a -> b
$ \g (a -> r)
gar -> Day g k r -> h r
forall x. Day g k x -> h x
h (g (a -> r) -> k a -> ((a -> r) -> a -> r) -> Day g k r
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 (a -> r) -> a -> r
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 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) = Curried f h c -> f (c -> b) -> h b
forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a -> r) -> h r
runCurried (k c -> Curried f h c
forall a. k a -> Curried f h a
f k c
kd) (b -> c -> b
cdb (b -> c -> b) -> f b -> f (c -> b)
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 :: u a -> Curried f Identity a
adjointToCurried u a
ua = (forall r. f (a -> r) -> Identity r) -> Curried f Identity a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried (r -> Identity r
forall a. a -> Identity a
Identity (r -> Identity r) -> (f (a -> r) -> r) -> f (a -> r) -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> r) -> u r) -> f (a -> r) -> r
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct ((a -> r) -> u a -> u r
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 :: Curried f Identity a -> u a
curriedToAdjoint (Curried forall r. f (a -> r) -> Identity r
m) = (f (a -> a) -> a) -> (a -> a) -> u a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (f (a -> a) -> Identity a) -> f (a -> a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (a -> a) -> Identity a
forall r. f (a -> r) -> Identity r
m) a -> a
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 :: Curried f h a -> u (h a)
curriedToComposedAdjoint (Curried forall r. f (a -> r) -> h r
m) = (f (a -> a) -> h a) -> (a -> a) -> u (h a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f (a -> a) -> h a
forall r. f (a -> r) -> h r
m a -> a
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 :: u (h a) -> Curried f h a
composedAdjointToCurried u (h a)
uha = (forall r. f (a -> r) -> h r) -> Curried f h a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried ((forall r. f (a -> r) -> h r) -> Curried f h a)
-> (forall r. f (a -> r) -> h r) -> Curried f h a
forall a b. (a -> b) -> a -> b
$ ((a -> r) -> u (h r)) -> f (a -> r) -> h r
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\a -> r
b -> (a -> r) -> h a -> h r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> r
b (h a -> h r) -> u (h a) -> u (h r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> u (h a)
uha)
{-# INLINE composedAdjointToCurried #-}