Languages with potential: Types & recurrences for formal amortized analysis