Severe efficiency problems in Idris, Haskell fine

[nicolabotta]

The program

> module Main

> %default total
> %access public export
> %auto_implicits off

> J : Type -> Type -> Type
> J R X = (X -> R) -> X

> K : Type -> Type -> Type
> K R X = (X -> R) -> R

> overline : {X, R : Type} -> J R X -> K R X
> overline e p = p (e p)

> otimes : {X, R : Type} -> J R X -> (X -> J R (List X)) -> J R (List X)  
> otimes e f p = x :: xs where
>   x   =    e (\ x' => overline (f x') (\ xs' => p (x' :: xs')))
>   xs  =  f x (\ xs' => p (x :: xs'))

> partial
> bigotimes : {X, R : Type} -> List (List X -> J R X) -> J R (List X)
> bigotimes       []   =  \ p => []
> bigotimes (e :: es)  =  (e []) `otimes` (\x => bigotimes [\ xs => d (x :: xs) | d <- es])

> partial
> argsup : {X : Type} -> (xs : List X) -> J Int X
> argsup (x :: Nil) p = x
> argsup (x :: x' :: xs) p = if p x < p x' then argsup (x' :: xs) p else argsup (x :: xs) p

> partial
> e : List Int -> J Int Int
> e _ = argsup [0..1]

> p : List Int -> Int
> p = sum 

> partial
> main : IO ()
> main = do putStr ("bigotimes (replicate 3 e) p = "
>                   ++
>                   show (bigotimes (replicate 3 e) p) ++ "\n")

can be compiled under 1.3.0-git:02bfaac6f with idris -O3 --warnreach --allow-capitalized-pattern-variables Main.lidr -o Main. The executable runs more or less instantaneosly:

$ time ./Main
bigotimes (replicate 3 e) p = [1, 1, 1]

real    0m0.009s
user    0m0.008s
sys 0m0.000s

But replacing line 33 with

> e _ = argsup [0..3]

yields execution times of about 3 seconds

$ time ./Main
bigotimes (replicate 3 e) p = [3, 3, 3]

real    0m3.113s
user    0m3.092s
sys 0m0.020s

and

> e _ = argsup [0..5]

execution times of about one and a half minutes

$ time ./Main
bigotimes (replicate 3 e) p = [5, 5, 5]

real    1m23.630s
user    1m23.520s
sys 0m0.024s

Running with

> e _ = argsup [0..7]

takes about 13 minutes

$ time ./Main
bigotimes (replicate 3 e) p = [7, 7, 7]

real    13m16.190s
user    13m15.468s
sys 0m0.148s

and if one increases the length of the argsup argument above about 10, the Idris program keeps on running for days, perhaps months! Notice that the corresponding Haskell program

> module Main where

> type J r x = (x -> r) -> x

> type K r x = (x -> r) -> r

> overline :: J r x -> K r x
> overline e p = p (e p)

> otimes :: J r x -> (x -> J r [x]) -> J r [x]
> otimes e f p = x : xs where
>   x   =    e (\ x' -> overline (f x') (\ xs' -> p (x' : xs')))
>   xs  =  f x (\ xs' -> p (x : xs'))

> bigotimes ::  [[x] -> J r x] -> J r [x]
> bigotimes       []   =  \ p -> []
> bigotimes (e : es)   =  (e []) `otimes` (\x -> bigotimes [\ xs -> d (x : xs) | d <- es])

> argsup :: [x] -> J Int x
> argsup (x : []) p = x
> argsup (x : x' : xs) p = if p x < p x' then argsup (x' : xs) p else argsup (x : xs) p

> e :: [Int] -> J Int Int
> e _ = argsup [0..1]

> p :: [Int] -> Int
> p = sum

> main :: IO ()
> main = do putStr ("bigotimes (replicate 3 e) p = "
>                   ++
>                   show (bigotimes (replicate 3 e) p) ++ "\n")

executes in slightly more than quadratic time in the lengths of the argsup argument for lengths up to 400:

$ time ./Main 
bigotimes (replicate 3 e) p = [99,99,99]

real    0m0.511s
user    0m0.496s
sys 0m0.008s
$ make
ghc -O3  Main.lhs -o Main
[1 of 1] Compiling Main             ( Main.lhs, Main.o )
Linking Main ...
$ time ./Main 
bigotimes (replicate 3 e) p = [199,199,199]

real    0m4.193s
user    0m4.164s
sys 0m0.020s
$ make
ghc -O3  Main.lhs -o Main
[1 of 1] Compiling Main             ( Main.lhs, Main.o )
Linking Main ...
$ time ./Main 
bigotimes (replicate 3 e) p = [399,399,399]

real    0m34.397s
user    0m34.056s
sys 0m0.264s

What do you expect to be the complexity of the computation in the length of the argsup argument? What is going wrong in the Idris execution? Is there a way to get acceptable execution times in Idris? Or to understand what makes the Idris code so inefficient? Thanks, Nicola

[nicolabotta]

As it turns out, the problem is the implementation of otimes. Replacing

> otimes e f p = x :: xs where
>   x   =    e (\ x' => overline (f x') (\ xs' => p (x' :: xs')))
>   xs  =  f x (\ xs' => p (x :: xs'))

with

> otimes e f p = let x  = e (\ x' => overline (f x') (\ xs' => p (x' :: xs'))) in
>                let xs = f x (\ xs' => p (x :: xs')) in
>                x :: xs

makes the code run in times comparable with those of the Haskell implementation. The problem is that, with where, the computation of x is delegated to a global function that is then called three times: two times in the computation of xs and one time in the computation of x :: xs.

Thanks to Edwin for spotting the problem! I am not going to close the issue for the time being as I am not sure that this is the intended behavior.