summaryrefslogtreecommitdiff
path: root/provider/posts
diff options
context:
space:
mode:
Diffstat (limited to 'provider/posts')
-rw-r--r--provider/posts/events/02.lhs174
1 files changed, 174 insertions, 0 deletions
diff --git a/provider/posts/events/02.lhs b/provider/posts/events/02.lhs
new file mode 100644
index 0000000..9b919a7
--- /dev/null
+++ b/provider/posts/events/02.lhs
@@ -0,0 +1,174 @@
1---
2title: "A Monad Encoding Co-Total Lists Admitting Cutoff-Rules"
3published: 2016-07-29
4tags: events
5repo: https://git.yggdrasil.li/gkleen/pub/events
6base: https://git.yggdrasil.li/gkleen/pub/events/tree/events/src/Events/Types/NDT.hs?id=9bffd435230514c00177a315bf65d9c13969f7dc
7---
8
9In [the last post](01.html) I presented `Eval`{.haskell}, a monad transformer
10for constructing a finite list of `Object`{.haskell}s together with a
11`Bool`{.haskell}-Annotation (denoting whether the `Event`{.haskell} represented
12by the `Object`{.haskell} should occur or not) while having access to arbitrary
13monadic state.
14
15The Implementation presented used [`ListT`{.haskell}][] to encapsulate
16non-determinism.
17
18Consider the following (nonfunctional[^brokenExample] for the sake of readability) example:
19
20~~~ {.haskell}
21fmap filterTime . evaluate {- This is not the `evaluate` defined in Events.Eval -} $ do
22 n <- fromFoldable [1..]
23 objPayload .= [ ("date", toJSON $ (n * 7) `addDays` (fromGregorian 2016 07 29))
24 ]
25 where
26 filterTime :: [Object] -> [Object]
27 filterTime = filter $ maybe False (\t -> qDate <= t && t <= qDate') <$> view (objPayload . key "date" . asDate)
28 qDate = fromGregorian 2016 08 01
29 qDate' = fromGregorian 2016 08 07
30~~~
31
32Due to `fromFoldable [1..]`{.haskell} this will surely never terminate yet it is obvious that the question, whether the week from 2016-08-01 to 2016-08-07 contains one of our series of events, is answerable in finite time.
33
34We would like to be able to employ constructions like the one above for the sake of convenience – it is often the case that we don´t yet know when a regularly scheduled appointment will stop taking place.
35Ensuring that our list-comprehensions always terminate is of course the halting problem – we can however employ some trickery to make rather simple constructs, like the one above, work.
36
37To do so in our concrete application we leverage the fact that, at evaluation time, we always know which `TimeRange`{.haskell} we´re interested in and can stop, given that we generate new `Event`{.haskell}s only monotonically in time, checking new `Event`{.haskell}s exactly when we encounter the first in our worldline which lies entirely after our `TimeRange`{.haskell}.
38
39> {-# LANGUAGE GADTs #-}
40> {-# LANGUAGE TupleSections #-}
41> {-# LANGUAGE ViewPatterns #-}
42> {-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
43>
44> module Events.Types.NDT
45> ( NDT
46> , foldNDT
47> , cons
48> , fromFoldable
49> ) where
50>
51> import Data.Monoid
52> import Data.Foldable (foldr)
53> import Data.Maybe
54> import Data.Either
55>
56> import Control.Applicative (Alternative)
57> import qualified Control.Applicative as Alt (Alternative(..))
58> import Control.Monad
59> import Control.Monad.Identity
60>
61> import Control.Monad.Trans
62>
63> data NDT m a where
64> NDTBind :: NDT m a -> (a -> NDT m b) -> NDT m b
65> NDTCons :: m (Maybe (a, NDT m a)) -> NDT m a
66
67`NDT m a`{.haskell} as defined above is essentially just `m [a]`{.haskell}.
68The more involved construction, reminiscent of [`Free`{.haskell}][][^usingFree] is owed to the fact that stopping to evaluate after some criterion requires that criterion be known; we´d have to save it in `NDT`{.haskell}, which is incompatible with `return`{.haskell}.
69
70What follows are some fairly straight forward and not particularly interesting instances needed essentially for making `NDT`{.haskell} into a proper monad-transformer.
71
72> instance Functor m => Functor (NDT m) where
73> fmap f (NDTBind a g) = NDTBind a (fmap f . g)
74> fmap f (NDTCons x) = NDTCons $ fmap f' x
75> where
76> f' Nothing = Nothing
77> f' (Just (x, xs)) = Just (f x, fmap f xs)
78>
79> instance Applicative m => Applicative (NDT m) where
80> pure x = NDTCons . pure $ Just (x, empty)
81> fs <*> xs = fs >>= (\f -> xs >>= pure . (f $))
82>
83> instance Applicative m => Monad (NDT m) where
84> return = pure
85> (>>=) = NDTBind
86>
87> instance Monad m => Monoid (NDT m a) where
88> mempty = empty
89> mappend (NDTCons x) y'@(NDTCons y) = NDTCons $ maybe y (\(x, xs) -> return $ Just (x, xs <> y')) =<< x
90> mappend (NDTBind x f) (NDTBind y g) = NDTBind (fmap Left x <> fmap Right y) (either f g)
91> mappend x@(NDTBind _ _) y = x <> NDTBind y return
92> mappend x y@(NDTBind _ _) = NDTBind x return <> y
93>
94> instance MonadTrans NDT where
95> lift = NDTCons . fmap Just . fmap (,empty)
96>
97> instance Monad m => Alternative (NDT m) where
98> empty = mempty
99> (<|>) = mappend
100>
101> instance Monad m => MonadPlus (NDT m) where
102> mzero = mempty
103> mplus = mappend
104>
105> instance MonadIO m => MonadIO (NDT m) where
106> liftIO = lift . liftIO
107>
108> empty :: Applicative m => NDT m a
109> empty = NDTCons $ pure Nothing
110>
111> cons :: Applicative m => a -> NDT m a -> NDT m a
112> cons x xs = NDTCons . pure $ Just (x, xs)
113>
114> fromFoldable :: (Foldable f, Monad m) => f a -> NDT m a
115> fromFoldable = foldr cons empty
116
117The evaluation function below implements the pruning behaviour described above:
118
119> foldNDT :: (Foldable f, Applicative f, Monoid (f a), Monad m) => (a -> m Bool) -> NDT m a -> m (f a)
120> -- ^ Evaluate depth-first, pruning leaves under the assumption that the selection predicate is monotonic on siblings and children
121
122Cons-cells are rather straightforward – iff the head doesn´t fulfil our criterion we ignore both it and the tail:
123
124> foldNDT sel (NDTCons mx) = do
125> mx' <- mx
126> case mx' of
127> Nothing -> return mempty
128> Just (x, mxs) -> do
129> continue <- sel x
130> case continue of
131> False -> return mempty
132> True -> (pure x <>) <$> foldNDT sel mxs
133
134This encodes pruning children of cons-cells which don´t satisfy the criterion in our tree composed of `NDTCons`{.haskell} and `NDTBind`{.haskell}.
135
136Deferred bind operations (`NDTBind`{.haskell}) are somewhat more involved.
137To make handling them easier we first squash `NDTBind`{.haskell}s such that the only children of `NDTBind`{.haskell}s are always cons-cells.
138
139> foldNDT sel (NDTBind (NDTBind x g) f) = foldNDT sel $ NDTBind x (f <=< g)
140
141The desired pruning behaviour for `NDTBind`{.haskell}s is as follows: iff evaluating the tree produced by applying `f`{.haskell} to the head of the cons-cell does not produce a valid object we discard the tail, too[^unproductivePaths].
142
143> foldNDT sel (NDTBind (NDTCons x) f) = do
144> x' <- x
145> case x' of
146> Nothing -> return mempty
147> Just (x'', xs) -> do
148> x3 <- foldNDT sel $ f x''
149> xs' <- if null x3 then return mempty else foldNDT sel (NDTBind xs f)
150> return $ x3 <> xs'
151
152Using the above the following now works:
153
154~~~ {.haskell}
155(Yaml.encode <=< evaluate predicate) $ do
156 n <- lift $ NDT.fromFoldable ([1..] :: [Integer])
157 objOccurs .= (n >= 2)
158 objPayload ?= [ ("num", Yaml.Number $ fromIntegral n)
159 ]
160 where
161 predicate :: Monad m => Maybe Yaml.Object -> m Bool
162 predicate = ordPredicate $ maybe LT (`compare` 5) . view (at "num" . asDouble)
163 ordPredicate :: Applicative m => (Object -> Ordering) -> (Maybe Object -> m Bool)
164 ordPredicate _ Nothing = pure True
165 ordPredicate f (Just (f -> o)) = pure $ o <= EQ -- View Patterns
166~~~
167
168[^brokenExample]: Neither `fromFoldable`{.haskell} nor `asDate`{.haskell} currently exist. I didn´t even bother to see whether the example typechecks.
169[^usingFree]: I am confident that `NDT`{.haskell} could be alternatively constructed using the monad-transformer version of `Free`{.haskell}: [`FreeT`{.haskell}][]
170[^unproductivePaths]: Currently this discards trees which don´t produce valid objects not because they produce invalid ones (which is our stated termination-criterion) but because they don´t produce anything at all. I´ll probably end up changing that after I find a case where that´s a problem (Care to provide one?).
171
172[`ListT`{.haskell}]: <https://hackage.haskell.org/package/list-t>
173[`Free`{.haskell}]: <https://hackage.haskell.org/package/free/docs/Control-Monad-Free.html#t:Free>
174[`FreeT`{.haskell}]: https://hackage.haskell.org/package/free/docs/Control-Monad-Trans-Free.html#t:FreeT<>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 08:34:53 +0000