Structurally recursive nubBy
Not so long time ago, there were a discussion on #haskell channel about whether one could write a nub using structural recursion. In fact you can.
I had time to exercise my Coq skills. There are proofs below. The equivalence of original nub and structurally recursive relies on the fact that delete and nub commute.
no obvious defects vs. obviously no defects
Structurally recursive functions obviously terminate. Convincing the termination checker about the original definition is quite simple, although not trivial.
The original nub slightly expanded is below:
It terminates, but not obviously. Recusive nubBy called with deleteBy eq x xs, not with xs. The function is total, i.e. terminates on all inputs, because the list argument is getting smaller on each recursion call. This is because deleteBy result’s length is less than or equal to parameter’s length.
Yet if we inspect structurally recursive nubBy:
This version is obviously total. The argument to recursive call of nubBy is the part of the function argment. And if we pretend that input is always finite, the function will always terminate, by definition.
The two versions have only slight difference. I don’t know why base package developers choose non-structural one. Maybe it has better performance, yet both functions have quadratic complexity. Especially if deleteFirstBy is used in structurally recursive version, it shouldn’t perform too badly.
deleteFirst x (nub xs) ≡ nub (delete x xs)
The equivalence above is quite obvious, but wasn’t that easy to prove. Yet below is the mechanised proof.
