The design of online learning algorithms typically aims to optimize the incurred loss or \emph{cost}, e.g., the number of classification mistakes made by the algorithm. The goal of this paper is to build a type-theoretic framework to \emph{prove} that a certain algorithm actually achieves its stated bound on the cost.

Online learning algorithms often rely on randomness, their loss functions are often defined as expectations, precise bounds are often non-polynomial (e.g., logarithmic) and proofs of optimality often rely on potential-based arguments. Accordingly, we present p$\lambda$-amor, a type-theoretic graded modal framework for analysing (expected) costs of higher-order \emph{probabilistic} programs with recursion. p$\lambda$-amor is an effect-based framework which uses graded modal types to represent potentials, cost and probability at the type level. It extends prior work ($\lambda$-amor) on cost analysis for \emph{deterministic} programs. We prove p$\lambda$-amor sound relative to a Kripke step-indexed model which relates potentials with probabilistic coupling. We use p$\lambda$-amor to prove cost bounds of several examples from online machine learning literature. Finally, we describe an extension of p$\lambda$-amor with a graded comonad and describe relationship between the different modalities.