List concatenation ((++) :: [a] -> [a] -> [a])

Append the second list after the first. For a finite left list of length $n$, consuming the concatenation costs $\Theta (n)$ to copy its spine and can share the second argument. Repeatedly appending large left lists can cause quadratic time complexity; difference lists make concatenation into function composition.

Concatenating the initial list prefix accepted by a predicate with the remaining list suffix reconstructs the input, provided every test reached before the first false result terminates. Prove the finite case by structural induction: a true test copies the head, and a false test returns the untouched list suffix. An undefined reached test is an obstruction because reconstruction loses an exposed cons cell. An infinite all-true list prefix can still reconstruct the input, since list concatenation never demands its second argument there.