{-# LANGUAGE CPP #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Safe #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2014-2015 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  portable
--
----------------------------------------------------------------------------
module Data.Profunctor.Monad where

import Control.Comonad
import Data.Bifunctor.Tannen
import Data.Bifunctor.Product
import Data.Bifunctor.Sum
import Data.Profunctor.Types

-- | 'ProfunctorFunctor' has a polymorphic kind since @5.6@.

-- ProfunctorFunctor :: ((Type -> Type -> Type) -> (k1 -> k2 -> Type)) -> Constraint
class ProfunctorFunctor t where
  -- | Laws:
  --
  -- @
  -- 'promap' f '.' 'promap' g ≡ 'promap' (f '.' g)
  -- 'promap' 'id' ≡ 'id'
  -- @
  promap :: Profunctor p => (p :-> q) -> t p :-> t q

instance Functor f => ProfunctorFunctor (Tannen f) where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Tannen f p :-> Tannen f q
promap p :-> q
f (Tannen f (p a b)
g) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p :-> q
f f (p a b)
g)

instance ProfunctorFunctor (Product p) where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Product p p :-> Product p q
promap p :-> q
f (Pair p a b
p p a b
q) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair p a b
p (p :-> q
f p a b
q)

instance ProfunctorFunctor (Sum p) where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Sum p p :-> Sum p q
promap p :-> q
_ (L2 p a b
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 p a b
p
  promap p :-> q
f (R2 p a b
q) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (p :-> q
f p a b
q)

-- | Laws:
--
-- @
-- 'promap' f '.' 'proreturn' ≡ 'proreturn' '.' f
-- 'projoin' '.' 'proreturn' ≡ 'id'
-- 'projoin' '.' 'promap' 'proreturn' ≡ 'id'
-- 'projoin' '.' 'projoin' ≡ 'projoin' '.' 'promap' 'projoin'
-- @

-- ProfunctorMonad :: ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> Constraint
class ProfunctorFunctor t => ProfunctorMonad t where
  proreturn :: Profunctor p => p :-> t p
  projoin   :: Profunctor p => t (t p) :-> t p

#if __GLASGOW_HASKELL__ < 710
instance (Functor f, Monad f) => ProfunctorMonad (Tannen f) where
#else
instance Monad f => ProfunctorMonad (Tannen f) where
#endif
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Tannen f p
proreturn = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
Tannen f (Tannen f p) :-> Tannen f p
projoin (Tannen f (Tannen f p a b)
m) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen forall a b. (a -> b) -> a -> b
$ f (Tannen f p a b)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {k1} {k2} {k3} (f :: k1 -> *) (p :: k2 -> k3 -> k1)
       (a :: k2) (b :: k3).
Tannen f p a b -> f (p a b)
runTannen

instance ProfunctorMonad (Sum p) where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Sum p p
proreturn = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
Sum p (Sum p p) :-> Sum p p
projoin (L2 p a b
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 p a b
p
  projoin (R2 Sum p p a b
m) = Sum p p a b
m

-- | Laws:
--
-- @
-- 'proextract' '.' 'promap' f ≡ f '.' 'proextract'
-- 'proextract' '.' 'produplicate' ≡ 'id'
-- 'promap' 'proextract' '.' 'produplicate' ≡ 'id'
-- 'produplicate' '.' 'produplicate' ≡ 'promap' 'produplicate' '.' 'produplicate'
-- @

-- ProfunctorComonad :: ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> Constraint
class ProfunctorFunctor t => ProfunctorComonad t where
  proextract :: Profunctor p => t p :-> p
  produplicate :: Profunctor p => t p :-> t (t p)

instance Comonad f => ProfunctorComonad (Tannen f) where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Tannen f p :-> p
proextract = forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} (f :: k1 -> *) (p :: k2 -> k3 -> k1)
       (a :: k2) (b :: k3).
Tannen f p a b -> f (p a b)
runTannen
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Tannen f p :-> Tannen f (Tannen f p)
produplicate (Tannen f (p a b)
w) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen forall a b. (a -> b) -> a -> b
$ forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen f (p a b)
w

instance ProfunctorComonad (Product p) where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Product p p :-> p
proextract (Pair p a b
_ p a b
q) = p a b
q
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Product p p :-> Product p (Product p p)
produplicate pq :: Product p p a b
pq@(Pair p a b
p p a b
_) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair p a b
p Product p p a b
pq