research: computation strategies

In the paper Evaluation strategies for monadic computations, Tomas Petricek describes a typeclass

class Monad m => MonadAlias m where
  malias :: m a -> m (m a)

Instances of this class are subject to the following laws:

naturality: fmap (fmap f) . malias = malias . fmap f
associativity: fmap malias . malias = malias . malias
computationality: malias . return = return . return
identity: join . malias = id

Petricek presents three instances.

newtype Cbv m a = Cbv { runCbv :: m a }
instance Monad m => MonadAlias Cbv where
  malias m = m >>= (return . return)

newtype Cbn m a = Cbn { runCbn :: m a }
instance Monad m => MonadAlias (Cbn m) where
  malias m = return m

newtype Cbl s m a = Cbl { runCbl :: STT s m a }
instance Monad m => MonadAlias (Cbl s m) where
  malias (Cbl m) = Cbl do
    r <- newSTRef Nothing
    return $ Cbl do
      rv <- readSTRef r
      case rv of
        Nothing -> do
          v <- m
          writeSTRef r (Just v)
          return v
        Just v -> return v

Here we present a new instance, which encodes clairvoyance semantics. In the spirit of Petricek's paper, we present it as a monad transformer, which augments an existing monad. However, in order to do this, we need to take a brief detour.

0.1. detour: encoding clairvoyance semantics

We begin by considering a simpler problem: how to model clairvoyance semantics as a monad (sans transformer).

Clairvoyance semantics is nondeterministic. In Haskell, nondeterminism is usually modeled via the list monad.

newtype Cv' a = Cv' { runCv' :: [a] }

instance MonadAlias Cv' where
  malias (Cv' xs) = Cv' $ [] : [[x] | x <- xs]

Now, how do we turn this into a monad transformer? The level 1 answer is: use a list monad transformer. However, the intuitive idea of a “list monad transformer” turns out to be surprisingly difficult to pin down, and in fact the Haskell community has not reached a consensus on the best solution to this problem. To avoid upsetting anyone, we punt: rather than imposing any particular semantics for nondeterminism, we ask the user to provide their own semantics via a typeclass instance.

Now, the standard library has a typeclass that can model nondeterminism: it is MonadPlus. Here is a candidate instance.

newtype Cv'' m a = Cv'' { runCv :: m a }

instance MonadPlus m => MonadAlias (Cv'' m) where
  malias (Cv'' m) = Cv'' $ return mempty `mplus` fmap return m

We remark that, for any instance of MonadPlus, the following hold due to parametricity:

fmap return mzero = mzero (free theorem of mzero)
fmap f (m1 `mplus` m2) = fmap f m1 `mplus` fmap f m2 (free theorem of mplus)

0.1.1. naturality

fmap (fmap f) (malias m) = fmap (fmap f) . (return mzero `mplus` fmap return m) = fmap (fmap f) (return mzero) `mplus` fmap (fmap f) (fmap return m) = return (fmap f mzero) `mplus` fmap (fmap f . return) m = return (fmap f mzero) `mplus` fmap (return . f) m = return mzero `mplus` fmap return (fmap f m) = malias (fmap f m)

0.1.2. associativity

fmap malias (malias m) = fmap (\m -> return mzero `mplus` fmap return m) (return mzero `mplus` fmap return m) = fmap (\m -> return mzero `mplus` fmap return m) (return mzero) `mplus` fmap (\m -> return mzero `mplus` fmap return m) (fmap return m) = return (return mzero `mplus` fmap return mzero) `mplus` fmap (\m -> return mzero `mplus` fmap return (return m)) m = return (return mzero `mplus` return mzero) `mplus` fmap (\m -> return mzero `mplus` return (return m)) m return mzero `mplus` fmap return (return mzero `mplus` fmap return m) = malias . malias

Now, there is something interesting about the instances for Cbv, Cbn, and Cv.

Recall the notion of a thunk-force category.

In Haskell, we could encode this as a typeclass via subhask.

class Functor cat l => ThunkForce cat l where
  thunk :: cat a (l a)
  force :: cat (l a) a

The class is subject to the following laws:

fmap thunk . thunk = thunk . thunk,
thunk . fmap f = fmap (fmap f) . thunk,
force . thunk = id, and
fmap force . thunk = id.

1. relevant papers

1.1. prehistory