Safe Haskell	None
Language	Haskell2010

Agda.Utils.Update

Synopsis

data Change a
class Monad m => MonadChange m where
runChange :: Change a -> (a, Bool)
type Updater a = a -> Change a
sharing :: Updater a -> Updater a
runUpdater :: Updater a -> a -> (a, Bool)
dirty :: Updater a
ifDirty :: MonadChange m => m a -> (a -> m b) -> (a -> m b) -> m b
class Traversable f => Updater1 f where
class Updater2 f where

Documentation

data Change a #

The Change monad.

Instances

Monad Change #
Instance details Defined in Agda.Utils.Update Methods (>>=) :: Change a -> (a -> Change b) -> Change b # (>>) :: Change a -> Change b -> Change b # return :: a -> Change a # fail :: String -> Change a #
Functor Change #
Instance details Defined in Agda.Utils.Update Methods fmap :: (a -> b) -> Change a -> Change b # (<$) :: a -> Change b -> Change a #
Applicative Change #
Instance details Defined in Agda.Utils.Update Methods pure :: a -> Change a # (<>) :: Change (a -> b) -> Change a -> Change b # liftA2 :: (a -> b -> c) -> Change a -> Change b -> Change c # (>) :: Change a -> Change b -> Change b # (<*) :: Change a -> Change b -> Change a #
MonadChange Change #
Instance details Defined in Agda.Utils.Update Methods tellDirty :: Change () # listenDirty :: Change a -> Change (a, Bool) #

class Monad m => MonadChange m where #

The class of change monads.

Minimal complete definition

tellDirty, listenDirty

Methods

tellDirty #

Arguments

:: m ()

Mark computation as having changed something.

listenDirty :: m a -> m (a, Bool) #

Instances

MonadChange Identity #	A mock change monad.
Instance details Defined in Agda.Utils.Update Methods tellDirty :: Identity () # listenDirty :: Identity a -> Identity (a, Bool) #
MonadChange Change #
Instance details Defined in Agda.Utils.Update Methods tellDirty :: Change () # listenDirty :: Change a -> Change (a, Bool) #

runChange :: Change a -> (a, Bool) #

Run a Change computation, returning result plus change flag.

type Updater a = a -> Change a #

sharing :: Updater a -> Updater a #

Replace result of updating with original input if nothing has changed.

runUpdater :: Updater a -> a -> (a, Bool) #

Blindly run an updater.

dirty :: Updater a #

Mark a computation as dirty.

ifDirty :: MonadChange m => m a -> (a -> m b) -> (a -> m b) -> m b #

class Traversable f => Updater1 f where #

Like Functor, but preserving sharing.

Methods

updater1 :: Updater a -> Updater (f a) #

updates1 #

Arguments

:: Updater a
-> Updater (f a)	= sharing . updater1

update1 :: Updater a -> EndoFun (f a) #

Instances

Updater1 [] #
Instance details Defined in Agda.Utils.Update Methods updater1 :: Updater a -> Updater [a] # updates1 :: Updater a -> Updater [a] # update1 :: Updater a -> EndoFun [a] #
Updater1 Maybe #
Instance details Defined in Agda.Utils.Update Methods updater1 :: Updater a -> Updater (Maybe a) # updates1 :: Updater a -> Updater (Maybe a) # update1 :: Updater a -> EndoFun (Maybe a) #

class Updater2 f where #

Like Bifunctor, but preserving sharing.

Minimal complete definition

updater2

Methods

updater2 :: Updater a -> Updater b -> Updater (f a b) #

updates2 :: Updater a -> Updater b -> Updater (f a b) #

update2 :: Updater a -> Updater b -> EndoFun (f a b) #

Instances

Updater2 Either #
Instance details Defined in Agda.Utils.Update Methods updater2 :: Updater a -> Updater b -> Updater (Either a b) # updates2 :: Updater a -> Updater b -> Updater (Either a b) # update2 :: Updater a -> Updater b -> EndoFun (Either a b) #
Updater2 (,) #
Instance details Defined in Agda.Utils.Update Methods updater2 :: Updater a -> Updater b -> Updater (a, b) # updates2 :: Updater a -> Updater b -> Updater (a, b) # update2 :: Updater a -> Updater b -> EndoFun (a, b) #