The definition of "basic step", which includes arithmetic on unbounded integers, is suspicious. And I don't see any attempt at establishing an upper bound on the size of coefficients. I wouldn't be surprised if they grow exponentially.
I sometimes wonder if using logarithms would be more appropriate in most cases. Then we can simply add up the numbers as one "would expect".
We could choose the base to be ~2.7048138 such that 1% regular growth corresponds to 1% logarithmic growth. For low percentages they would mostly agree. But +40% would become +34% while -40% would become -51%, thus making the combined effect more apparent.
I work on developing better tools for solving computational geometry problems robustly and efficiently, so I got quite excited when this paper first appeared.
However, while the type theoretic developments based on Abstract Stone Duality is interesting, they mostly ignore the problem of efficiency by simply representing every real number as a Dedekind cut. Thus, it doesn't scale without significant advances in compiling real arithmetic. A problem I'm working on presently, but it might take a few years...
One important aspect of programming with functors is the ability to quantify over them, i.e. higher-kinded types. This is crucial for building reusable components on the functor-level of abstraction.
In modern OOP this would amount to quantifying over interfaces which is typically not even possible in those languages.
Discrimination runs in linear time not in the number of items but in the total size of the data. If you have n items each of size k it takes O(kn). Conventional sorting often assumes that you can compare keys of size k in constant time and therefore gets O(n lg n) but a more honest analysis would yield O(kn log n) for (say) merge sort.
All orderings must be specified as a reduction to a primitive order using the fact that if you have an equivalence relation on some type A and a reduction f : B -> A then you have an equivalence on B defined by x = y when f(x) = f(y).
Now, take the rational numbers. For the usual binary comparison we can simply define (a/b) < (c/d) as ad < cb. It's not obvious how to express this as a reduction to a primitive ordering (the answer is to compute the continued fraction).
In fact, I'm not aware of any systematic way of deriving discrimination-suitable orderings from binary predicates -- it might be an open research problem, as far as I am aware.
I'm happy to see this excellent paper mentioned. Fritz Henglein (the author) was my thesis supervisor last year, and I worked on developing some of his ideas further.
In particular, I generalised discrimination (and added a touch of linear algebra) to devise a simple multi-way join algorithm that computes the join of any number of relations in optimal time (in a specific technical sense). Such results have been obtained recently, but only with far more complicated algorithms.
Alas, the fully general proof of optimality eludes us, so nothing has been published yet.