{-# 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 :: (p :-> q) -> Tannen f p :-> Tannen f q
promap p :-> q
f (Tannen f (p a b)
g) = f (q a b) -> Tannen f q a b
forall k k1 k2 (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen ((p a b -> q a b) -> f (p a b) -> f (q a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p a b -> q a b
p :-> q
f f (p a b)
g)

instance ProfunctorFunctor (Product p) where
  promap :: (p :-> q) -> Product p p :-> Product p q
promap p :-> q
f (Pair p a b
p p a b
q) = p a b -> q a b -> Product p q 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 (p a b -> q a b
p :-> q
f p a b
q)

instance ProfunctorFunctor (Sum p) where
  promap :: (p :-> q) -> Sum p p :-> Sum p q
promap p :-> q
_ (L2 p a b
p) = p a b -> Sum p q a b
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) = q a b -> Sum p q a b
forall k k1 (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (p a b -> q a b
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 :: p :-> Tannen f p
proreturn = f (p a b) -> Tannen f p a b
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) -> Tannen f p a b)
-> (p a b -> f (p a b)) -> p a b -> Tannen f p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a b -> f (p a b)
forall (m :: * -> *) a. Monad m => a -> m a
return
  projoin :: Tannen f (Tannen f p) :-> Tannen f p
projoin (Tannen f (Tannen f p a b)
m) = f (p a b) -> Tannen f p a b
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) -> Tannen f p a b) -> f (p a b) -> Tannen f p a b
forall a b. (a -> b) -> a -> b
$ f (Tannen f p a b)
m f (Tannen f p a b) -> (Tannen f p a b -> f (p a b)) -> f (p a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Tannen f p a b -> f (p a b)
forall k1 (f :: k1 -> *) k2 k3 (p :: k2 -> k3 -> k1) (a :: k2)
       (b :: k3).
Tannen f p a b -> f (p a b)
runTannen

instance ProfunctorMonad (Sum p) where
  proreturn :: p :-> Sum p p
proreturn = p a b -> Sum p p a b
forall k k1 (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2
  projoin :: Sum p (Sum p p) :-> Sum p p
projoin (L2 p a b
p) = p a b -> Sum p p a b
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 :: Tannen f p :-> p
proextract = f (p a b) -> p a b
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f (p a b) -> p a b)
-> (Tannen f p a b -> f (p a b)) -> Tannen f p a b -> p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tannen f p a b -> f (p a b)
forall k1 (f :: k1 -> *) k2 k3 (p :: k2 -> k3 -> k1) (a :: k2)
       (b :: k3).
Tannen f p a b -> f (p a b)
runTannen
  produplicate :: Tannen f p :-> Tannen f (Tannen f p)
produplicate (Tannen f (p a b)
w) = f (Tannen f p a b) -> Tannen f (Tannen f p) a b
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 (Tannen f p a b) -> Tannen f (Tannen f p) a b)
-> f (Tannen f p a b) -> Tannen f (Tannen f p) a b
forall a b. (a -> b) -> a -> b
$ (f (p a b) -> Tannen f p a b) -> f (p a b) -> f (Tannen f p a b)
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f (p a b) -> Tannen f p a b
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 :: Product p p :-> p
proextract (Pair p a b
_ p a b
q) = p a b
q
  produplicate :: Product p p :-> Product p (Product p p)
produplicate pq :: Product p p a b
pq@(Pair p a b
p p a b
_) = p a b -> Product p p a b -> Product p (Product 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