| Abstract: |
"Theorems for Free!" (Wadler, FPCA'89)
is a slogan for a technique that allows to
derive statements about functions just from their types. So far, the statements
considered have always had a purely extensional flavor: statements relating the
value semantics of program expressions, but not statements relating their runtime
(or other) cost. Here we study an extension of the technique that allows precisely
statements of the latter flavor, by deriving quantitative theorems for free. After
developing the theory, we walk through a number of example derivations. Probably
none of the statements derived in those simple examples will be particularly
surprising to most readers, but what is maybe surprising, and at the very least
novel, is that there is a general technique for obtaining such results on a
quantitative level in a principled way. Moreover, there is good potential to bring
that technique to bear on more complex examples as well. We turn our attention to
short-cut fusion (Gill et al., FPCA'93)
in particular.
|