# 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.