-
Notifications
You must be signed in to change notification settings - Fork 58
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unexpected run-time complexity #71
Comments
At least at compile time, it's almost certainly down to the |
Right, all test were done by running
The correspondent Idris 1 program was
also tested with |
You can use :c at the REPL just like in Idris 1, as long as you have chez scheme installed. Nobody has implemented -o yet. There seems to be a couple of weird things going on. Firstly, there's more effort than there should be going into type checking, but also there's a segfault in compilation that happens in a surprising place. I'll try to look into it, because this sort of thing is not supposed to happen with the way Idris 2 is set up, but I should also go on holiday at some point so it might be a while unless someone else is enthusiastic about poking around the core. |
Hmmm, chez scheme is installed but
|
@nicolabotta: Currently the parser expects an "unqualified name" for the filename, thus it is not allowed to have @edwinb: I can look into implementing |
@chrrasmussen: thanks! I can confirm the problem is a type checking one. Once an executable is generated, the run-time seems to be constant in @edwinb: thanks but do not forget your holiday! As it turns out, for
|
So I've worked out what's going on - interestingly it's fast in Idris 1 because there it reduces everything to normal form, and it's slow in Idris 2 because it's only computing what's needed to build the proof. This sounds good, until you look at the suspended computation and see that it's shared everywhere throughout the Fin that gets built. It's erased at run time, so if you get that far, it runs pretty much instantly (I succeeded up to N=320 after a bit of tweaking at least). I don't know exactly the right way to proceed, but I have a long train journey tomorrow so I'll have a poke. The question is why sharing gets broken - it may be to do with auto implicit search or maybe something a bit deeper. Or it might be that for the moment we need a different way of implementing fromInteger for Fin. |
I'll play around with a different implementation of |
It should be linear in N but I'm having trouble testing that experimentally because it erases things predictably in Idris 2 so I'm only really seeing the start up cost of the chez runtime! |
It seems plausible that the auto implicit in
and
type checks and run in Idris 1 and 2 in the following times:
and
Type checking is much slower in Idris 2 but generating and running the executable takes about the same time as in Idris 1. If we uncomment/comment
In Idris 2, type checking takes hours or longer and, as we have seen, compiling yields segfaults even for smaller values of |
I've found that chicken takes quite a while to generate code from the scheme that Idris passes to it. It also generates code that is quite a bit slower than Idris 1 generates. If you can, I'd recommend giving it a go with Chez (though I seem to remember there was some reason this didn't work in the past). Possibly using the racket code generator would also give better performance. There's something about the scheme we generate that chicken just doesn't like... Anyway - I've been poking around this one a bit. I think I now understand what's going on, and it is unfortunately hard to solve, because in the end, Fin doesn't scale well at all. There are things we can do to improve evaluation time (I've tried a few which have helped), but even if we do, we'll just hit a performance problem a bit later. Whatever happens, converting to Fin is linear time at best (and the indices mean it's probably quadratic or worse when computing a normal form). Really for this kind of problem what we need is a proper O(1) implementation of arrays with compile time bounds checking. This is achievable with QTT, but there isn't an easy answer. |
In the specific example, with chicken it takes about twice as long as with chez to compile the
The
|
It seems that indexing
This is perhaps disappointing but still far better than using the orginal What kind of conclusions can we infer from this example? Is this an irrelevant, pathological case? Is it an issue that we are likely to encounter at application-level code? |
The program
type checks and executes in more than quadratic time in
N
in idris 2:For "large" values of
N
, it segfaults. In idris 1, the correspondent program also does not run in linear time, but it does not segfault and is faster. What is the expected complexity of the program? Shouldn't building the vector and reading its last component be linear operations in
N
?The text was updated successfully, but these errors were encountered: