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
|
{-# LANGUAGE Rank2Types
, MultiParamTypeClasses
, FunctionalDependencies
, UndecidableInstances #-}
-------------------------------------------------------------------------------------------
-- |
-- Module : Data.Functor.Adjunction
-- Copyright : 2008-2011 Edward Kmett
-- License : BSD
--
-- Maintainer : Edward Kmett <ekmett@gmail.com>
-- Stability : experimental
-- Portability : rank 2 types, MPTCs, fundeps
--
-------------------------------------------------------------------------------------------
module Data.Functor.Adjunction
( Adjunction(..)
, tabulateAdjunction
, indexAdjunction
, zipR, unzipR
, unabsurdL, absurdL
, cozipL, uncozipL
, extractL, duplicateL
, splitL, unsplitL
) where
import Control.Applicative
import Control.Arrow ((&&&), (|||))
import Control.Monad.Instances ()
import Control.Monad.Trans.Identity
import Control.Monad.Trans.Reader
import Control.Monad.Trans.Writer
import Control.Comonad.Trans.Env
import Control.Comonad.Trans.Traced
import Data.Functor.Identity
import Data.Functor.Compose
import Data.Functor.Representable
import Data.Void
-- | An adjunction between Hask and Hask.
--
-- Minimal definition: both 'unit' and 'counit' or both 'leftAdjunct'
-- and 'rightAdjunct', subject to the constraints imposed by the
-- default definitions that the following laws should hold.
--
-- > unit = leftAdjunct id
-- > counit = rightAdjunct id
-- > leftAdjunct f = fmap f . unit
-- > rightAdjunct f = counit . fmap f
--
-- Any implementation is required to ensure that 'leftAdjunct' and
-- 'rightAdjunct' witness an isomorphism from @Nat (f a, b)@ to
-- @Nat (a, g b)@
--
-- > rightAdjunct unit = id
-- > leftAdjunct counit = id
class (Functor f, Representable u) =>
Adjunction f u | f -> u, u -> f where
unit :: a -> u (f a)
counit :: f (u a) -> a
leftAdjunct :: (f a -> b) -> a -> u b
rightAdjunct :: (a -> u b) -> f a -> b
unit = leftAdjunct id
counit = rightAdjunct id
leftAdjunct f = fmap f . unit
rightAdjunct f = counit . fmap f
-- | Every right adjoint is representable by its left adjoint
-- applied to a unit element
--
-- Use this definition and the primitives in
-- Data.Functor.Representable to meet the requirements of the
-- superclasses of Representable.
tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
tabulateAdjunction f = leftAdjunct f ()
-- | This definition admits a default definition for the
-- 'index' method of 'Index", one of the superclasses of
-- Representable.
indexAdjunction :: Adjunction f u => u b -> f a -> b
indexAdjunction = rightAdjunct . const
splitL :: Adjunction f u => f a -> (a, f ())
splitL = rightAdjunct (flip leftAdjunct () . (,))
unsplitL :: Functor f => a -> f () -> f a
unsplitL = (<$)
extractL :: Adjunction f u => f a -> a
extractL = fst . splitL
duplicateL :: Adjunction f u => f a -> f (f a)
duplicateL as = as <$ as
-- | A right adjoint functor admits an intrinsic
-- notion of zipping
zipR :: Adjunction f u => (u a, u b) -> u (a, b)
zipR = leftAdjunct (rightAdjunct fst &&& rightAdjunct snd)
-- | Every functor in Haskell permits unzipping
unzipR :: Functor u => u (a, b) -> (u a, u b)
unzipR = fmap fst &&& fmap snd
absurdL :: Void -> f Void
absurdL = absurd
-- | A left adjoint must be inhabited, or we can derive bottom.
unabsurdL :: Adjunction f u => f Void -> Void
unabsurdL = rightAdjunct absurd
-- | And a left adjoint must be inhabited by exactly one element
cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
cozipL = rightAdjunct (leftAdjunct Left ||| leftAdjunct Right)
-- | Every functor in Haskell permits 'uncozipping'
uncozipL :: Functor f => Either (f a) (f b) -> f (Either a b)
uncozipL = fmap Left ||| fmap Right
-- Requires deprecated Impredicative types
-- limitR :: Adjunction f u => (forall a. u a) -> u (forall a. a)
-- limitR = leftAdjunct (rightAdjunct (\(x :: forall a. a) -> x))
instance Adjunction ((,) e) ((->) e) where
leftAdjunct f a e = f (e, a)
rightAdjunct f ~(e, a) = f a e
instance Adjunction Identity Identity where
leftAdjunct f = Identity . f . Identity
rightAdjunct f = runIdentity . f . runIdentity
instance Adjunction f g =>
Adjunction (IdentityT f) (IdentityT g) where
unit = IdentityT . leftAdjunct IdentityT
counit = rightAdjunct runIdentityT . runIdentityT
instance Adjunction w m =>
Adjunction (EnvT e w) (ReaderT e m) where
unit = ReaderT . flip fmap EnvT . flip leftAdjunct
counit (EnvT e w) = rightAdjunct (flip runReaderT e) w
instance Adjunction m w =>
Adjunction (WriterT s m) (TracedT s w) where
unit = TracedT . leftAdjunct (\ma s -> WriterT (fmap (\a -> (a, s)) ma))
counit = rightAdjunct (\(t, s) -> ($s) <$> runTracedT t) . runWriterT
instance (Adjunction f g, Adjunction f' g') =>
Adjunction (Compose f' f) (Compose g g') where
unit = Compose . leftAdjunct (leftAdjunct Compose)
counit = rightAdjunct (rightAdjunct getCompose) . getCompose
|
