tweag / capability

Extensional capabilities and deriving combinators
BSD 3-Clause "New" or "Revised" License
213 stars 9 forks source link

Enclosing call to 'local' resets accumulated Writer value when the values share a record #93

Open byorgey opened 3 years ago

byorgey commented 3 years ago

Describe the bug Sometimes an enclosing call to 'local' for a particular Reader capability causes the accumulated value for a (conceptually unrelated) Writer capability to be reset. This only seems to happen when the concrete monad implementing the capabilities stores the values in the same record, though it's possible the record thing is a red herring.

To Reproduce

Below is the smallest example I have been able to come up with.

{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE TypeApplications           #-}

import qualified Capability.Reader    as CR
import qualified Capability.Sink      as CSk
import qualified Capability.Source    as CSc
import qualified Capability.State     as CS
import qualified Capability.Writer    as CW
import qualified Control.Monad.Reader as MR
import qualified Control.Monad.State  as MS

import           Data.Bifunctor       (second)
import           Data.Monoid          (Sum (..))
import           GHC.Generics         (Generic)

------------------------------------------------------------

-- This is the generic action we will run.  The fact that the call to 'tell' is enclosed within
-- a call to 'local' should not affect the accumulated Writer value, but as we will see,
-- sometimes it does.
act :: (CW.HasWriter "w" (Sum Int) m, CR.HasReader "r" Char m) => m ()
act = CR.local @"r" (const 'b') $ do
  CW.tell @"w" (Sum 1)
  return ()

------------------------------------------------------------

-- One concrete monad with the required capabilities, simply using mtl transformers.
newtype M1 a = M1 { unM1 :: MS.StateT (Sum Int) (MR.Reader Char) a }
  deriving (Functor, Applicative, Monad)
  deriving (CW.HasWriter "w" (Sum Int), CSk.HasSink "w" (Sum Int)) via
    (CW.WriterLog
    (CS.MonadState
    (MS.StateT (Sum Int) (MR.Reader Char))))
  deriving (CR.HasReader "r" Char, CSc.HasSource "r" Char) via
    (CR.MonadReader
    (MS.StateT (Sum Int) (MR.Reader Char)))

runM1 :: M1 a -> (a, Sum Int)
runM1 = flip MR.runReader 'a' . flip MS.runStateT mempty . unM1

------------------------------------------------------------

-- Another concrete monad with the required capabilities, this time using a state monad
-- with a single record, using the Field strategy to pick out fields for the various capabilities.

data S = S { w :: Sum Int, r :: Char }
  deriving (Eq, Ord, Show, Generic)

newtype M2 a = M2 { unM2 :: MS.State S a }
  deriving (Functor, Applicative, Monad)
  deriving (CW.HasWriter "w" (Sum Int), CSk.HasSink "w" (Sum Int)) via
    (CW.WriterLog
    (CS.Field "w" ()
    (CS.MonadState
    (MS.State S))))
  deriving (CR.HasReader "r" Char, CSc.HasSource "r" Char) via
    (CS.Field "r" ()
    (CR.ReadStatePure
    (CS.MonadState
    (MS.State S))))

runM2 :: M2 a -> (a, Sum Int)
runM2 = second w . flip MS.runState (S 0 'a') . unM2

------------------------------------------------------------

main = do
  let ((), s') = runM1 act
  print (getSum s')

  let ((), s) = runM2 act
  print (getSum s)

Expected behavior I expect the above code to print 1 twice; which concrete monad + deriving strategies we use should not change the semantics of 'act', especially when only Reader + Writer are involved (which should commute etc.) and there are no IO or exceptions anywhere to be seen.

Instead, the above code prints 1, then 0.

Environment

byorgey commented 3 years ago

Edited to add: it turns out that it works (i.e. both print 1) if we switch the order of the strategies CS.Field "r" () and CR.ReadStatePure in the derivation of HasReader for M2. I don't really understand why this should make a difference. If this is in fact expected behavior, then at the very least I think the documentation ought to be improved/clarified; I don't remember seeing anything warning me of this pitfall.

aherrmann commented 3 years ago

@byorgey Thank you for reporting! This is indeed expected behavior. I agree that this should be clarified better in the docs.

The following ordering

  deriving (CR.HasReader "r" Char, CSc.HasSource "r" Char) via
    (CS.Field "r" ()
    (CR.ReadStatePure
    (CS.MonadState
    (MS.State S))))

first creates a reader in the record S and only then focuses in on the field r in the reader's context. I.e. the underlying implementation of local will operate on the full record S and will reset the whole record at the end of local. In effect the writer and reader capability overlap on the field w of the record S.

On the other hand, if the order of Field and ReadStatePure is swapped, then the underlying implementation of local will operate only on the field r. I.e. the following is the correct ordering.

  deriving (CR.HasReader "r" Char, CSc.HasSource "r" Char) via
    (CR.ReadStatePure
    (CS.Field "r" ()
    (CS.MonadState
    (MS.State S))))
byorgey commented 3 years ago

Ah, I get it now, thanks for the explanation! I suggest... a big fat warning attached to the Field combinator? Or the ReadStatePure combinator? Or both?

I wonder if there could be a way to prevent or warn about this. It is unfortunate that there are valid ways to compose the strategies that give bogus results. You need a type system for your type-level strategy combinators... =)