-
Notifications
You must be signed in to change notification settings - Fork 21
/
Multi.hs
293 lines (240 loc) · 10.4 KB
/
Multi.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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
{-# LANGUAGE DeriveFunctor, GADTs, RankNTypes, TupleSections, TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables, LambdaCase #-}
-----------------------------------------------------------------------------
-- |
-- Module : Control.Selective.Multi
-- Copyright : (c) Andrey Mokhov 2018-2020
-- License : MIT (see the file LICENSE)
-- Maintainer : andrey.mokhov@gmail.com
-- Stability : experimental
--
-- This is a library for /selective applicative functors/, or just
-- /selective functors/ for short, an abstraction between applicative functors
-- and monads, introduced in this paper:
-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf.
--
-- This module defines /multi-way selective functors/, which are more efficient
-- when selecting from a large number of options. They also fully subsume the
-- 'Applicative' type class because they allow to express the notion of
-- independet effects.
--
-- This definition is inspired by the following construction by Daniel Peebles,
-- with the main difference being the added @Enumerable@ constraint:
-- https://gist.github.com/copumpkin/d5bdbc7afda54ff04049b6bdbcffb67e
--
-----------------------------------------------------------------------------
module Control.Selective.Multi (
-- * Generalised sum types
Sigma (..), inject, Zero, One (..), Two (..), Many (..), many, matchPure,
eitherToSigma, sigmaToEither,
-- * Selective functors
Some (..), Enumerable (..), Selective (..), Over (..), Under (..), select,
branch, apS, bindS,
-- * Applicative functors
ApplicativeS (..), ap, matchA,
-- * Monads
MonadS (..), bind, matchM,
-- * Generalised products and various combinators
type (~>), Pi, project, identity, compose, apply, toSigma, fromSigma, toPi,
fromPi, pairToPi, piToPair, Case (..), matchCases,
) where
import Control.Applicative ((<**>))
import Data.Functor.Identity
------------------------ Meet two friends: Sigma and Pi ------------------------
-- | A generalised sum type where @t@ stands for the type of constructor "tags".
-- Each tag has a type parameter @x@ which determines the type of the payload.
-- A 'Sigma' @t@ value therefore contains a payload whose type is not visible
-- externally but is revealed when pattern-matching on the tag.
--
-- See 'Two', 'eitherToSigma' and 'sigmaToEither' for an example.
data Sigma t where
Sigma :: t x -> x -> Sigma t
-- | An injection into a generalised sum. An alias for 'Sigma'.
inject :: t x -> x -> Sigma t
inject = Sigma
-- | A data type defining no tags. Similar to 'Data.Void.Void' but parameterised.
data Zero a where
-- | A data type with a single tag. This data type is commonly known as @Refl@,
-- see "Data.Type.Equality".
data One a b where
One :: One a a
-- | A data type with two tags 'A' and 'B' that allows us to encode the good old
-- 'Either' as 'Sigma' 'Two', where the tags 'A' and 'B' correspond to 'Left'
-- and 'Right', respectively. See 'eitherToSigma' and 'sigmaToEither' that
-- witness the isomorphism between 'Either' @a b@ and 'Sigma' @(@'Two'@ a b)@.
data Two a b c where
A :: Two a b a
B :: Two a b b
-- | Encode 'Either' into a generalised sum type.
eitherToSigma :: Either a b -> Sigma (Two a b)
eitherToSigma = \case
Left a -> inject A a
Right b -> inject B b
-- | Decode 'Either' from a generalised sum type.
sigmaToEither :: Sigma (Two a b) -> Either a b
sigmaToEither = \case
Sigma A a -> Left a
Sigma B b -> Right b
-- | A potentially uncountable collection of tags for the same unit @()@ payload.
data Many a b where
Many :: a -> Many a ()
many :: a -> Sigma (Many a)
many a = Sigma (Many a) ()
-- | Generalised pattern matching on a Sigma type using a Pi type to describe
-- how to handle each case.
--
-- This is a specialisation of 'matchCases' for @f = Identity@. We could also
-- have also given it the following type:
--
-- @
-- matchPure :: Sigma t -> (t ~> Case Identity a) -> a
-- @
--
-- We chose to simplify it by inlining '~>', 'Case' and 'Identity'.
matchPure :: Sigma t -> (forall x. t x -> x -> a) -> a
matchPure (Sigma t x) pi = pi t x
------------------------- Mutli-way selective functors -------------------------
-- | Hide the type of the payload a tag.
--
-- There is a whole library dedicated to this nice little GADT:
-- http://hackage.haskell.org/package/some.
data Some t where
Some :: t a -> Some t
-- | A class of tags that can be enumerated.
--
-- An valid instance must list every tag in the resulting list exactly once.
class Enumerable t where
enumerate :: [Some t]
instance Enumerable Zero where
enumerate = []
instance Enumerable (One a) where
enumerate = [Some One]
instance Enumerable (Two a b) where
enumerate = [Some A, Some B]
instance Enum a => Enumerable (Many a) where
enumerate = [ Some (Many x) | x <- enumFrom (toEnum 0) ]
-- | Multi-way selective functors. Given a computation that produces a value of
-- a sum type, we can 'match' it to the corresponding computation in a given
-- product type.
--
-- For greater similarity with 'matchCases', we could have given the following
-- type to 'match':
--
-- @
-- match :: f (Sigma t) -> (t ~> Case f a) -> f a
-- @
--
-- We chose to simplify it by inlining '~>' and 'Case'.
class Applicative f => Selective f where
match :: Enumerable t => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
-- | The basic "if-then" selection primitive from "Control.Selective".
select :: Selective f => f (Either a b) -> f (a -> b) -> f b
select x f = match (eitherToSigma <$> x) $ \case
A -> f
B -> pure id
-- | Choose a matching effect with 'Either'.
branch :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
branch x f g = match (eitherToSigma <$> x) $ \case
A -> f
B -> g
-- | Recover the application operator '<*>' from 'match'.
apS :: Selective f => f a -> f (a -> b) -> f b
apS x f = match (inject One <$> x) (\One -> f)
-- | A restricted version of monadic bind.
bindS :: (Enum a, Selective f) => f a -> (a -> f b) -> f b
bindS x f = match (many <$> x) (\(Many x) -> const <$> f x)
-- | Static analysis of selective functors with over-approximation.
newtype Over m a = Over { getOver :: m }
deriving (Eq, Functor, Ord, Show)
instance Monoid m => Applicative (Over m) where
pure _ = Over mempty
Over x <*> Over y = Over (mappend x y)
instance Monoid m => Selective (Over m) where
match (Over m) pi = Over (mconcat (m : ms))
where
ms = [ getOver (pi t) | Some t <- enumerate ]
-- | Static analysis of selective functors with under-approximation.
newtype Under m a = Under { getUnder :: m }
deriving (Eq, Functor, Ord, Show)
instance Monoid m => Applicative (Under m) where
pure _ = Under mempty
Under x <*> Under y = Under (mappend x y)
instance Monoid m => Selective (Under m) where
match (Under m) _ = Under m
-- | An alternative definition of applicative functors, as witnessed by 'ap' and
-- 'matchOne'. This class is almost like 'Selective' but has a strict constraint
-- on @t@.
class Functor f => ApplicativeS f where
pureA :: a -> f a
matchOne :: t ~ One x => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
-- | Recover the application operator '<*>' from 'matchOne'.
ap :: ApplicativeS f => f a -> f (a -> b) -> f b
ap x f = matchOne (inject One <$> x) (\One -> f)
-- | Every 'Applicative' is also an 'ApplicativeS'.
matchA :: (Applicative f, t ~ One x) => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
matchA x pi = (\case (Sigma One x) -> x) <$> x <**> pi One
-- | An alternative definition of monads, as witnessed by 'bind' and 'matchM'.
-- This class is almost like 'Selective' but has no the constraint on @t@.
class Applicative f => MonadS f where
matchUnconstrained :: f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
-- Adapted from the original implementation by Daniel Peebles:
-- https://gist.github.com/copumpkin/d5bdbc7afda54ff04049b6bdbcffb67e
-- | Monadic bind.
bind :: MonadS f => f a -> (a -> f b) -> f b
bind x f = matchUnconstrained (many <$> x) (\(Many x) -> const <$> f x)
-- | Every monad is a multi-way selective functor.
matchM :: Monad f => f (Sigma t) -> (forall x. t x -> f (x -> a)) -> f a
matchM sigma pi = sigma >>= \case Sigma t x -> ($x) <$> pi t
-- | A generalised product type (Pi), which holds an appropriately tagged
-- payload @u x@ for every possible tag @t x@.
--
-- Note that this looks different than the standard formulation of Pi types.
-- Maybe it's just all wrong!
--
-- See 'Two', 'pairToPi' and 'piToPair' for an example.
type (~>) t u = forall x. t x -> u x
infixl 4 ~>
-- | A product type where the payload has the type specified with the tag.
type Pi t = t ~> Identity
-- | A projection from a generalised product.
project :: t a -> Pi t -> a
project t pi = runIdentity (pi t)
-- | A trivial product type that stores nothing and simply returns the given tag
-- as the result.
identity :: t ~> t
identity = id
-- | As it turns out, one can compose such generalised products. Why not: given
-- a tag, get the payload of the first product and then pass it as input to the
-- second. This feels too trivial to be useful but is still somewhat cute.
compose :: (u ~> v) -> (t ~> u) -> (t ~> v)
compose = (.)
-- | Update a generalised sum given a generalised product that takes care of all
-- possible cases.
apply :: (t ~> u) -> Sigma t -> Sigma u
apply pi (Sigma t x) = Sigma (pi t) x
-- | Encode a value into a generalised sum type that has a single tag 'One'.
toSigma :: a -> Sigma (One a)
toSigma = inject One
-- | Decode a value from a generalised sum type that has a single tag 'One'.
fromSigma :: Sigma (One a) -> a
fromSigma (Sigma One a) = a
-- | Encode a value into a generalised product type that has a single tag 'One'.
toPi :: a -> Pi (One a)
toPi a One = Identity a
-- | Decode a value from a generalised product type that has a single tag 'One'.
fromPi :: Pi (One a) -> a
fromPi = project One
-- | Encode @(a, b)@ into a generalised product type.
pairToPi :: (a, b) -> Pi (Two a b)
pairToPi (a, b) = \case
A -> Identity a
B -> Identity b
-- | Decode @(a, b)@ from a generalised product type.
piToPair :: Pi (Two a b) -> (a, b)
piToPair pi = (project A pi, project B pi)
-- | Handler of a single case in a generalised pattern matching 'matchCases'.
newtype Case f a x = Case { handleCase :: f (x -> a) }
-- | Generalised pattern matching on a Sigma type using a Pi type to describe
-- how to handle each case.
matchCases :: Functor f => Sigma t -> (t ~> Case f a) -> f a
matchCases (Sigma t x) pi = ($x) <$> handleCase (pi t)