diff --git a/CHANGELOG.md b/CHANGELOG.md index 2a4ea0157d..39b87098b3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -251,6 +251,9 @@ * Adds `Data.Vect.foldrImplGoLemma`. +* `Ref` interface from `Data.Ref` inherits `Monad` and was extended by a function + for value modification implemented through reading and writing by default. + #### System * Changes `getNProcessors` to return the number of online processors rather than diff --git a/libs/base/Data/Ref.idr b/libs/base/Data/Ref.idr index 7bb99cc5f5..2993018c7a 100644 --- a/libs/base/Data/Ref.idr +++ b/libs/base/Data/Ref.idr @@ -7,11 +7,21 @@ import Control.Monad.State.Interface %default total public export -interface Ref m r | m where +interface Monad m => Ref m r | m where newRef : {0 a : Type} -> a -> m (r a) readRef : {0 a : Type} -> r a -> m a writeRef : r a -> a -> m () + ||| Updates a value and returns the previous value + modifyRef : (a -> a) -> r a -> m a + modifyRef f ref = do + old <- readRef ref + writeRef ref (f old) $> old + +public export +modifyRef_ : Ref m r => (a -> a) -> r a -> m () +modifyRef_ = ignore .: modifyRef + export HasIO io => Ref io IORef where newRef = newIORef