From 77d60ec2b76eca35ef2254361ff0df3bb6a25903 Mon Sep 17 00:00:00 2001 From: Brian McKenna Date: Sun, 11 Feb 2018 23:18:47 +1100 Subject: [PATCH] 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 | 2 + src/Data/Functor/Invariant/Day.hs | 150 ++++++++++++++++++++++++++++++ 2 files changed, 152 insertions(+) create mode 100644 src/Data/Functor/Invariant/Day.hs diff --git a/kan-extensions.cabal b/kan-extensions.cabal index caf6edf..99805ca 100644 --- a/kan-extensions.cabal +++ b/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 diff --git a/src/Data/Functor/Invariant/Day.hs b/src/Data/Functor/Invariant/Day.hs new file mode 100644 index 0000000..9f6a623 --- /dev/null +++ b/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 +-- Stability : provisional +-- Portability : portable +-- +-- The Day convolution of two invariant functors is an invariant +-- functor. +-- +-- +---------------------------------------------------------------------------- + +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