dirty-haskell.org: A Monad Encoding Co-Total Lists Admitting Cutoff-Rules

It's not crazy — it's having fun with types.

In the last post I presented Eval, a monad transformer for constructing a finite list of Objects together with a Bool-Annotation (denoting whether the Event represented by the Object should occur or not) while having access to arbitrary monadic state.

The Implementation presented used ListT to encapsulate non-determinism.

Consider the following (nonfunctional1 for the sake of readability) example:

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..] 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 we´re interested in and can stop, given that we generate new Events only monotonically in time, checking new Events exactly when we encounter the first in our worldline which lies entirely after our TimeRange.

> {-# 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 as defined above is essentially just m [a]. The more involved construction, reminiscent of Free2 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, which is incompatible with return.

What follows are some fairly straight forward and not particularly interesting instances needed essentially for making NDT 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 and NDTBind.

Deferred bind operations (NDTBind) are somewhat more involved. To make handling them easier we first squash NDTBinds such that the only children of NDTBinds are always cons-cells.

> foldNDT sel (NDTBind (NDTBind x g) f) = foldNDT sel $ NDTBind x (f <=< g)

The desired pruning behaviour for NDTBinds is as follows: iff evaluating the tree produced by applying f to the head of the cons-cell does not produce a valid object we discard the tail, too3.

> 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:

(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

  1. Neither fromFoldable nor asDate currently exist. I didn´t even bother to see whether the example typechecks.↩

  2. I am confident that NDT could be alternatively constructed using the monad-transformer version of Free: FreeT↩

  3. 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?).↩