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*

[ahmadsalim]

@nicolabotta Thanks for the update!