aspiwack / haskell-benign

A library for benign effects in Haskell
MIT License
20 stars 0 forks source link

Consider introducing an `Evaluation` monad #17

Open aspiwack opened 1 year ago

aspiwack commented 1 year ago

The Evaluation (possible alternative name Strategy) monad would have a single primitive evaluate (the same as the IO monad. In fact, under the hood, it would possibly be the IO monad, though maybe there is a pure solution).

The idea would be that the Evaluation monad would support a (safe) run :: Evaluation a -> a function, contrary to the IO monad.

It may be less clunky to use than the Thunk/extractEval approach that I currently use. On the other hand, it may make it harder to deal with strict types.


Something that I would love to get out of this is to be able to unify somehow the classes Eval and EvalIO (the latter being introduced by #16 ). But the difficulty remains that EvalIO (IO a) must hold and Eval (IO a) absolutely mustn't. How can these be conciliated?

aspiwack commented 1 year ago

Here's a plan, albeit a half-baked one still.

We can make a class

class Monad m => MonadEvaluate m where
  evaluate :: a -> m a

Evidently, IO is an instance (and so is the Evaluation monad from the original message).

Now, if we have something that can be purely evaluated, then we can define it's eval function polymorphically eval :: MonadEvaluate m => a -> m (Result a).

To be able to do that, we can generalise the Eval class:

class MonadEvaluate m => EvalIn m a where
  type Result a
  eval :: a -> m (Result a)

type EvalIO = EvalIn IO
type Eval = EvalIn Evaluation

(mostly equivalently, we could have type Eval a = forall m. MonadEvaluate m => EvalIn m a, but quantified constraints don't like type synonyms, so it's probably not going to work. On the other hand we ca define data Evaluation = MkEvaluation (forall m. MonadEvaluate m => EvalIn m a); I don't know whether it's a good idea).

In the pure function, we would require Eval, in impure function EvalIO = EvalIn IO.


My big question, based on these thoughts, is whether we can replace

withAlteringIO :: EvalIO a => … -> a -> IO (Result a)

with

withAlteringM :: EvalIn m a => … a -> m (Result a)

Which, together with an instance

instance EvalIn m (m a)

would allow for convenient composition of several withAlteringM like we do with withAlteringIO.

One thing that is slightly unsatisfactory, is that we would use an unsafePerformIO in the definition of withAlteringM, so at type IO, we would do a return . unsafePerformIO, this is a little silly. We could extend MonadEvaluate with an (unsafe) function IO a -> m a, which would be an improvement, but we would still need NOINLINE on withAlteringM. It's a little icky. Nothing really terrible.

An idea: if we actually define the Evaluation monad as a newtype around IO. Then we don't need NOINLINE when calling the unsafe function. The NOINLINE would only occur on the runEvaluation :: Evaluation a -> a function. Maybe that'll work for me.


A smaller question (which may be irrelevant according to previous paragraph) is whether it's possible to define the Evaluation function in a way that Evaluation a is isomorphic to a (at least when restricted to total terms). The current implementation of the Eval class may provide a solution

class Eval a where
  data Thunk a
  type Result a

  -- | Evaluating the @eval x@ thunk executes the evaluation strategy.
  eval :: a -> Thunk a

  extractEval :: Thunk a -> Result a

newtype Seq a = Seq a
  deriving anyclass (EvalIO)

instance SeqIsEval a => Eval (Seq a) where
  newtype Thunk (Seq a) = SeqThunk a
  type Result (Seq a) = a
  eval (Seq x) = SeqThunk x
  extractEval (SeqThunk x) = x

This suggest that, maybe data Evaluation a = Evaluation a could work (compare to newtype Identity a = Identity a). With return = Evaluation and evaluate x = x `seq` Evaluation x).

aspiwack commented 1 year ago

An issue of allowing IO computations with local state, is that IO computations can call myThreadId, since I silently create threads each time we modify the local state, myThreadId will return silly values. Worse, maybe, if someone calls forkIO or async inside that computation, they will lose the local state (an issue that context addresses by providing its own forking primitives).