Order-independent implementation of SubList for Effects

[aaronc]

This is my first attempt at solving #1837 - Ordering of Effects when calling effectual programs

This implementation has what seems to me to be unnecessary complexity due to needing to figure out how to get the Handler eff m type class resolution to be inferred through-out the Env re-ordering code - envElem and dropEnv is a good example of this. I think that possibly someone else could make this a bit cleaner, but it works in my tests.

[aaronc]

I apologize - I typed in the wrong issue ref number for some reason (brain fart...). This should ref issue #1837

[jfdm]

Cheers for looking at this, is it possible for you to add your tests to the test suite demonstrating the new functionality.

[aaronc]

So, I have some tests that I'm almost ready to add. I ran into another issue however. dropEnv as I've defined it isn't total. There is a missing case clause for [] (InList i is). Of course this case can't exist because the a non-empty list can't be a sub-list of an empty list, but I haven't figured out how to tell Idris this. To get my code working, I've had to add a %assert_total directive for dropEnv. I'd like to tell Idris this case is impossible but it won't accept that as is. Any thoughts on how to solve this?

[edwinb]

Thanks for this!

I'd like to play around before I merge into master, though, since I'm about to do a release and I'd like to make sure it works on the effects code I have which really exercises this. In the mean time, if you get around to fixing the conflicts before I do that would be most helpful.

[edwinb]

As far as I can tell, this works very well, thanks! Sorry for taking so long to sort out the merge conflicts, but it's done now and I've updated it for the latest export rules and so on.

[aaronc]

Oh looks like you merged in the Dockerfile I created too. Was that intentional? This Dockerfile is useful and could be auto-built by dockerhub so that people can quickly pull a docker image for building idris code... That may actually be the quickest way to get an Idris repl up an running on a new machine now that I think of it. If you have docker installed you can try it like this: docker run -it aaroncr/idris-dev idris - instant idris repl, no installation required.

Also, melvar had showed me how to avoid the %assert_total in dropEnv but I didn't get around to pushing the fix yet. Also, he pointed out that EffElem can be safely replaced by Elem from Data.List.

[edwinb]

I fixed the dropEnv in a different patch. Didn't notice the Dockerfile
though...

I did notice about Elem too, but that can be fixed easily enough.

On 17/03/2016 16:21, Aaron Craelius wrote:

Oh looks like you merged in the Dockerfile I created too. Was that intentional? This Dockerfile is useful and could be auto-built by dockerhub so that people can quickly pull a docker image for building idris code... That may actually be the quickest way to get an Idris repl up an running on a new machine now that I think of it. If you have docker installed you can try it like this: docker run -it aaroncr/idris-dev idris - instant idris repl, no installation required.

Also, melvar had showed me how to avoid the %assert_total in dropEnv but I didn't get around to pushing the fix yet. Also, he pointed out that EffElem can be safely replaced by Elem from Data.List.

---

You are receiving this because you modified the open/close state.
Reply to this email directly or view it on GitHub:
#2864 (comment)