Presheaf.hs

{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wall -Werror #-}

-- | A reified presheaf: a contravariant mapping from one category to another,
-- wrapping @forall a b. cat a b -> cat' (f b) (f a)@.
--
-- 'Presheaf' @cat cat' f@ reifies the action of a contravariant functor on
-- a type constructor @f@, generalised over a source category @cat@ and a
-- target category @cat'@. When both are @(->)@, this specialises to
-- 'Presheaf'' @f@ wrapping @forall a b. (a -> b) -> f b -> f a@, which is
-- exactly 'Data.Functor.Contravariant.contramap'.
--
-- Unlike 'Data.Functor.Contravariant.Contravariant' which is a type class
-- (one instance per type), this is a value — and it is generalised over the
-- source and target categories.
--
-- @
-- newtype 'Presheaf' cat cat' f = 'Presheaf' (forall a b. cat a b -> cat' (f b) (f a))
-- type 'Presheaf'' f = 'Presheaf' (->) (->) f
-- @
module Data.Valuation.Presheaf
  ( Presheaf (..),
    Presheaf',

    -- * combinators
    runPresheaf,
    composePresheafFunctor,
    composeFunctorPresheaf,
    composePresheaf,
    contramapPresheaf,

    -- * presheaf values
    predicatePresheaf,
    comparisonPresheaf,
    equivalencePresheaf,
    proxyPresheaf,
    constPresheaf,

    -- * laws
    lawPresheafIdentity,
    lawPresheafComposition,
  )
where

import Data.Functor.Compose (Compose (..))
import Data.Functor.Const (Const (..))
import Data.Functor.Contravariant
  ( Comparison (..),
    Contravariant (contramap),
    Equivalence (..),
    Predicate (..),
  )
import Data.Profunctor (Profunctor (dimap))
import Data.Proxy (Proxy)
import Data.Valuation.CovariantFunctor (CovariantFunctor (..))

-- $setup
-- >>> :set -Wno-name-shadowing -Wno-type-defaults
-- >>> import Data.Functor.Contravariant (Predicate(..), getPredicate, Comparison(..), getComparison, Equivalence(..), getEquivalence)
-- >>> import Data.Functor.Const (Const(..))
-- >>> import Data.Proxy (Proxy(..))

-- |
-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 3
-- True
-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 4
-- False
--
-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 1 2
-- GT
newtype Presheaf cat cat' f = Presheaf (forall a b. cat a b -> cat' (f b) (f a))

-- | A 'Presheaf' specialised to @(->)@ for both categories.
-- Wraps @forall a b. (a -> b) -> f b -> f a@, equivalent to
-- 'Data.Functor.Contravariant.contramap'.
type Presheaf' f = Presheaf (->) (->) f

-- | Unwrap a 'Presheaf' to its underlying natural transformation.
--
-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 3
-- True
-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 4
-- False
--
-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 1 2
-- GT
-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 2 1
-- LT
runPresheaf :: Presheaf cat cat' f -> cat a b -> cat' (f b) (f a)
runPresheaf (Presheaf f) = f

-- | Compose a 'Presheaf' (contravariant) with a 'CovariantFunctor' (covariant).
-- The result is contravariant (contravariant ∘ covariant = contravariant).
--
-- Given @f@ contravariant from @cat@ to @cat'@ and @g@ covariant from @cat'@ to @cat''@,
-- @g ∘ f@ is contravariant from @cat@ to @cat''@ acting on @'Compose' g f@.
--
-- >>> import Data.Functor.Compose (Compose(..))
-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), proxyCovariantFunctor, maybeCovariantFunctor)
-- >>> let p = composePresheafFunctor constPresheaf proxyCovariantFunctor
-- >>> runPresheaf p not (Compose (Proxy :: Proxy (Const Int Bool)))
-- Compose Proxy
--
-- >>> import Data.Functor.Compose (Compose(..))
-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), maybeCovariantFunctor)
-- >>> let p = composePresheafFunctor constPresheaf maybeCovariantFunctor
-- >>> runPresheaf p not (Compose (Just (Const 42 :: Const Int Bool)))
-- Compose (Just (Const 42))
-- >>> runPresheaf p not (Compose Nothing :: Compose Maybe (Const Int) Bool)
-- Compose Nothing
composePresheafFunctor ::
  (Profunctor cat'') =>
  Presheaf cat cat' f ->
  CovariantFunctor cat' cat'' g ->
  Presheaf cat cat'' (Compose g f)
composePresheafFunctor (Presheaf f) (CovariantFunctor g) =
  Presheaf (dimap getCompose Compose . g . f)

-- | Compose a 'CovariantFunctor' (covariant) with a 'Presheaf' (contravariant).
-- The result is contravariant (covariant ∘ contravariant = contravariant).
--
-- Given @f@ covariant from @cat@ to @cat'@ and @g@ contravariant from @cat'@ to @cat''@,
-- @g ∘ f@ is contravariant from @cat@ to @cat''@ acting on @'Compose' g f@.
--
-- >>> import Data.Functor.Compose (Compose(..))
-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), proxyCovariantFunctor, maybeCovariantFunctor)
-- >>> let p = composeFunctorPresheaf proxyCovariantFunctor constPresheaf
-- >>> runPresheaf p not (Compose (Const 42 :: Const Int (Proxy Bool)))
-- Compose (Const 42)
--
-- >>> import Data.Functor.Compose (Compose(..))
-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), maybeCovariantFunctor)
-- >>> let p = composeFunctorPresheaf maybeCovariantFunctor constPresheaf
-- >>> runPresheaf p not (Compose (Const 42 :: Const Int (Maybe Bool)))
-- Compose (Const 42)
composeFunctorPresheaf ::
  (Profunctor cat'') =>
  CovariantFunctor cat cat' f ->
  Presheaf cat' cat'' g ->
  Presheaf cat cat'' (Compose g f)
composeFunctorPresheaf (CovariantFunctor f) (Presheaf g) =
  Presheaf (dimap getCompose Compose . g . f)

-- | Compose two presheaves (contravariant functors) to obtain a covariant functor.
-- The result is covariant (contravariant ∘ contravariant = covariant).
--
-- Given @f@ contravariant from @cat@ to @cat'@ and @g@ contravariant from @cat'@ to @cat''@,
-- @g ∘ f@ is covariant from @cat@ to @cat''@ acting on @'Compose' g f@.
--
-- >>> import Data.Functor.Compose (Compose(..))
-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), runCovariantFunctor)
-- >>> let p = composePresheaf constPresheaf proxyPresheaf
-- >>> runCovariantFunctor p not (Compose (Proxy :: Proxy (Const Int Bool)))
-- Compose Proxy
--
-- >>> import Data.Functor.Compose (Compose(..))
-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), runCovariantFunctor)
-- >>> let p = composePresheaf proxyPresheaf constPresheaf
-- >>> runCovariantFunctor p not (Compose (Const Proxy :: Const (Proxy Bool) (Proxy Bool)))
-- Compose (Const Proxy)
composePresheaf ::
  (Profunctor cat'') =>
  Presheaf cat cat' f ->
  Presheaf cat' cat'' g ->
  CovariantFunctor cat cat'' (Compose g f)
composePresheaf (Presheaf f) (Presheaf g) =
  CovariantFunctor (dimap getCompose Compose . g . f)

-- | The canonical 'Presheaf'' for any 'Data.Functor.Contravariant.Contravariant' functor,
-- using 'Data.Functor.Contravariant.contramap'.
--
-- >>> getPredicate (runPresheaf contramapPresheaf abs (Predicate (> 3) :: Predicate Int)) (-5)
-- True
-- >>> getPredicate (runPresheaf contramapPresheaf abs (Predicate (> 3) :: Predicate Int)) (-2)
-- False
--
-- >>> getEquivalence (runPresheaf contramapPresheaf (`mod` 3) (Equivalence (==) :: Equivalence Int)) 4 7
-- True
-- >>> getEquivalence (runPresheaf contramapPresheaf (`mod` 3) (Equivalence (==) :: Equivalence Int)) 4 6
-- False
contramapPresheaf :: (Contravariant f) => Presheaf' f
contramapPresheaf = Presheaf contramap

-- | 'Presheaf'' on 'Predicate': pulls back a predicate along a function.
--
-- >>> getPredicate (runPresheaf predicatePresheaf even (Predicate not)) 2
-- False
-- >>> getPredicate (runPresheaf predicatePresheaf even (Predicate not)) 3
-- True
--
-- >>> getPredicate (runPresheaf predicatePresheaf abs (Predicate (> 3) :: Predicate Int)) (-5)
-- True
-- >>> getPredicate (runPresheaf predicatePresheaf abs (Predicate (> 3) :: Predicate Int)) (-2)
-- False
predicatePresheaf :: Presheaf' Predicate
predicatePresheaf = Presheaf contramap

-- | 'Presheaf'' on 'Comparison': pulls back a comparison along a function.
--
-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 1 2
-- GT
-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 2 1
-- LT
--
-- >>> getComparison (runPresheaf comparisonPresheaf length (Comparison compare :: Comparison Int)) "hi" "hello"
-- LT
comparisonPresheaf :: Presheaf' Comparison
comparisonPresheaf = Presheaf contramap

-- | 'Presheaf'' on 'Equivalence': pulls back an equivalence relation along a function.
--
-- >>> getEquivalence (runPresheaf equivalencePresheaf even (Equivalence (==) :: Equivalence Bool)) 2 4
-- True
-- >>> getEquivalence (runPresheaf equivalencePresheaf even (Equivalence (==) :: Equivalence Bool)) 2 3
-- False
--
-- >>> getEquivalence (runPresheaf equivalencePresheaf (`mod` 3) (Equivalence (==) :: Equivalence Int)) 4 7
-- True
equivalencePresheaf :: Presheaf' Equivalence
equivalencePresheaf = Presheaf contramap

-- | 'Presheaf'' on 'Proxy': trivially maps the phantom type parameter.
--
-- >>> runPresheaf proxyPresheaf not (Proxy :: Proxy Bool)
-- Proxy
--
-- >>> runPresheaf proxyPresheaf length (Proxy :: Proxy Int)
-- Proxy
proxyPresheaf :: Presheaf' Proxy
proxyPresheaf = Presheaf contramap

-- | 'Presheaf'' on @'Const' r@: trivially maps the phantom second parameter.
-- The constant value is preserved.
--
-- >>> runPresheaf constPresheaf not (Const 42 :: Const Int Bool)
-- Const 42
--
-- >>> runPresheaf constPresheaf length (Const "hello" :: Const String Int)
-- Const "hello"
constPresheaf :: Presheaf' (Const r)
constPresheaf = Presheaf contramap

-- | The identity law for a 'Presheaf'': mapping the identity morphism
-- must be the identity on @f a@.
--
-- @
-- 'runPresheaf' p 'id' x == x
-- @
--
-- >>> lawPresheafIdentity proxyPresheaf (Proxy :: Proxy Int)
-- True
-- >>> lawPresheafIdentity constPresheaf (Const 42 :: Const Int Bool)
-- True
lawPresheafIdentity :: (Eq (f a)) => Presheaf' f -> f a -> Bool
lawPresheafIdentity p x =
  runPresheaf p id x == x

-- | The composition law for a 'Presheaf'': mapping a composition must
-- equal composing the individual mappings, with contravariant reversal.
--
-- @
-- 'runPresheaf' p (g '.' f) x == 'runPresheaf' p f ('runPresheaf' p g x)
-- @
--
-- >>> lawPresheafComposition proxyPresheaf not (&&True) (Proxy :: Proxy Bool)
-- True
-- >>> lawPresheafComposition constPresheaf (+1) (*2) (Const "hello" :: Const String Int)
-- True
lawPresheafComposition :: (Eq (f a)) => Presheaf' f -> (b -> c) -> (a -> b) -> f c -> Bool
lawPresheafComposition p g f x =
  runPresheaf p (g . f) x == runPresheaf p f (runPresheaf p g x)