Add staticEff/toEff
Sometimes when working with effectful programs which change state, you
need to give the intermediate effect state explicitly, which can be
inconvenient with (>>=) especially, so these functions make it easier.
toEff is especially useful with 'case' blocks which branch the effects then
rejoin after.
commitcc99207a3e60445048fb8888b2652cf2b51afd7c
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 30 May 2014, 18:57 (12 years ago)
parent8e2f681
CHANGELOG+1
@@ -25,6 +25,7 @@ New in 0.9.13:
2525* Extend :addclause to add instance bodies as well as definitions
2626* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
2727* Move foldl into Foldable so it can be overridden.
28+* Experimental :search REPL command for finding functions by type
2829
2930Internal changes
3031
libs/effects/Effects.idr+14
@@ -166,6 +166,20 @@ data Eff : (m : Type -> Type)
166166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
167167(>>=) = ebind
168168
169+-- namespace SimpleBind
170+-- (>>=) : Eff m a xs (\v => xs) ->
171+-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
172+-- (>>=) = ebind
173+
174+||| Run a subprogram which results in an effect state the same as the input.
175+staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)
176+staticEff = id
177+
178+||| Explicitly give the expected set of result effects for an effectful
179+||| operation.
180+toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')
181+toEff xs' = id
182+
169183return : a -> Eff m a xs (\v => xs)
170184return x = value x
171185