-
Notifications
You must be signed in to change notification settings - Fork 33
/
Day.hs
201 lines (177 loc) · 6.04 KB
/
Day.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE RankNTypes #-}
-----------------------------------------------------------------------------
-- |
-- Copyright : (C) 2014-2016 Edward Kmett
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Edward Kmett <ekmett@gmail.com>
-- Stability : provisional
-- Portability : portable
--
-- Eitan Chatav first introduced me to this construction
--
-- The Day convolution of two covariant functors is a covariant functor.
--
-- Day convolution is usually defined in terms of contravariant functors,
-- however, it just needs a monoidal category, and Hask^op is also monoidal.
--
-- Day convolution can be used to nicely describe monoidal functors as monoid
-- objects w.r.t this product.
--
-- <http://ncatlab.org/nlab/show/Day+convolution>
----------------------------------------------------------------------------
module Data.Functor.Day
( Day(..)
, day
, dap
, assoc, disassoc
, swapped
, intro1, intro2
, elim1, elim2
, trans1, trans2
) where
import Control.Applicative
import Control.Comonad
import Data.Distributive
import Data.Functor.Identity
import Data.Functor.Rep
#ifdef __GLASGOW_HASKELL__
import Data.Typeable
#endif
-- | The Day convolution of two covariant functors.
--
-- @Day f g a -> h a@ is isomorphic to @f a -> Rift g h a@
data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a)
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
deriving Typeable
#endif
-- | Construct the Day convolution
day :: f (a -> b) -> g a -> Day f g b
day fa gb = Day fa gb id
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
instance (Typeable1 f, Typeable1 g) => Typeable1 (Day f g) where
typeOf1 tfga = mkTyConApp dayTyCon [typeOf1 (fa tfga), typeOf1 (ga tfga)]
where fa :: t f (g :: * -> *) a -> f a
fa = undefined
ga :: t (f :: * -> *) g a -> g a
ga = undefined
dayTyCon :: TyCon
#if MIN_VERSION_base(4,4,0)
dayTyCon = mkTyCon3 "contravariant" "Data.Functor.Day" "Day"
#else
dayTyCon = mkTyCon "Data.Functor.Day.Day"
#endif
#endif
instance Functor (Day f g) where
fmap f (Day fb gc bca) = Day fb gc $ \b c -> f (bca b c)
instance (Applicative f, Applicative g) => Applicative (Day f g) where
pure x = Day (pure ()) (pure ()) (\_ _ -> x)
(Day fa fb u) <*> (Day gc gd v) =
Day ((,) <$> fa <*> gc) ((,) <$> fb <*> gd)
(\(a,c) (b,d) -> u a b (v c d))
instance (Representable f, Representable g) => Distributive (Day f g) where
distribute f = Day (tabulate id) (tabulate id) $ \x y -> fmap (\(Day m n o) -> o (index m x) (index n y)) f
instance (Representable f, Representable g) => Representable (Day f g) where
type Rep (Day f g) = (Rep f, Rep g)
tabulate f = Day (tabulate id) (tabulate id) (curry f)
index (Day m n o) (x,y) = o (index m x) (index n y)
instance (Comonad f, Comonad g) => Comonad (Day f g) where
extract (Day fb gc bca) = bca (extract fb) (extract gc)
duplicate (Day fb gc bca) = Day (duplicate fb) (duplicate gc) (\fb' gc' -> Day fb' gc' bca)
instance (ComonadApply f, ComonadApply g) => ComonadApply (Day f g) where
Day fa fb u <@> Day gc gd v =
Day ((,) <$> fa <@> gc) ((,) <$> fb <@> gd)
(\(a,c) (b,d) -> u a b (v c d))
instance ComonadTrans (Day f) where
lower (Day fb gc bca) = bca (extract fb) <$> gc
-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'fmap' f '.' 'assoc' = 'assoc' '.' 'fmap' f
-- @
assoc :: Day f (Day g h) a -> Day (Day f g) h a
assoc (Day fb (Day gd he dec) bca) = Day (Day fb gd (,)) he $
\ (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'
-- 'fmap' f '.' 'disassoc' = 'disassoc' '.' 'fmap' f
-- @
disassoc :: Day (Day f g) h a -> Day f (Day g h) a
disassoc (Day (Day fb gc bce) hd eda) = Day fb (Day gc hd (,)) $ \ b (c,d) ->
eda (bce b c) d
-- | The monoid for 'Day' convolution on the cartesian monoidal structure is symmetric.
--
-- @
-- 'fmap' f '.' 'swapped' = 'swapped' '.' 'fmap' f
-- @
swapped :: Day f g a -> Day g f a
swapped (Day fb gc abc) = Day gc fb (flip abc)
-- | '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
-- | 'Identity' is the unit of 'Day' convolution
--
-- @
-- 'intro1' '.' 'elim1' = 'id'
-- 'elim1' '.' 'intro1' = 'id'
-- @
elim1 :: Functor f => Day Identity f a -> f a
elim1 (Day (Identity b) fc bca) = bca b <$> fc
-- | 'Identity' is the unit of 'Day' convolution
--
-- @
-- 'intro2' '.' 'elim2' = 'id'
-- 'elim2' '.' 'intro2' = 'id'
-- @
elim2 :: Functor f => Day f Identity a -> f a
elim2 (Day fb (Identity c) bca) = flip bca c <$> fb
-- | Collapse via a monoidal functor.
--
-- @
-- 'dap' ('day' f g) = f '<*>' g
-- @
dap :: Applicative f => Day f f a -> f a
dap (Day fb fc abc) = liftA2 abc fb fc
-- | Apply a natural transformation to the left-hand side of a Day convolution.
--
-- This respects the naturality of the natural transformation you supplied:
--
-- @
-- 'fmap' f '.' 'trans1' fg = 'trans1' fg '.' 'fmap' f
-- @
trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 fg (Day fb hc bca) = Day (fg fb) hc bca
-- | Apply a natural transformation to the right-hand side of a Day convolution.
--
-- This respects the naturality of the natural transformation you supplied:
--
-- @
-- 'fmap' f '.' 'trans2' fg = 'trans2' fg '.' 'fmap' f
-- @
trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 gh (Day fb gc bca) = Day fb (gh gc) bca