{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}

module Profunctor.Monad.Cofunctor
  ( Profunctor
  , Cofunctor (..)
  , (=.)
  , (=:)
  , cofilter
  ) where

import Control.Applicative (Alternative)
import Control.Monad (guard)
import Control.Arrow (Kleisli(..), Arrow(..))
import Control.Category (Category, (>>>))
import Data.Functor (($>))
import Data.Constraint.Forall

infixl 5 =:, =.

-- | A 'Profunctor' is a bifunctor @p :: * -> * -> *@ from the product of an
-- arbitrary category, denoted @'First' p@, and @(->)@.
--
-- This is a generalization of the 'profunctors' package's @Profunctor@,
-- where @'First' p ~ (->)@.
--
-- A profunctor is two functors on different domains at once, one
-- contravariant, one covariant, and that is made clear by this definition
-- specifying 'Cofunctor' and 'Functor' separately.
--
type Profunctor p = (Cofunctor p, ForallF Functor p)

-- | Types @p :: * -> * -> *@ which are contravariant functors
-- over their first parameter.
--
-- Functor laws:
--
-- @
-- 'lmap' 'id' = 'id'
-- 'lmap' (i '>>>' j) = 'lmap' i '.' 'lmap' j
-- @
--
-- If the domain @'First' p@ is an 'Arrow', and if for every @a@, the type
-- @p a@ is an instance of 'Applicative', then a pure arrow 'arr' f should
-- correspond to an "applicative natural transformation":
--
-- @
-- 'lmap' ('arr' f) (p '<*>' q)
-- =
-- 'lmap' ('arr' f) p '<*>' 'lmap' ('arr' f) q
-- @
--
-- @
-- 'lmap' ('arr' f) ('pure' a) = 'pure' a
-- @
--
-- The following may not be true in general, but seems to hold in practice,
-- when the instance @'Applicative' (p a)@ orders effects from left to right,
-- in particular that should be the case if there is also a @'Monad' (p a)@:
--
-- @
-- 'lmap' ('first' i) ('lmap' ('arr' 'fst') p '<*>' 'lmap' ('arr' 'snd') q)
-- =
-- 'lmap' ('first' i '>>>' 'arr' 'fst') p '<*>' 'lmap' ('arr' 'snd') q
-- @
--
class Category (First p) => Cofunctor p where
  -- | Domain of the functor.
  type First p :: * -> * -> *
  -- | Mapping morphisms from @'First' p@ to @(->)@.
  lmap :: First p y x -> p x a -> p y a

instance Cofunctor (->) where
  type First (->) = (->)
  lmap :: First (->) y x -> (x -> a) -> y -> a
lmap First (->) y x
f x -> a
g = x -> a
g (x -> a) -> (y -> x) -> y -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First (->) y x
y -> x
f

instance Monad m => Cofunctor (Kleisli m) where
  type First (Kleisli m) = Kleisli m
  lmap :: First (Kleisli m) y x -> Kleisli m x a -> Kleisli m y a
lmap = First (Kleisli m) y x -> Kleisli m x a -> Kleisli m y a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
(>>>)

-- | Mapping with a regular function.
(=.)
  :: (Cofunctor p, Arrow (First p))
  => (y -> x) -> p x a -> p y a
=. :: (y -> x) -> p x a -> p y a
(=.) = First p y x -> p x a -> p y a
forall (p :: * -> * -> *) y x a.
Cofunctor p =>
First p y x -> p x a -> p y a
lmap (First p y x -> p x a -> p y a)
-> ((y -> x) -> First p y x) -> (y -> x) -> p x a -> p y a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (y -> x) -> First p y x
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr

-- | Monadic mapping; e.g., mapping which can fail ('Maybe').
(=:)
  :: (Cofunctor p, First p ~ Kleisli m)
  => (y -> m x) -> p x a -> p y a
=: :: (y -> m x) -> p x a -> p y a
(=:) = Kleisli m y x -> p x a -> p y a
forall (p :: * -> * -> *) y x a.
Cofunctor p =>
First p y x -> p x a -> p y a
lmap (Kleisli m y x -> p x a -> p y a)
-> ((y -> m x) -> Kleisli m y x) -> (y -> m x) -> p x a -> p y a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (y -> m x) -> Kleisli m y x
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli

cofilter
  :: (Cofunctor p, First p ~ Kleisli m, Alternative m)
  => (x -> Bool) -> p x a -> p x a
cofilter :: (x -> Bool) -> p x a -> p x a
cofilter x -> Bool
p = (x -> m x) -> p x a -> p x a
forall (p :: * -> * -> *) (m :: * -> *) y x a.
(Cofunctor p, First p ~ Kleisli m) =>
(y -> m x) -> p x a -> p y a
(=:) (\x
x -> Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (x -> Bool
p x
x) m () -> x -> m x
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> x
x)