Ordering of Effects when calling effectual programs.

[jfdm]

The effects tutorial mentions that the specification order for a list of effects does not matter. When an effectual function is treated in isolation this is true. However, ordering does matter between effectful functions. For instance, given the following program:

module EffectfulExpressionCalculator

import Effects
import Effect.State
import Effect.Random
import Effect.Exception

data Expr = Val Integer | Var String | Add Expr Expr | Random Integer

Env : Type
Env = List (String, Integer)

eval : Expr -> { [EXCEPTION String, RND, STATE Env]} Eff Integer
eval (Val x)   = pure x
eval (Add l r) = pure $ !(eval l) + !(eval r)
eval (Random upper) =  rndInt 0 upper
eval (Var x)   = case lookup x (!get) of
  Nothing  => raise $ "No such variable " ++ x
  Just val => pure val

runEval : Env -> Expr -> Maybe Integer
runEval args expr = run (eval' expr)
  where
    eval' : Expr -> {[EXCEPTION String, STATE Env, RND]} Eff Integer
    eval' e = do
      put args
      eval e

The program does not compile as the list of effects used is 'out-of-order'.

Can Effects be fixed such that ordering does not matter across an effectual program?

[edwinb]

On 8 Jan 2015, at 14:02, Jan de Muijnck-Hughes [email protected] wrote:

Can Effects be fixed such that ordering does not matter across an effectual program?

Not easily - it would need the ‘SubList’ proof to be cleverer and be able to detect changes in ordering as well as merely missing elements, and we’d need some kind of automated proof search to spot this (it might not work with proof search, depending on how it was done).

It would be nice, at least, if we could add some kind of explicit effect permutation operator, otherwise there’s difficulty in composing effectful programs.

Now that we’ve been using Effects for a few different things, especially with resource tracking, I’m getting a better idea of what the annoyances are and what the requirements should have been if only I’d known what I was doing when I started ;). I’m playing around with a few ideas separately so we’ll see what happens…

[jfdm]

Oh yeah, I should have lead with: I knew somewhat about the 'restrictions' but wanted to make public a note about them, as I don't think we had done so yet. This issue was submitted on the back of effects library complaining about my error-ful code not working, and me not realising there were errors in my code.

[aaronc]

Has there been any progress on this issue? I see that there is still the same SubList issue in the new effects library but is there possibly a way to do "effect permutations"? I think the effect permutation option may be a preferable solution if there is a lot of complexity in improving the SubList proof - seems like that could add a lot of overhead to type-checking. If no solution exists yet in the new effects library (from reading the source I don't see one), how hard would it be to add it? Willing to take a crack at it with some guidance.

[aaronc]

By the way, I figured out a simple (albeit somewhat naive) way to solve this problem:

data SubElem : a -> List a -> Type where
  Here : SubElem a (a :: as)
  There : SubElem a as -> SubElem a (b :: as)

data SubList : List a -> List a -> Type where
  SubNil : SubList [] xs
  InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys

I checked this with proof search and it does work as expected with no additional coercion required. The issue seems to be that this would make updateWith, rebuildEnv, etc. plus the proof search O(n^2) complexity as opposed to O(n) which they are now. Since there is a trivial transformation from Here, There to Z, S and thus the natural numbers, I'm thinking that a solution for this would be to use an actual array for Env at runtime so that these just end up being trivial array lookups. In at lot of cases, people are probably only using 2-3 lists in effects so the complexity tradeoff might not be that big of a deal anyway. Another possibility is using this in a separate explicit LiftPermutateP operation until it can be made more efficient.

[edwinb]

@aaronc It might be that the simple solution you suggest is okay in practice so I'd suggest giving it a go.

I have a longer term plan to reimplement the effects library so that updateWith, rebuildEnv, etc can be run at compile time with known proofs. I haven't tried this yet mainly because early experiments suggested there wasn't that much performance benefit, and because I can't guarantee it'll actually work without some tradeoffs... nevertheless, we're still playing here so it's worth having a go and seeing what the consequences are. As you say, it seems likely that there are ways to speed it up in any case.

[aaronc]

Okay, so when I get a free moment, I'll give this refactoring a try. I'm thinking of trying to use Vect as opposed to List so that updateWith, etc. use Fin internally instead of Here and There. Is it correct that Fin is also optimized to Integer at runtime like Nat?

[david-christiansen]

Unfortunately, Finretains its unary structure at runtime.

[aaronc]

Would it be possible to optimize it or is that too complex?

By the way, I just wanted to mention that I did do a like benchmark to measure the overhead of Effects when doing actual IO. Looks like it's on the order 40% over just straight monad IO, which is in my mind acceptable for most cases. I'm imagining that with either the optimization that Edwin is talking about or just using native arrays, there would be significantly less slowdown.

[edwinb]

It's not that it's complex, just that it would be nicer to have a more
general way to do this than to introduce lots of hacks in the compiler.

I'm not sure there'd be much benefit in using Vects over Lists here
though. The main reason for using Vects is that you specifically care
about the size, whereas here we're only interested in the contents.

The overhead will depend on quite a lot of things - how much pure
computation you're doing, how many effects are available, specifically
which effects you're using, etc - but I think it is possible to more or
less eliminate it with a finally tagless approach to writing the effects
interpreter and some careful partial evaluation annotations. Some of the
overhead comes from Eff itself being a data structure that gets
interpreted, and some from the handling of the effects and looking them
up in the list. I'll have a look some day...

On 14/12/2015 17:13, Aaron Craelius wrote:

Would it be possible to optimize it or is that too complex?

By the way, I just wanted to mention that I did do a like benchmark to
measure the overhead of Effects when doing actual IO. Looks like it's on
the order 40% over just straight monad IO, which is in my mind
acceptable for most cases. I'm imagining that with either the
optimization that Edwin is talking about or just using native arrays,
there would be significantly less slowdown.

—
Reply to this email directly or view it on GitHub
#1837 (comment).

[jfdm]

Closing this issue, as it appears to have been fixed.

[andreykl]

When I trying to run this game http://docs.idris-lang.org/en/latest/effects/hangman.html I faced next thing. When type of game is

game : Eff () [MYSTERY (Running (S g) w), STDIO] [MYSTERY NotRunning, STDIO]

code is compiled. But if I change it to

game : Eff () [STDIO, MYSTERY (Running (S g) w)] [STDIO, MYSTERY NotRunning]

the compiler does not like it anymore.

It looks to me like it can be the same problem. Sorry if I've missed something. Source code is attached.
MysteryWord2.txt