I show that in cases where the two programs and their inputs are closely related, relational cost analysis is superior to non-relational analysis both in terms of precision and simplicity. Specifically, I show that a refinement type and effect system provides a precise and compact mechanism for proving the relative cost of two programs.
The idea behind relational cost analysis can be extended to other nontrivial domains. In particular, I show that relational cost analysis can be adapted to prove upper bounds on the update costs of incremental programs.
Finally, I briefly present a bidirectional technique to typecheck relational cost bounds.