  A central method for analyzing the asymptotic complexity of a functional
program is to extract and then solve a recurrence that expresses evaluation
cost in terms of input size. The relevant notion of input size is often
specific to a datatype, with measures including the length of a list, the
maximum element in a list, and the height of a tree. In this work, we give a
formal account of the extraction of cost and size recurrences from higher-order
functional programs over inductive datatypes. Our approach allows a wide range
of programmer-specified notions of size, and ensures that the extracted
recurrences correctly predict evaluation cost. To extract a recurrence from a
program, we first make costs explicit by applying a monadic translation from
the source language to a complexity language, and then abstract datatype values
as sizes. Size abstraction can be done semantically, working in models of the
complexity language, or syntactically, by adding rules to a preorder judgement.
We give several different models of the complexity language, which support
different notions of size. Additionally, we prove by a logical relations
argument that recurrences extracted by this process are upper bounds for
evaluation cost; the proof is entirely syntactic and therefore applies to all
of the models we consider.
