From afa41a48274110460411b7b7858383fc05c5928b Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 29 Jul 2016 18:16:03 +0200 Subject: events.02 --- provider/posts/events/02.lhs | 174 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 174 insertions(+) create mode 100644 provider/posts/events/02.lhs (limited to 'provider') 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 @@ +--- +title: "A Monad Encoding Co-Total Lists Admitting Cutoff-Rules" +published: 2016-07-29 +tags: events +repo: https://git.yggdrasil.li/gkleen/pub/events +base: https://git.yggdrasil.li/gkleen/pub/events/tree/events/src/Events/Types/NDT.hs?id=9bffd435230514c00177a315bf65d9c13969f7dc +--- + +In [the last post](01.html) I presented `Eval`{.haskell}, a monad transformer +for constructing a finite list of `Object`{.haskell}s together with a +`Bool`{.haskell}-Annotation (denoting whether the `Event`{.haskell} represented +by the `Object`{.haskell} should occur or not) while having access to arbitrary +monadic state. + +The Implementation presented used [`ListT`{.haskell}][] to encapsulate +non-determinism. + +Consider the following (nonfunctional[^brokenExample] for the sake of readability) example: + +~~~ {.haskell} +fmap filterTime . evaluate {- This is not the `evaluate` defined in Events.Eval -} $ do + n <- fromFoldable [1..] + objPayload .= [ ("date", toJSON $ (n * 7) `addDays` (fromGregorian 2016 07 29)) + ] + where + filterTime :: [Object] -> [Object] + filterTime = filter $ maybe False (\t -> qDate <= t && t <= qDate') <$> view (objPayload . key "date" . asDate) + qDate = fromGregorian 2016 08 01 + qDate' = fromGregorian 2016 08 07 +~~~ + +Due 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. + +We 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. +Ensuring 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. + +To 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}. + +> {-# LANGUAGE GADTs #-} +> {-# LANGUAGE TupleSections #-} +> {-# LANGUAGE ViewPatterns #-} +> {-# LANGUAGE FlexibleContexts, FlexibleInstances #-} +> +> module Events.Types.NDT +> ( NDT +> , foldNDT +> , cons +> , fromFoldable +> ) where +> +> import Data.Monoid +> import Data.Foldable (foldr) +> import Data.Maybe +> import Data.Either +> +> import Control.Applicative (Alternative) +> import qualified Control.Applicative as Alt (Alternative(..)) +> import Control.Monad +> import Control.Monad.Identity +> +> import Control.Monad.Trans +> +> data NDT m a where +> NDTBind :: NDT m a -> (a -> NDT m b) -> NDT m b +> NDTCons :: m (Maybe (a, NDT m a)) -> NDT m a + +`NDT m a`{.haskell} as defined above is essentially just `m [a]`{.haskell}. +The 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}. + +What follows are some fairly straight forward and not particularly interesting instances needed essentially for making `NDT`{.haskell} into a proper monad-transformer. + +> instance Functor m => Functor (NDT m) where +> fmap f (NDTBind a g) = NDTBind a (fmap f . g) +> fmap f (NDTCons x) = NDTCons $ fmap f' x +> where +> f' Nothing = Nothing +> f' (Just (x, xs)) = Just (f x, fmap f xs) +> +> instance Applicative m => Applicative (NDT m) where +> pure x = NDTCons . pure $ Just (x, empty) +> fs <*> xs = fs >>= (\f -> xs >>= pure . (f $)) +> +> instance Applicative m => Monad (NDT m) where +> return = pure +> (>>=) = NDTBind +> +> instance Monad m => Monoid (NDT m a) where +> mempty = empty +> mappend (NDTCons x) y'@(NDTCons y) = NDTCons $ maybe y (\(x, xs) -> return $ Just (x, xs <> y')) =<< x +> mappend (NDTBind x f) (NDTBind y g) = NDTBind (fmap Left x <> fmap Right y) (either f g) +> mappend x@(NDTBind _ _) y = x <> NDTBind y return +> mappend x y@(NDTBind _ _) = NDTBind x return <> y +> +> instance MonadTrans NDT where +> lift = NDTCons . fmap Just . fmap (,empty) +> +> instance Monad m => Alternative (NDT m) where +> empty = mempty +> (<|>) = mappend +> +> instance Monad m => MonadPlus (NDT m) where +> mzero = mempty +> mplus = mappend +> +> instance MonadIO m => MonadIO (NDT m) where +> liftIO = lift . liftIO +> +> empty :: Applicative m => NDT m a +> empty = NDTCons $ pure Nothing +> +> cons :: Applicative m => a -> NDT m a -> NDT m a +> cons x xs = NDTCons . pure $ Just (x, xs) +> +> fromFoldable :: (Foldable f, Monad m) => f a -> NDT m a +> fromFoldable = foldr cons empty + +The evaluation function below implements the pruning behaviour described above: + +> foldNDT :: (Foldable f, Applicative f, Monoid (f a), Monad m) => (a -> m Bool) -> NDT m a -> m (f a) +> -- ^ Evaluate depth-first, pruning leaves under the assumption that the selection predicate is monotonic on siblings and children + +Cons-cells are rather straightforward – iff the head doesn´t fulfil our criterion we ignore both it and the tail: + +> foldNDT sel (NDTCons mx) = do +> mx' <- mx +> case mx' of +> Nothing -> return mempty +> Just (x, mxs) -> do +> continue <- sel x +> case continue of +> False -> return mempty +> True -> (pure x <>) <$> foldNDT sel mxs + +This encodes pruning children of cons-cells which don´t satisfy the criterion in our tree composed of `NDTCons`{.haskell} and `NDTBind`{.haskell}. + +Deferred bind operations (`NDTBind`{.haskell}) are somewhat more involved. +To make handling them easier we first squash `NDTBind`{.haskell}s such that the only children of `NDTBind`{.haskell}s are always cons-cells. + +> foldNDT sel (NDTBind (NDTBind x g) f) = foldNDT sel $ NDTBind x (f <=< g) + +The 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]. + +> foldNDT sel (NDTBind (NDTCons x) f) = do +> x' <- x +> case x' of +> Nothing -> return mempty +> Just (x'', xs) -> do +> x3 <- foldNDT sel $ f x'' +> xs' <- if null x3 then return mempty else foldNDT sel (NDTBind xs f) +> return $ x3 <> xs' + +Using the above the following now works: + +~~~ {.haskell} +(Yaml.encode <=< evaluate predicate) $ do + n <- lift $ NDT.fromFoldable ([1..] :: [Integer]) + objOccurs .= (n >= 2) + objPayload ?= [ ("num", Yaml.Number $ fromIntegral n) + ] + where + predicate :: Monad m => Maybe Yaml.Object -> m Bool + predicate = ordPredicate $ maybe LT (`compare` 5) . view (at "num" . asDouble) + ordPredicate :: Applicative m => (Object -> Ordering) -> (Maybe Object -> m Bool) + ordPredicate _ Nothing = pure True + ordPredicate f (Just (f -> o)) = pure $ o <= EQ -- View Patterns +~~~ + +[^brokenExample]: Neither `fromFoldable`{.haskell} nor `asDate`{.haskell} currently exist. I didn´t even bother to see whether the example typechecks. +[^usingFree]: I am confident that `NDT`{.haskell} could be alternatively constructed using the monad-transformer version of `Free`{.haskell}: [`FreeT`{.haskell}][] +[^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?). + +[`ListT`{.haskell}]: +[`Free`{.haskell}]: +[`FreeT`{.haskell}]: https://hackage.haskell.org/package/free/docs/Control-Monad-Trans-Free.html#t:FreeT<> -- cgit v1.2.3