forked from mroman42/vitrea
/
CategoriesInstances.hs
201 lines (157 loc) · 7.33 KB
/
CategoriesInstances.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
{-|
Module : Categories, Instances
Description : Instances of constrained categories
Copyright : (c) Mario Román, 2020
License : GPL-3
Maintainer : mromang08@gmail.com
Stability : experimental
Portability : POSIX
Provides instances for the definition of category constrained on the objects.
-}
module CategoriesInstances where
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Void
import Control.Monad
import Categories
-- Instances for some common categories
class Any x
instance Any x
instance Category Any (->) where
unit = \x -> x
comp = \g f x -> g (f x)
newtype Nat f g = Nat { nat :: forall x . f x -> g x }
instance Category Functor Nat where
unit = Nat id
comp (Nat h) (Nat k) = Nat (h . k)
instance Category Applicative Nat where
unit = unit @Functor
comp = comp @Functor
instance Category Traversable Nat where
unit = unit @Functor
comp = comp @Functor
newtype App f a = App { getApp :: f a }
instance Bifunctor Any (->) Any (->) Any (->) (,) where
bimap f g (x,y) = (f x , g y)
instance Bifunctor Functor Nat Functor Nat Functor Nat Compose where
bimap (Nat h) (Nat k) = Nat (Compose . fmap k . h . getCompose)
instance Bifunctor Applicative Nat Applicative Nat Applicative Nat Compose where
bimap = bimap @Functor @Nat @Functor @Nat @Functor @Nat @Compose
instance Bifunctor Traversable Nat Traversable Nat Traversable Nat Compose where
bimap = bimap @Functor @Nat @Functor @Nat @Functor @Nat @Compose
instance Bifunctor Any (->) Any (->) Any (->) Either where
bimap f _ (Left x) = Left (f x)
bimap _ g (Right x) = Right (g x)
instance Bifunctor Functor Nat Any (->) Any (->) App where
bimap (Nat h) f = App . fmap f . h . getApp
instance Bifunctor Applicative Nat Any (->) Any (->) App where
bimap = bimap @Functor @Nat @Any @(->) @Any @(->) @App
instance Bifunctor Traversable Nat Any (->) Any (->) App where
bimap = bimap @Functor @Nat @Any @(->) @Any @(->) @App
instance MonoidalCategory Any (->) (,) () where
alpha (x,(y,z)) = ((x,y),z)
alphainv ((x,y),z) = (x,(y,z))
lambda (x,_) = x
lambdainv x = (x,())
rho (_,x) = x
rhoinv x = ((),x)
instance MonoidalCategory Any (->) Either Void where
alpha = either (Left . Left) (either (Left . Right) Right)
alphainv = either (either Left (Right . Left)) (Right . Right)
lambda = either (\x -> x) absurd
lambdainv = Left
rho = either absurd (\x -> x)
rhoinv = Right
instance MonoidalCategory Functor Nat Compose Identity where
alpha = Nat (Compose . Compose . fmap getCompose . getCompose)
alphainv = Nat (Compose . fmap Compose . getCompose . getCompose)
lambda = Nat (fmap runIdentity . getCompose)
lambdainv = Nat (Compose . fmap Identity)
rho = Nat (runIdentity . getCompose)
rhoinv = Nat (Compose . Identity)
instance MonoidalCategory Applicative Nat Compose Identity where
alpha = alpha @Functor @Nat @Compose @Identity
alphainv = alphainv @Functor @Nat @Compose @Identity
lambda = lambda @Functor @Nat @Compose @Identity
lambdainv = lambdainv @Functor @Nat @Compose @Identity
rho = rho @Functor @Nat @Compose @Identity
rhoinv = rhoinv @Functor @Nat @Compose @Identity
instance MonoidalCategory Traversable Nat Compose Identity where
alpha = alpha @Functor @Nat @Compose @Identity
alphainv = alphainv @Functor @Nat @Compose @Identity
lambda = lambda @Functor @Nat @Compose @Identity
lambdainv = lambdainv @Functor @Nat @Compose @Identity
rho = rho @Functor @Nat @Compose @Identity
rhoinv = rhoinv @Functor @Nat @Compose @Identity
instance MonoidalAction Functor Nat Compose Identity Any (->) App where
unitor = runIdentity . getApp
unitorinv = App . Identity
multiplicator = App . Compose . fmap getApp . getApp
multiplicatorinv = App . fmap App . getCompose . getApp
instance MonoidalAction Applicative Nat Compose Identity Any (->) App where
unitor = unitor @Functor @Nat @Compose @Identity @Any @(->) @App
unitorinv = unitorinv @Functor @Nat @Compose @Identity @Any @(->) @App
multiplicator = multiplicator @Functor @Nat @Compose @Identity @Any @(->) @App
multiplicatorinv = multiplicatorinv @Functor @Nat @Compose @Identity @Any @(->) @App
instance MonoidalAction Traversable Nat Compose Identity Any (->) App where
unitor = unitor @Functor @Nat @Compose @Identity @Any @(->) @App
unitorinv = unitorinv @Functor @Nat @Compose @Identity @Any @(->) @App
multiplicator = multiplicator @Functor @Nat @Compose @Identity @Any @(->) @App
multiplicatorinv = multiplicatorinv @Functor @Nat @Compose @Identity @Any @(->) @App
instance (MonoidalCategory objm m o i) => MonoidalAction objm m o i objm m o where
unitor = rho @objm @m
unitorinv = rhoinv @objm @m
multiplicator = alpha @objm @m @o @i
multiplicatorinv = alphainv @objm @m @o @i
class (Monad m) => Algebra m a where
algebra :: m a -> a
instance (Monad m) => Algebra m (m a) where
algebra = join
instance (Monad m) => Category (Algebra m) (->) where
unit = unit @Any
comp = comp @Any
instance (Monad m) => Bifunctor (Algebra m) (->) (Algebra m) (->) (Algebra m) (->) (,) where
bimap = bimap @Any @(->) @Any @(->) @Any @(->)
instance (Monad m) => Algebra m () where
algebra _ = ()
instance (Monad m, Algebra m x, Algebra m y) => Algebra m (x,y) where
algebra u = (algebra $ fmap fst u, algebra $ fmap snd u)
instance (Monad m) => MonoidalCategory (Algebra m) (->) (,) () where
alpha = alpha @Any @(->) @(,) @()
alphainv = alphainv @Any @(->) @(,) @()
lambda = lambda @Any @(->) @(,) @()
lambdainv = lambdainv @Any @(->) @(,) @()
rho = rho @Any @(->) @(,) @()
rhoinv = rhoinv @Any @(->) @(,) @()
instance (Monad m) => Bifunctor (Algebra m) (->) Any (->) Any (->) (,) where
bimap = bimap @Any @(->) @Any @(->) @Any @(->) @(,)
instance (Monad m) => MonoidalAction (Algebra m) (->) (,) () Any (->) (,) where
unitor = unitor @Any @(->) @(,) @() @Any @(->) @(,)
unitorinv = unitorinv @Any @(->) @(,) @() @Any @(->) @(,)
multiplicator = multiplicator @Any @(->) @(,) @() @Any @(->) @(,)
multiplicatorinv = multiplicatorinv @Any @(->) @(,) @() @Any @(->) @(,)
-- FunLists are the free applicatives over Store functors. We
-- implement the type-changing FunList.
data FunList s a b = Done b | More s (FunList s a (a -> b))
instance Functor (FunList s a) where
fmap f (Done b) = Done (f b)
fmap f (More s l) = More s (fmap (f .) l)
-- This instance declaration can be seen, for instance, in Pickering,
-- Gibbons, Wu.
instance Applicative (FunList s a) where
pure = Done
(Done f) <*> l' = fmap f l'
(More x l) <*> l' = More x (fmap flip l <*> l')
-- Kleisli categories of free algebras. The morphisms Kl(a,b) are
-- written in the usual (a -> m b) form.
newtype Kleisli m a b = Kleisli { getKleisli :: (a -> m b) }
instance (Monad m) => Category Any (Kleisli m) where
unit = Kleisli return
comp (Kleisli g) (Kleisli f) = Kleisli (join . fmap g . f)
instance (Monad m) => Bifunctor Any (->) Any (Kleisli m) Any (Kleisli m) (,) where
bimap f (Kleisli g) = Kleisli (\(x,y) -> fmap ((,) (f x)) (g y))
instance (Monad m) => MonoidalAction Any (->) (,) () Any (Kleisli m) (,) where
unitor = unitor @Any @(->) @(,) @() @Any @(Kleisli m) @(,)
unitorinv = unitorinv @Any @(->) @(,) @() @Any @(Kleisli m) @(,)
multiplicator = multiplicator @Any @(->) @(,) @() @Any @(Kleisli m) @(,)
multiplicatorinv = multiplicatorinv @Any @(->) @(,) @() @Any @(Kleisli m) @(,)