Add an Invariant version of Day

Derived by combining the covariant and contravariant versions of Day. Using this
as a tensor gives us a combination of Applicative and Divisible, which seems
useful for things like derivation of function pairs like parsers/printers.

kan-extensions.cabal

@@ -57,6 +57,7 @@ library
     containers    >= 0.4     && < 0.6,
     contravariant >= 1       && < 2,
     distributive  >= 0.2.2   && < 1,
+    invariant     >= 0.1     && < 1,
     fail          >= 4.9     && < 5,
     free          >= 4       && < 6,
     mtl           >= 2.0.1   && < 2.3,
@@ -75,6 +76,7 @@ library
     Data.Functor.Contravariant.Coyoneda
     Data.Functor.Day
     Data.Functor.Day.Curried
+    Data.Functor.Invariant.Day
     Data.Functor.Kan.Lan
     Data.Functor.Kan.Ran
     Data.Functor.Yoneda

src/Data/Functor/Invariant/Day.hs

@@ -0,0 +1,150 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE RankNTypes                #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2018 Brian Mckenna
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- The Day convolution of two invariant functors is an invariant
+-- functor.
+--
+-- <http://ncatlab.org/nlab/show/Day+convolution>
+----------------------------------------------------------------------------
+
+module Data.Functor.Invariant.Day
+  ( Day(..)
+  , day
+  , assoc, disassoc
+  , swapped
+  , intro1, intro2
+  , elim1, elim2
+  , trans1, trans2
+  , toContravariant, toCovariant
+  ) where
+
+import qualified Data.Functor.Contravariant.Day as Contravariant
+import qualified Data.Functor.Day               as Covariant
+import           Data.Functor.Identity
+import           Data.Functor.Invariant
+
+-- | The Day convolution of two invariant functors.
+data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a) (a -> (b, c))
+
+instance Invariant (Day f g) where
+  invmap f g (Day fb gc bca abc) = Day fb gc ((f .) . bca) (abc . g)
+
+-- | Construct the Day convolution
+day :: f a -> g b -> Day f g (a, b)
+day fa gb = Day fa gb (,) id
+
+-- | Day convolution provides a monoidal product. The associativity
+-- of this monoid is witnessed by 'assoc' and 'disassoc'.
+--
+-- @
+-- 'assoc' . 'disassoc' = 'id'
+-- 'disassoc' . 'assoc' = 'id'
+-- 'invmap' f g '.' 'assoc' = 'assoc' '.' 'invmap' f g
+-- @
+assoc :: Day f (Day g h) a -> Day (Day f g) h a
+assoc (Day fb (Day gd he dec cde) bca abc) = flip (Day (Day fb gd (,) id) he) f g
+  where
+    f a =
+      let (b,c) = abc a
+          (d,e) = cde c
+      in ((b,d),e)
+    g (b,d) e =
+      bca b (dec d e)
+
+-- | Day convolution provides a monoidal product. The associativity
+-- of this monoid is witnessed by 'assoc' and 'disassoc'.
+--
+-- @
+-- 'assoc' . 'disassoc' = 'id'
+-- 'disassoc' . 'assoc' = 'id'
+-- 'invmap' f g '.' 'disassoc' = 'disassoc' '.' 'invmap' f g
+-- @
+disassoc :: Day (Day f g) h a -> Day f (Day g h) a
+disassoc (Day (Day fb gc deb bde) hd bca abc) = Day fb (Day gc hd (,) id) f g
+  where
+    f e (d,c) =
+      bca (deb e d) c
+    g a =
+      let (b,c) = abc a
+          (d,e) = bde b
+      in (d,(e,c))
+
+-- | The monoid for 'Day' convolution on the cartesian monoidal structure is symmetric.
+--
+-- @
+-- 'invmap' f g '.' 'swapped' = 'swapped' '.' 'invmap' f g
+-- @
+swapped :: Day f g a -> Day g f a
+swapped (Day fb gc bca abc) = Day gc fb (flip bca) (\a -> let (b, c) = abc a in (c, b))
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro1' '.' 'elim1' = 'id'
+-- 'elim1' '.' 'intro1' = 'id'
+-- @
+intro1 :: f a -> Day Identity f a
+intro1 fa = Day (Identity ()) fa (\_ a -> a) ((,) ())
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro2' '.' 'elim2' = 'id'
+-- 'elim2' '.' 'intro2' = 'id'
+-- @
+intro2 :: f a -> Day f Identity a
+intro2 fa = Day fa (Identity ()) const (flip (,) ())
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro1' '.' 'elim1' = 'id'
+-- 'elim1' '.' 'intro1' = 'id'
+-- @
+elim1 :: Invariant f => Day Identity f a -> f a
+elim1 (Day (Identity b) fc bca abc) = invmap (bca b) (snd . abc) fc
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro2' '.' 'elim2' = 'id'
+-- 'elim2' '.' 'intro2' = 'id'
+-- @
+elim2 :: Invariant f => Day f Identity a -> f a
+elim2 (Day fb (Identity c) bca abc) = invmap (flip bca c) (fst . abc) fb
+
+-- | Apply a natural transformation to the left-hand side of a Day convolution.
+--
+-- This respects the naturality of the natural transformation you supplied:
+--
+-- @
+-- 'invmap' f g '.' 'trans1' fg = 'trans1' fg '.' 'invmap' f g
+-- @
+trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
+trans1 fg (Day fb hc bca abc) = Day (fg fb) hc bca abc
+
+-- | Apply a natural transformation to the right-hand side of a Day convolution.
+--
+-- This respects the naturality of the natural transformation you supplied:
+--
+-- @
+-- 'invmap' f g '.' 'trans2' fg = 'trans2' fg '.' 'invmap' f g
+-- @
+trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
+trans2 gh (Day fb gc bca abc) = Day fb (gh gc) bca abc
+
+-- | Drop the covariant part of the Day convolution.
+toContravariant :: Day f g a -> Contravariant.Day f g a
+toContravariant (Day fb gc _ abc) = Contravariant.Day fb gc abc
+
+-- | Drop the contravariant part of the Day convolution.
+toCovariant :: Day f g a -> Covariant.Day f g a
+toCovariant (Day fb gc bca _) = Covariant.Day fb gc bca