  A standard informal method for analyzing the asymptotic complexity of a
program is to extract a recurrence that describes its cost in terms of the size
of its input, and then to compute a closed-form upper bound on that recurrence.
We give a formal account of that method for functional programs in a
higher-order language with let-polymorphism. The method consists of two phases.
In the first phase, a monadic translation is performed to extract a
cost-annotated version of the original program. In the second phase, the
extracted program is interpreted in a model. The key feature of this second
phase is that different models describe different notions of size. This plays
out in several ways. For example, when analyzing functions that take arguments
of inductive types, different notions of size may be appropriate depending on
the analysis. When analyzing polymorphic functions, our approach shows that one
can formally describe the notion of size of an argument in terms of the data
that is common to the notions of size for each type instance of the domain
type. We give several examples of different models that formally justify
various informal cost analyses to show the applicability of our approach.
