Mapping a List over a rank 2 function has O(n^2) time complexity

[stefan-hoeck]

I found the following (reduced to a minimal example) when mapping over the functor wrapped in a free monad:

Steps to Reproduce

Run the following program:

mapK : {0 f,g : _} -> (forall x . f x -> g x) -> List (f a) -> List (g a)
mapK fun [] = []
mapK fun (x :: xs) = fun x :: mapK {f} {g} fun xs

main : IO ()
main = printLn . length $ mapK {f = Maybe} toList vals
  where vals : List (Maybe Bits32)
        vals = map Just [1 .. 100000]

Expected Behavior

Runs in less than a second (same as the standard map).

Observed Behavior

Takes more than 10 seconds on my machine.

The reason can best be explained, when looking at the code generated by the JS backends (the Scheme backends have the same issue):

function Test_mapK($0, $1) {
 switch($1.h) {
  case 0: return {h: 0};
  case undefined: return {a1: $0(undefined)($1.a1), a2: Test_mapK($b => $0(undefined), $1.a2)};
 }
}

As can be seen, instead of passing the function argument $0 as is in the recursive call, a new function with an erased argument is being created ($b => $0(undefined)). This leads to k applications of undefined in the k-th iteration, hence the observed quadratic time complexity.

[stefan-hoeck]

Quick update: If I use an explicit erased argument, the program runs instantaneously.

mapK : {0 f,g : _} -> ((0 x : Type) -> f x -> g x) -> List (f a) -> List (g a)
mapK fun [] = []
mapK fun (x :: xs) = fun _ x :: mapK {f} {g} fun xs

main : IO ()
main = printLn . length $ mapK {f = Maybe} (\_ => toList) vals
  where vals : List (Maybe Bits32)
        vals = map Just [1 .. 100000]

[iacore]

Why is mapK so complicated? Will this work?

mapK : (f -> g) -> List f -> List g
mapK fun [] = []
mapK fun (x :: xs) = fun x :: mapK fun xs

main : IO ()
main = printLn . length $ abb
  where vals : List (Maybe Bits32)
        vals = (map Just [1 .. 100000]) ++ [Nothing, Nothing]
        abb = mapK toList vals

[gallais]

We have similarly annoying issues with implicit lambdas being eagerly eta-expanded in #660