git.iko.soy/Idris-dev
on master help sign in
Add staticEff/toEff
cc99207Edwin Brady
CHANGELOG+1
compare with master
unifiedsplit
@@ -25,6 +25,7 @@ New in 0.9.13:
25* Extend :addclause to add instance bodies as well as definitions
25* Extend :addclause to add instance bodies as well as definitions
26* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
26* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
27* Move foldl into Foldable so it can be overridden.
27* Move foldl into Foldable so it can be overridden.
28+* Experimental :search REPL command for finding functions by type
28
29
29Internal changes
30Internal changes
30
31
libs/effects/Effects.idr+14
@@ -166,6 +166,20 @@ data Eff : (m : Type -> Type)
166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
167(>>=) = ebind
167(>>=) = ebind
168
168
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+
169return : a -> Eff m a xs (\v => xs)
183return : a -> Eff m a xs (\v => xs)
170return x = value x
184return x = value x
171
185