Comments (16)
Comment by edwinb
Monday Aug 05, 2019 at 18:48 GMT
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.
from idris2.
Yes, will open a PR then.
from idris2.
Comment by edwinb
Thursday Aug 01, 2019 at 18:00 GMT
At least at compile time, it's almost certainly down to the fromInteger
which has to compute a proof that the Fin is within bounds. This is a compile time thing. Are you compiling and executing things too? And if so, what happens? Can you be precise about where these numbers come from?
from idris2.
Comment by nicolabotta
Thursday Aug 01, 2019 at 18:18 GMT
Right, all test were done by running time idris2 --exec main Linear.idr
. For instance, for N = 20
:
nicola@lt561:~/gitlab/botta/Idris2Libs/tests$ time idris2 --exec main Linear.idr
xs(20) = 20
real 0m0.876s
user 0m0.850s
sys 0m0.024s
nicola@lt561:~/gitlab/botta/Idris2Libs/tests$
The correspondent Idris 1 program was
> import Data.Fin
> import Data.Vect
> tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
> tail f = f . FS
> toVectFun : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
> toVectFun {n = Z} _ = Nil
> toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
> N : Nat
> N = 1600
> xs : Vect (S N) Nat
> xs = toVectFun {n = S N} finToNat
> main : IO ()
> main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (toIntegerNat N)) xs))
also tested with time idris --exec main Linear.lidr
. How can I just generate an executable in Idris 2?
from idris2.
Comment by edwinb
Thursday Aug 01, 2019 at 18:23 GMT
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.
from idris2.
Comment by nicolabotta
Thursday Aug 01, 2019 at 18:41 GMT
Hmmm, chez scheme is installed but :c
does not seem to work as in idris 1:
nicola@lt561:~/gitlab/botta/Idris2Libs/tests$ idris2 Linear.idr
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :c linear2.exe
(interactive):1:11--1:15:'.' is not a prefix operator
Main>
from idris2.
Comment by chrrasmussen
Thursday Aug 01, 2019 at 19:12 GMT
@nicolabotta: :c
is used like this: :c linear main
, where linear
is the filename and main
is the entrypoint function. The Chez codegen will then generate a linear.ss
file and a linear.so
file.
Currently the parser expects an "unqualified name" for the filename, thus it is not allowed to have .
in the filename (ref. https://github.com/edwinb/Idris2/blob/master/src/Idris/Parser.idr#L1422).
@edwinb: I can look into implementing -o
this weekend.
from idris2.
Comment by nicolabotta
Thursday Aug 01, 2019 at 19:57 GMT
@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 N
in idris 2.
@edwinb: thanks but do not forget your holiday!
As it turns out, for N = 160
, idris 2 type checking terminates (after a few minutes!) but :c linear main
aborts with a segfault. Thus, indeed, there seem to be two issues here:
-
The type checking time that is neither constant nor linear in
N
. -
The segfault problem.
from idris2.
Comment by edwinb
Thursday Aug 01, 2019 at 23:14 GMT
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.
from idris2.
Comment by nicolabotta
Friday Aug 02, 2019 at 05:51 GMT
I'll play around with a different implementation of fromInteger
and report. I am actually more worried about the Idris 1 run-time behavior. Shouldn't it be linear in N
?
from idris2.
Comment by edwinb
Friday Aug 02, 2019 at 07:39 GMT
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!
from idris2.
Comment by nicolabotta
Friday Aug 02, 2019 at 11:08 GMT
It seems plausible that the auto implicit in fromInteger
is the culprit for the segfaults in Idris 2. The codes
> import Data.Fin
> import Data.Vect
> tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
> tail f = f . FS
> toVectFun : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
> toVectFun {n = Z} _ = Nil
> toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
> N : Nat
> N = 800
> xs : Vect (S N) Nat
> xs = toVectFun {n = S N} finToNat
> fromNat : {n : Nat} -> Nat -> Fin n
> fromNat {n = S m} Z = FZ
> fromNat {n = S m} (S i) = if i < m then FS (fromNat i) else last
> main : IO ()
> -- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (toIntegerNat N)) xs))
> main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromNat N) xs))
and
import Data.Fin
import Data.Vect
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = 800
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
fromNat : {n : Nat} -> Nat -> Fin n
fromNat {n = S m} Z = FZ
fromNat {n = S m} (S i) = if i < m then FS (fromNat i) else last
main : IO ()
-- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromNat N) xs))
type checks and run in Idris 1 and 2 in the following times:
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris Linear.lidr -o linear
real 0m7.838s
user 0m7.060s
sys 0m0.496s
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time ./linear
xs(800) = 800
real 0m0.117s
user 0m0.112s
sys 0m0.004s
and
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris2 --cg chicken Linear.idr
1/1: Building Linear (Linear.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :c linear2 main
linear2 written
Main> :q
Bye for now!
real 0m45.559s
user 0m41.444s
sys 0m0.316s
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time ./linear2
xs(800) = 800
real 0m0.308s
user 0m0.292s
sys 0m0.008s
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 main
so as to use fromInteger
the situation gets much worse for type checking and compiling in Idris 1:
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris Linear.lidr -o linear
real 2m12.576s
user 1m37.984s
sys 0m10.548s
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time ./linear
xs(800) = 800
real 0m0.077s
user 0m0.072s
sys 0m0.000s
In Idris 2, type checking takes hours or longer and, as we have seen, compiling yields segfaults even for smaller values of N
.
from idris2.
Comment by nicolabotta
Wednesday Aug 07, 2019 at 05:01 GMT
In the specific example, with chicken it takes about twice as long as with chez to compile the fromNat
case:
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris2 --cg chicken Linear.idr
1/1: Building Linear (Linear.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :c linear2 main
linear2 written
Main> :q
Bye for now!
real 0m39.584s
user 0m34.919s
sys 0m0.254s
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris2 Linear.idr
1/1: Building Linear (Linear.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :c linear2 main
compiling linear2.ss with output to linear2.so
linear2 written
Main> :q
Bye for now!
real 0m19.038s
user 0m15.835s
sys 0m0.081s
The fromInteger . natToInteger
case, however, fails to terminate both with chicken and with chez. With chez, for instance:
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris2 Linear.idr
1/1: Building Linear (Linear.idr)
Uncaught error: Error in TTC file: End of buffer when reading String
real 583m54.436s
user 583m31.545s
sys 0m17.752s
nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$
from idris2.
Comment by nicolabotta
Wednesday Aug 21, 2019 at 09:27 GMT
It seems that indexing Vect n a
with bounded natural numbers instead of Fin n
s gives a nearly perfect quadratic complexity:
import Data.Fin
import Data.Vect
import Data.Nat
LTB : Nat -> Type
LTB b = DPair Nat (\ n => LT n b)
idx : {n : Nat} -> Vect n alpha -> LTB n -> alpha
idx {n = Z} Nil (MkDPair i prf) = absurd prf
idx {n = S m} (x :: xs) (MkDPair Z prf) = x
idx {n = S m} (x :: xs) (MkDPair (S k) (LTESucc prf)) = idx xs (MkDPair k prf)
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = 100
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
lemma : (n : Nat) -> LT n (S n)
lemma Z = LTESucc LTEZero
lemma (S m) = LTESucc (lemma m)
main : IO ()
-- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (idx xs (MkDPair N (lemma N))))
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$ time idris2 --exec main 71_run_time_complexity.idr
xs(100) = 100
real 0m0.999s
user 0m0.958s
sys 0m0.040s
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$ time idris2 --exec main 71_run_time_complexity.idr
xs(200) = 200
real 0m2.557s
user 0m2.540s
sys 0m0.017s
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$ time idris2 --exec main 71_run_time_complexity.idr
xs(400) = 400
real 0m8.460s
user 0m8.423s
sys 0m0.037s
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$ time idris2 --exec main 71_run_time_complexity.idr
xs(800) = 800
real 0m33.110s
user 0m33.032s
sys 0m0.070s
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$ time idris2 --exec main 71_run_time_complexity.idr
xs(1600) = 1600
real 2m16.461s
user 2m16.224s
sys 0m0.112s
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$
This is perhaps disappointing but still far better than using the orginal index
function and converting Nat
s to Fin n
s: this segfaults already for N = 100
!
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?
from idris2.
Situation is way better currently, got the following times and no segfault:
N = 20, user time = 373.77 millis
N = 40, user time = 405.00 millis
N = 80, user time = 414.71 millis
N = 160, user time = 987.71 millis
N = 320, user time = 4.63 secs
Edit: should be closed?
from idris2.
Edit: should be closed?
Can we add a test case to the idris2/perf
category?
from idris2.
Related Issues (20)
- Make output of ide-mode `:interpret` consistent to always return consistent datatype (String)
- Inconsistent error message when finding more than one implementation of an interface
- Reconstructing a (structurally smaller) aggregate from pattern-matched components trips up the totality checker HOT 8
- Support type annotations on LHS of a monadic bind `<-` HOT 9
- Incremental compilation includes some but not all metas
- Test idris2/reflection/reflection024 fails due to not accounting for locales
- Nested code blocks are ignored in literate markdown HOT 1
- Bootstrap with Racket error: `raco: Unrecognized command: exe` HOT 3
- Why quoted values are EmptyFC?
- Totality checker inconsistency when using Inf HOT 2
- Case split doesn't detect cases when working inside a namespace
- Regression in #3328, compilation now hangs sometimes HOT 2
- Syntax for Dictionary types HOT 7
- Erased type-casing function seen as total when it's not
- Case split causes my function to no longer be covering HOT 4
- Searching of `auto` inside pairs introduces ambiguity error between actually same things HOT 3
- Holes at unerased quantity produce bad code
- Parsing Performance & Maintainability. HOT 4
- Names received using as-matching are not reduced under `case`
- Evaluation of partial functions during conversion HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris2.