fromList and exponential compile time
Opened this issue · 8 comments
The following program
> module Main
> n : Nat
> n = 100
> nats : Vect Nat n
> nats = fromList [1..n]
> main : IO ()
> main = putStrLn (show (cast n))
executes in constant time in n as one would expect. Compilation, however, takes exponential time:
n user time
100 0m0.728s
200 0m1.304s
400 0m3.352s
800 0m14.737s
1600 1m30.258s
In fact, at n = 3200, compilation virtually stalls (on my laptop) after having eaten up the whole memory (8GB). Notice that replacing
> nats : Vect Nat n
> nats = fromList [1..n]
with
> nats : List Nat
> nats = [1..n]
yields constant compile times. Is it possible to construct vectors of natural numbers of length n in at most linear time (in n) ?
I think this may be to do with the Nat index - no special care is taken for the large unary numbers. I've been putting it off until there is a more general way of changing data structures, but I'll do it soon if it's getting in the way.
Still working on the new type checking implementation, which will hopefully improve lots of things. I'll get to this when it's done.
Edwin.
On 30 Jan 2013, at 14:49, nicolabotta notifications@github.com wrote:
The following program
module Main
n : Nat
n = 100nats : Vect Nat n
nats = fromList [1..n]main : IO ()
main = putStrLn (show (cast n))executes in constant time in n as one would expect. Compilation, however, takes exponential time:
n user time
100 0m0.728s
200 0m1.304s
400 0m3.352s
800 0m14.737s
1600 1m30.258sIn fact, at n = 3200, compilation virtually stalls (on my laptop) after having eaten up the whole memory (8GB). Notice that replacing
nats : Vect Nat n
nats = fromList [1..n]with
nats : List Nat
nats = [1..n]yields constant compile times. Is it possible to construct vectors of natural numbers of length n in at most linear time ?
—
Reply to this email directly or view it on GitHub.
Just a bump to say this problem still exists. Tested with Idris v0.9.13
, updated timings are below:
n | Vect | List |
---|---|---|
100 | 0m0.0646s | 0m0,669s |
200 | 0m1.763s | 0m0.676s |
400 | 0m4.159s | 0m0.660s |
800 | 0m15.353s | 0m0.657s |
1600 | 1m4.265s | 0m0.673s |
An updated program to reflect syntax changes is:
module Main
n : Nat
n = 100
nats : Vect n Nat
nats = fromList [1..n]
main : IO ()
main = putStrLn $ show $ cast n
Still there with Idris 0.9.14
Still seems to be there on 0.9.18
Updated code:
module Main
import Data.Vect
n : Nat
n = 800
nats : Vect n Nat
nats = fromList [1..n]
main : IO ()
main = putStrLn $ show n
But
> module Main
> import Data.Vect
> n : Nat
> nats : Vect (length (enumFromTo 1 n)) Nat
> nats = fromList [1..n]
> n = 100
> main : IO ()
> main = putStrLn $ show n
type checks and compiles in constant time in n
. The example shows the importance of deferring definitions in Idris programs. I have documented the problem in #2418 and #2423: in "realistic" applications, defining functions and parameters "as soon as possible" can effectively prevent type checking to terminate.
My understanding is that the current type checking approach requires Idris programs to be written in a "lazy implementation" sort of style. I do not know how to characterize such style precisely but the idea is that if a (pseudo) program P
import A, B, C, lala
f : A
g : B
h : C
h = lala f g
does type check and if a
and b
are values of type A
and B
, then a program that computes lala a b
by extending P
with suitable definitions of f
and g
should be implemented as
import A, B, C, lala
f : A
g : B
h : C
h = lala f g
g = b
f = a
rather than
import A, B, C, lala
f : A
f = a
g : B
g = b
h : C
h = lala f g
Is still an issue?
Update: it still seems like an issue on the latest version of Idris 0.11.
Ahmad Salim Al-Sibahi notifications@github.com wrote:
Is still an issue?
Sure, the problem is still there and the absolute compile time have
significantly worsened with 0.11. Here some results for
module Main
import Data.Vect
%auto_implicits off
n : Nat
n = 1600
nats : Vect n Nat
nats = fromList [1..n]
main : IO ()
main = putStrLn (show n)
n user time
100 0m6.640s
200 0m9.310s
400 0m17.712s
800 0m46.422s
1600 2m42.264s
Also, notice that freezing the definition of 'n':
module Main
import Data.Vect
%auto_implicits off
n : Nat
n = 400
%freeze n
nats : Vect n Nat
nats = fromList [1..n]
main : IO ()
main = putStrLn (show n)
yields
nicola@cirrus:~/github/SeqDecProbs/issue_reports$ time idris 172_type_checking_complexity.lidr -o 172_type_checking_complexity
172_type_checking_complexity.lidr:8:6:When checking right hand side of nats with expected type
Vect n NatType mismatch between
Vect (length (enumFromTo 1 n)) Nat (Type of fromList (enumFromTo 1 n))
and
Vect n Nat (Expected type)Specifically:
Type mismatch between
length (enumFromTo 1 n)
and
nreal 0m3.591s
user 0m3.456s
sys 0m0.136s
nicola@cirrus:~/github/SeqDecProbs/issue_reports$
which seems to be an Idris bug to me.
Thanks for looking into this issue! Ciao,
Nicola
—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub*
@nicolabotta Thanks for the update!