{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE KindSignatures #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2013-2016 Edward Kmett, Gershom Bazerman and Derek Elkins
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  portable
--
-- The Day convolution of two contravariant functors is a contravariant
-- functor.
--
-- <http://ncatlab.org/nlab/show/Day+convolution>
----------------------------------------------------------------------------

module Data.Functor.Contravariant.Day
  ( Day(..)
  , day
  , runDay
  , assoc, disassoc
  , swapped
  , intro1, intro2
  , day1, day2
  , diag
  , trans1, trans2
  ) where

import Control.Arrow ((***))
import Data.Functor.Contravariant
import Data.Functor.Contravariant.Rep
import Data.Functor.Contravariant.Adjunction
import Data.Functor.Contravariant.Divisible
import Data.Proxy
import Data.Tuple (swap)
import Data.Typeable

-- | The Day convolution of two contravariant functors.
data Day f g a = forall b c. Day (f b) (g c) (a -> (b, c))
  deriving Typeable

-- | Construct the Day convolution
--
-- @
-- 'day1' ('day' f g) = f
-- 'day2' ('day' f g) = g
-- @
day :: f a -> g b -> Day f g (a, b)
day :: forall (f :: * -> *) a (g :: * -> *) b.
f a -> g b -> Day f g (a, b)
day f a
fa g b
gb = f a -> g b -> ((a, b) -> (a, b)) -> Day f g (a, b)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f a
fa g b
gb (a, b) -> (a, b)
forall a. a -> a
id

instance Contravariant (Day f g) where
  contramap :: forall a' a. (a' -> a) -> Day f g a -> Day f g a'
contramap a' -> a
f (Day f b
fb g c
gc a -> (b, c)
abc) = f b -> g c -> (a' -> (b, c)) -> Day f g a'
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f b
fb g c
gc (a -> (b, c)
abc (a -> (b, c)) -> (a' -> a) -> a' -> (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> a
f)

instance (Divisible f, Divisible g) => Divisible (Day f g) where
  divide :: forall a b c. (a -> (b, c)) -> Day f g b -> Day f g c -> Day f g a
divide a -> (b, c)
h (Day f b
f g c
g b -> (b, c)
l) (Day f b
f' g c
g' c -> (b, c)
r) = f (b, b) -> g (c, c) -> (a -> ((b, b), (c, c))) -> Day f g a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day (f b -> f b -> f (b, b)
forall (f :: * -> *) a b. Divisible f => f a -> f b -> f (a, b)
divided f b
f f b
f') (g c -> g c -> g (c, c)
forall (f :: * -> *) a b. Divisible f => f a -> f b -> f (a, b)
divided g c
g g c
g') (((b, c), (b, c)) -> ((b, b), (c, c))
forall {a} {a} {b} {b}. ((a, a), (b, b)) -> ((a, b), (a, b))
intertwine (((b, c), (b, c)) -> ((b, b), (c, c)))
-> (a -> ((b, c), (b, c))) -> a -> ((b, b), (c, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> (b, c)
l (b -> (b, c)) -> (c -> (b, c)) -> (b, c) -> ((b, c), (b, c))
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** c -> (b, c)
r) ((b, c) -> ((b, c), (b, c)))
-> (a -> (b, c)) -> a -> ((b, c), (b, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
h)
    where intertwine :: ((a, a), (b, b)) -> ((a, b), (a, b))
intertwine ((a
a, a
b), (b
c, b
d)) = ((a
a, b
c), (a
b, b
d))
  conquer :: forall a. Day f g a
conquer = f a -> g a -> (a -> (a, a)) -> Day f g a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f a
forall a. f a
forall (f :: * -> *) a. Divisible f => f a
conquer g a
forall a. g a
forall (f :: * -> *) a. Divisible f => f a
conquer (\a
a -> (a
a, a
a))

instance (Representable f, Representable g) => Representable (Day f g) where
  type Rep (Day f g) = (Rep f, Rep g)

  tabulate :: forall a. (a -> Rep (Day f g)) -> Day f g a
tabulate a -> Rep (Day f g)
a2fg = f (Rep f, Rep g)
-> g (Rep f, Rep g)
-> (a -> ((Rep f, Rep g), (Rep f, Rep g)))
-> Day f g a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day (((Rep f, Rep g) -> Rep f) -> f (Rep f, Rep g)
forall a. (a -> Rep f) -> f a
forall (f :: * -> *) a. Representable f => (a -> Rep f) -> f a
tabulate (Rep f, Rep g) -> Rep f
forall a b. (a, b) -> a
fst) (((Rep f, Rep g) -> Rep g) -> g (Rep f, Rep g)
forall a. (a -> Rep g) -> g a
forall (f :: * -> *) a. Representable f => (a -> Rep f) -> f a
tabulate (Rep f, Rep g) -> Rep g
forall a b. (a, b) -> b
snd) ((a -> ((Rep f, Rep g), (Rep f, Rep g))) -> Day f g a)
-> (a -> ((Rep f, Rep g), (Rep f, Rep g))) -> Day f g a
forall a b. (a -> b) -> a -> b
$ \a
a -> let b :: Rep (Day f g)
b = a -> Rep (Day f g)
a2fg a
a in ((Rep f, Rep g)
Rep (Day f g)
b,(Rep f, Rep g)
Rep (Day f g)
b)

  index :: forall a. Day f g a -> a -> Rep (Day f g)
index (Day f b
fb g c
gc a -> (b, c)
abc) a
a = case a -> (b, c)
abc a
a of
    (b
b, c
c) -> (f b -> b -> Rep f
forall a. f a -> a -> Rep f
forall (f :: * -> *) a. Representable f => f a -> a -> Rep f
index f b
fb b
b, g c -> c -> Rep g
forall a. g a -> a -> Rep g
forall (f :: * -> *) a. Representable f => f a -> a -> Rep f
index g c
gc c
c)
  {-# INLINE index #-}

  contramapWithRep :: forall b a.
(b -> Either a (Rep (Day f g))) -> Day f g a -> Day f g b
contramapWithRep b -> Either a (Rep (Day f g))
d2eafg (Day f b
fb g c
gc a -> (b, c)
abc) = f (Either b (Rep f))
-> g (Either c (Rep g))
-> (b -> (Either b (Rep f), Either c (Rep g)))
-> Day f g b
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day ((Either b (Rep f) -> Either b (Rep f))
-> f b -> f (Either b (Rep f))
forall b a. (b -> Either a (Rep f)) -> f a -> f b
forall (f :: * -> *) b a.
Representable f =>
(b -> Either a (Rep f)) -> f a -> f b
contramapWithRep Either b (Rep f) -> Either b (Rep f)
forall a. a -> a
id f b
fb) ((Either c (Rep g) -> Either c (Rep g))
-> g c -> g (Either c (Rep g))
forall b a. (b -> Either a (Rep g)) -> g a -> g b
forall (f :: * -> *) b a.
Representable f =>
(b -> Either a (Rep f)) -> f a -> f b
contramapWithRep Either c (Rep g) -> Either c (Rep g)
forall a. a -> a
id g c
gc) ((b -> (Either b (Rep f), Either c (Rep g))) -> Day f g b)
-> (b -> (Either b (Rep f), Either c (Rep g))) -> Day f g b
forall a b. (a -> b) -> a -> b
$ \b
d -> case b -> Either a (Rep (Day f g))
d2eafg b
d of
    Left a
a -> case a -> (b, c)
abc a
a of
      (b
b, c
c) -> (b -> Either b (Rep f)
forall a b. a -> Either a b
Left b
b, c -> Either c (Rep g)
forall a b. a -> Either a b
Left c
c)
    Right (Rep f
vf, Rep g
vg) -> (Rep f -> Either b (Rep f)
forall a b. b -> Either a b
Right Rep f
vf, Rep g -> Either c (Rep g)
forall a b. b -> Either a b
Right Rep g
vg)
  {-# INLINE tabulate #-}

instance (Adjunction f u, Adjunction f' u') => Adjunction (Day f f') (Day u u') where
  unit :: forall a. a -> Day u u' (Day f f' a)
unit a
a = u (f a)
-> u' (f' a)
-> (Day f f' a -> (f a, f' a))
-> Day u u' (Day f f' a)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day (a -> u (f a)
forall a. a -> u (f a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit a
a) (a -> u' (f' a)
forall a. a -> u' (f' a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit a
a) (\(Day f b
f f' c
f' a -> (b, c)
g) -> ((a -> b) -> f b -> f a
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
g) f b
f, (a -> c) -> f' c -> f' a
forall a' a. (a' -> a) -> f' a -> f' a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
g) f' c
f'))
  counit :: forall a. a -> Day f f' (Day u u' a)
counit a
a = f (u a)
-> f' (u' a)
-> (Day u u' a -> (u a, u' a))
-> Day f f' (Day u u' a)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day (a -> f (u a)
forall a. a -> f (u a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> f (g a)
counit a
a) (a -> f' (u' a)
forall a. a -> f' (u' a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> f (g a)
counit a
a) (\(Day u b
u u' c
u' a -> (b, c)
g) -> ((a -> b) -> u b -> u a
forall a' a. (a' -> a) -> u a -> u a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
g) u b
u, (a -> c) -> u' c -> u' a
forall a' a. (a' -> a) -> u' a -> u' a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
g) u' c
u'))

-- | Break apart the Day convolution of two contravariant functors.
runDay :: (Contravariant f, Contravariant g) => Day f g a -> (f a, g a)
runDay :: forall (f :: * -> *) (g :: * -> *) a.
(Contravariant f, Contravariant g) =>
Day f g a -> (f a, g a)
runDay (Day f b
fb g c
gc a -> (b, c)
abc) =
  ( (a -> b) -> f b -> f a
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc) f b
fb
  , (a -> c) -> g c -> g a
forall a' a. (a' -> a) -> g a -> g a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc) g c
gc
  )

-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'contramap' f '.' 'assoc' = 'assoc' '.' 'contramap' f
-- @
assoc :: Day f (Day g h) a -> Day (Day f g) h a
assoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
Day f (Day g h) a -> Day (Day f g) h a
assoc (Day f b
fb (Day g b
gd h c
he c -> (b, c)
cde) a -> (b, c)
abc) = Day f g (b, b) -> h c -> (a -> ((b, b), c)) -> Day (Day f g) h a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day (f b -> g b -> ((b, b) -> (b, b)) -> Day f g (b, b)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f b
fb g b
gd (b, b) -> (b, b)
forall a. a -> a
id) h c
he ((a -> ((b, b), c)) -> Day (Day f g) h a)
-> (a -> ((b, b), c)) -> Day (Day f g) h a
forall a b. (a -> b) -> a -> b
$ \a
a ->
  case c -> (b, c)
cde (c -> (b, c)) -> (b, c) -> (b, (b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> (b, c)
abc a
a of
    (b
b, (b
d, c
e)) -> ((b
b, b
d), c
e)

-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'contramap' f '.' 'disassoc' = 'disassoc' '.' 'contramap' f
-- @
disassoc :: Day (Day f g) h a -> Day f (Day g h) a
disassoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
Day (Day f g) h a -> Day f (Day g h) a
disassoc (Day (Day f b
fd g c
ge b -> (b, c)
bde) h c
hc a -> (b, c)
abc) = f b -> Day g h (c, c) -> (a -> (b, (c, c))) -> Day f (Day g h) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f b
fd (g c -> h c -> ((c, c) -> (c, c)) -> Day g h (c, c)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day g c
ge h c
hc (c, c) -> (c, c)
forall a. a -> a
id) ((a -> (b, (c, c))) -> Day f (Day g h) a)
-> (a -> (b, (c, c))) -> Day f (Day g h) a
forall a b. (a -> b) -> a -> b
$ \a
a ->
  case a -> (b, c)
abc a
a of
    (b
b, c
c) -> case b -> (b, c)
bde b
b of
      (b
d, c
e) -> (b
d, (c
e, c
c))

-- | The monoid for Day convolution /in Haskell/ is symmetric.
--
-- @
-- 'contramap' f '.' 'swapped' = 'swapped' '.' 'contramap' f
-- @
swapped :: Day f g a -> Day g f a
swapped :: forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a
swapped (Day f b
fb g c
gc a -> (b, c)
abc) = g c -> f b -> (a -> (c, b)) -> Day g f a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day g c
gc f b
fb ((b, c) -> (c, b)
forall a b. (a, b) -> (b, a)
swap ((b, c) -> (c, b)) -> (a -> (b, c)) -> a -> (c, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc)

-- | Proxy serves as the unit of Day convolution.
--
-- @
-- 'day1' '.' 'intro1' = 'id'
-- 'contramap' f '.' 'intro1' = 'intro1' '.' 'contramap' f
-- @
intro1 :: f a -> Day Proxy f a
intro1 :: forall (f :: * -> *) a. f a -> Day Proxy f a
intro1 f a
fa = Proxy () -> f a -> (a -> ((), a)) -> Day Proxy f a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day Proxy ()
forall {k} (t :: k). Proxy t
Proxy f a
fa ((a -> ((), a)) -> Day Proxy f a)
-> (a -> ((), a)) -> Day Proxy f a
forall a b. (a -> b) -> a -> b
$ \a
a -> ((),a
a)

-- | Proxy serves as the unit of Day convolution.
--
-- @
-- 'day2' '.' 'intro2' = 'id'
-- 'contramap' f '.' 'intro2' = 'intro2' '.' 'contramap' f
-- @
intro2 :: f a -> Day f Proxy a
intro2 :: forall (f :: * -> *) a. f a -> Day f Proxy a
intro2 f a
fa = f a -> Proxy () -> (a -> (a, ())) -> Day f Proxy a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f a
fa Proxy ()
forall {k} (t :: k). Proxy t
Proxy ((a -> (a, ())) -> Day f Proxy a)
-> (a -> (a, ())) -> Day f Proxy a
forall a b. (a -> b) -> a -> b
$ \a
a -> (a
a,())

-- | In Haskell we can do general purpose elimination, but in a more general setting
-- it is only possible to eliminate the unit.
--
-- @
-- 'day1' '.' 'intro1' = 'id'
-- 'day1' = 'fst' '.' 'runDay'
-- 'contramap' f '.' 'day1' = 'day1' '.' 'contramap' f
-- @
day1 :: Contravariant f => Day f g a -> f a
day1 :: forall (f :: * -> *) (g :: * -> *) a.
Contravariant f =>
Day f g a -> f a
day1 (Day f b
fb g c
_ a -> (b, c)
abc) = (a -> b) -> f b -> f a
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc) f b
fb

-- | In Haskell we can do general purpose elimination, but in a more general setting
-- it is only possible to eliminate the unit.
-- @
-- 'day2' '.' 'intro2' = 'id'
-- 'day2' = 'snd' '.' 'runDay'
-- 'contramap' f '.' 'day2' = 'day2' '.' 'contramap' f
-- @
day2 :: Contravariant g => Day f g a -> g a
day2 :: forall (g :: * -> *) (f :: * -> *) a.
Contravariant g =>
Day f g a -> g a
day2 (Day f b
_ g c
gc a -> (b, c)
abc) = (a -> c) -> g c -> g a
forall a' a. (a' -> a) -> g a -> g a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc) g c
gc

-- | Diagonalize the Day convolution:
--
-- @
-- 'day1' '.' 'diag' = 'id'
-- 'day2' '.' 'diag' = 'id'
-- 'runDay' '.' 'diag' = \a -> (a,a)
-- 'contramap' f . 'diag' = 'diag' . 'contramap' f
-- @

diag :: f a -> Day f f a
diag :: forall (f :: * -> *) a. f a -> Day f f a
diag f a
fa = f a -> f a -> (a -> (a, a)) -> Day f f a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f a
fa f a
fa ((a -> (a, a)) -> Day f f a) -> (a -> (a, a)) -> Day f f a
forall a b. (a -> b) -> a -> b
$ \a
a -> (a
a,a
a)

-- | Apply a natural transformation to the left-hand side of a Day convolution.
--
-- This respects the naturality of the natural transformation you supplied:
--
-- @
-- 'contramap' f '.' 'trans1' fg = 'trans1' fg '.' 'contramap' f
-- @
trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
(forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 forall x. f x -> g x
fg (Day f b
fb h c
hc a -> (b, c)
abc) = g b -> h c -> (a -> (b, c)) -> Day g h a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day (f b -> g b
forall x. f x -> g x
fg f b
fb) h c
hc a -> (b, c)
abc

-- | Apply a natural transformation to the right-hand side of a Day convolution.
--
-- This respects the naturality of the natural transformation you supplied:
--
-- @
-- 'contramap' f '.' 'trans2' fg = 'trans2' fg '.' 'contramap' f
-- @
trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *) a.
(forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 forall x. g x -> h x
gh (Day f b
fb g c
gc a -> (b, c)
abc) = f b -> h c -> (a -> (b, c)) -> Day f h a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Day f b
fb (g c -> h c
forall x. g x -> h x
gh g c
gc) a -> (b, c)
abc