Structurally recursive nubBy

Oleg Grenrus
Sep 18, 2014 · 1 min read

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.

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store