fromList and exponential compile time

[nicolabotta]

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) ?

[edwinb]

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 = 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 ?

—
Reply to this email directly or view it on GitHub.

[jfdm]

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

[voila]

Still there with Idris 0.9.14

[clayrat]

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   

[nicolabotta]

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

[ahmadsalim]

Is still an issue?

Update: it still seems like an issue on the latest version of Idris 0.11.

[nicolabotta]

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 Nat

Type 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
n

real 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*