A *timed computation* \(\mathrm{TimeM}\, T\, \alpha \) records a return value in \(\alpha \) together with an accumulated time cost in \(T\). Suppose \(T\) carries a distinguished zero element, and let \(\mathrm{pure}\, a\) denote the timed computation that returns \(a\) at zero cost. Then for every \(a \in \alpha \), the return value of \(\mathrm{pure}\, a\) is \(a\).

Consider computations that carry both a return value and an accumulated time cost drawn from a type \(T\) equipped with an addition, and let the monadic bind of such a computation \(m\) with a continuation \(f\) run \(m\), pass its return value to \(f\), and add the two costs. Then the return value of \(m \mathbin {\gt \! \! \gt \! \! =} f\) equals the return value of \(f\) applied to the return value of \(m\).

A value of type \(\mathrm{TimeM}\ T\ \alpha \) is a timed computation, consisting of a return value \(\mathrm{ret} \in \alpha \) together with an accumulated time cost in \(T\), and \(\mathrm{TimeM}\ T\) carries the functor structure that acts on the return value. For any function \(f : \alpha \to \beta \) and any timed computation \(x\) of type \(\mathrm{TimeM}\ T\ \alpha \), the return value of the mapped computation obtained by applying \(f\) through this functor to \(x\) equals \(f(\mathrm{ret}(x))\).

Model a computation that tracks its running time as a pair consisting of a return value and an accumulated time cost drawn from a type \(T\) equipped with an addition. Given such a computation \(x\), with return value in a type \(\alpha \), and a thunk \(y\) producing a second such computation with return value in a type \(\beta \), the right-sequencing of \(x\) and \(y\) — which runs \(x\), then \(y()\), combines their time costs, and discards the value of \(x\) — has return value equal to that of \(y()\).

A value of type \(\mathrm{TimeM}\, T\, \alpha \) is a computation carrying both a return value in \(\alpha \) and an accumulated cost in \(T\); write \(\mathrm{ret}\) for the return-value component. Suppose \(T\) is equipped with an addition, let \(x\) be such a computation of type \(\mathrm{TimeM}\, T\, \alpha \), and let \(y\) be a (thunked) computation of type \(\mathrm{TimeM}\, T\, \beta \). Then the left-sequencing \(x \mathbin {\lt {*}} y\), which runs both computations and adds their costs but keeps only the value produced by \(x\), has return value \(\mathrm{ret}(x \mathbin {\lt {*}} y) = \mathrm{ret}(x)\).

Regard a value of type \(\mathrm{TimeM}\, T\, \alpha \) as a timed computation, carrying both a return value in \(\alpha \) and an accumulated time cost in \(T\), and suppose \(T\) is equipped with an addition, so that such computations may be sequenced. Let \(f\) be a timed computation whose return value is a function \(\alpha \to \beta \), and let \(x\) be a thunk, that is, a function on the one-point type producing a timed computation with return value in \(\alpha \). Then the return value of the computation obtained by sequencing \(f\) with \(x\) equals the return value of \(f\) applied to the return value of the computation \(x(\, )\) obtained by forcing the thunk.

Model a computation as a pair consisting of a return value in a type \(\alpha \) together with an accumulated time cost drawn from a type \(T\) equipped with an addition operation; write \(\mathrm{ret}(\cdot )\) for the returned value and \(\mathrm{time}(\cdot )\) for the cost. Given such a computation \(m\) and a continuation \(f\) that assigns to each value of type \(\alpha \) a further computation returning a value of type \(\beta \), the sequential composition \(m \gg \! = f\) (run \(m\), then run \(f\) on its result) has cost equal to the cost of \(m\) plus the cost of running \(f\) on the value returned by \(m\):

A cost-annotated computation over a type \(T\) of costs and a value type \(\alpha \) consists of a return value in \(\alpha \) together with an accumulated time cost in \(T\). Suppose \(T\) carries a distinguished zero element \(0\). Then for every value \(a \in \alpha \), the trivial computation that returns \(a\) (the \(\mathrm{pure}\) computation) has time cost \(0\).

A timed computation over a cost type \(T\) is a pair consisting of a return value in \(\alpha \) and an accumulated time cost in \(T\). For any function \(f\colon \alpha \to \beta \) and any timed computation \(x\), applying \(f\) to the return value of \(x\) (leaving the value’s type as \(\beta \)) yields a timed computation whose time cost equals that of \(x\).

A *timed computation* over an additive cost type \(T\) records a return value together with an accumulated cost in \(T\); write \(\mathrm{time}(c) \in T\) for the cost of such a computation \(c\). Let \(x\) be a timed computation and let \(y\) be a thunk that, when forced, produces a timed computation. The right-sequencing \(x \mathbin {*\gt } y\), which performs \(x\) and then \(y()\) and returns the value of \(y()\), has time cost

Fix a type \(T\) carrying an addition, and regard a value of type \(\mathrm{TimeM}\, T\, \alpha \) as a computation that records both a return value in \(\alpha \) and an accumulated time cost \(\mathrm{time}\in T\). Given such a computation \(x\) and a thunked computation \(y\colon \mathrm{Unit}\to \mathrm{TimeM}\, T\, \beta \), the left-sequencing \(x \mathbin {\lt *} y\) — which runs both but keeps the return value of \(x\) — has time cost \(\mathrm{time}(x) + \mathrm{time}\bigl(y()\bigr)\), the sum of the two individual costs.

Let \(T\) be a type equipped with an addition, and regard a value of \(\mathrm{TimeM}\, T\, \alpha \) as a computation that returns a result in \(\alpha \) together with an accumulated time cost \(\mathrm{time}(\cdot ) \in T\). Given a computation \(f\) of a function \(\alpha \to \beta \) and a thunked computation \(x\) of an argument in \(\alpha \), the applicative sequencing \(f \mathbin {\langle *\rangle } x\), which applies the computed function to the computed argument, has time cost \(\mathrm{time}(f) + \mathrm{time}(x())\), the sum of the cost of \(f\) and the cost of forcing and running \(x\).

For any time cost \(c\), the return value of the computation \(\mathrm{tick}\, c\) is the trivial (unit) value.

For any time cost \(c\), the operation \(\mathrm{tick}\, c\) — which charges \(c\) units of time and returns the trivial value — records accumulated time exactly \(c\).

Let \(a\), \(b\), \(c\) be elements of a linearly ordered set. Then the value returned by the timed computation \(\mathrm{median3}(a,b,c)\) is a median of \(a\), \(b\), and \(c\): it is one of the three inputs occupying the middle position in the order, so that at least one of the remaining two values is \(\le \) it and at least one is \(\ge \) it.

Let \(a\), \(b\), \(c\) be elements of a linear order, and let \(\mathrm{median3}(a,b,c)\) be the timed computation that returns a median of the three by a nested sequence of comparisons, charging one unit of time for each comparison performed. Then the recorded time cost of \(\mathrm{median3}(a,b,c)\) is at most \(3\); that is, the computation performs at most three comparisons.

Let \(\alpha \) be a linearly ordered type and let \(\mathit{xs}\) be a finite list of elements of \(\alpha \). Then \(\mathit{xs}\) is sorted — in the sense that each element is at most the one following it — if and only if \(\mathit{xs}\) is a chain for the relation \(\le \), meaning that \(x \le y\) holds for every pair of consecutive entries \(x, y\) of \(\mathit{xs}\).

Let \(\mathit{xs}\) be a finite list over a linearly ordered set. Then \(\mathit{xs}\) is sorted in the adjacent-pairs sense if and only if it is sorted in the usual pairwise sense with respect to \(\le \); that is, if and only if \(x_i \le x_j\) for every pair of indices \(i \lt j\).

Let \(\alpha \) be a linearly ordered type. For every \(x \in \alpha \) and every finite list \(\mathit{xs}\) over \(\alpha \), the value returned by the timed insertion of \(x\) into \(\mathit{xs}\) (discarding the accumulated time cost) coincides with the ordinary ordered insertion of \(x\) into \(\mathit{xs}\) with respect to the order \(\le \): the list obtained by placing \(x\) immediately before the first entry \(y\) of \(\mathit{xs}\) satisfying \(x \le y\), and at the end if no such entry exists.

Let \(\alpha \) be a linearly ordered type and let \(xs\) be a list of elements of \(\alpha \). The value returned by the timed insertion sort of \(xs\) equals the ordinary insertion sort of \(xs\) taken with respect to the order relation \(\le \).

Let \(\alpha \) be a linearly ordered type, let \(x \in \alpha \), and let \(xs\) be a finite list of elements of \(\alpha \). The return value of the timed ordered insertion of \(x\) into \(xs\) is a list of length \(\left\lvert xs\right\rvert + 1\).

For every list \(\mathit{xs}\) over a linearly ordered type, the output list produced by the timed insertion sort of \(\mathit{xs}\) has the same length as \(\mathit{xs}\).

Let \(\alpha \) be a linearly ordered type, let \(x \in \alpha \), and let \(xs\) be a finite list of elements of \(\alpha \). Then the list obtained by timed ordered insertion of \(x\) into \(xs\) is a permutation of \(x :: xs\), the list with \(x\) prepended to \(xs\).

Let \(\alpha \) be a linearly ordered type, let \(x \in \alpha \), and let \(\mathit{xs}\) be a sorted list over \(\alpha \). Then the list returned by the timed ordered insertion of \(x\) into \(\mathit{xs}\) — the return value of that computation, discarding its time cost — is again sorted.

Let \(\alpha \) be a linearly ordered type and let \(\mathit{xs}\) be a list of elements of \(\alpha \). Then the list produced by insertion sort applied to \(\mathit{xs}\) is a permutation of \(\mathit{xs}\).

Let \(\alpha \) be a linearly ordered type. For every list \(\mathit{xs}\) of elements of \(\alpha \), the list returned by the timed insertion sort of \(\mathit{xs}\) is sorted.

Let \(\alpha \) be a linearly ordered type and let \(\mathit{xs}\) be a finite list of elements of \(\alpha \). Then the list returned by the timed insertion sort applied to \(\mathit{xs}\) is sorted, and it is a permutation of \(\mathit{xs}\).

Let \(\alpha \) carry a linear order, and for \(x \in \alpha \) and a list \(\mathit{xs}\) over \(\alpha \) let \(\mathrm{insert}(x, \mathit{xs})\) denote the ordered insertion that scans \(\mathit{xs}\) from the front, spending one unit of time on each element compared, until it reaches the first entry not smaller than \(x\). Then the time cost incurred by \(\mathrm{insert}(x, \mathit{xs})\) is at most the length of \(\mathit{xs}\).

Let \(\alpha \) be a linearly ordered type and let \(xs\) be a finite list of elements of \(\alpha \). Running the timed insertion sort on \(xs\) charges at most \(T(\left\lvert xs\right\rvert )\) units of time, where \(\left\lvert xs\right\rvert \) is the length of \(xs\) and \(T\) is the recurrence given by \(T(0) = 0\) and \(T(n+1) = T(n) + n\).

Let \(T \colon \mathbb {N}\to \mathbb {N}\) be defined by the recurrence \(T(0) = 0\) and \(T(n+1) = T(n) + n\). Then for every \(n \in \mathbb {N}\),

Let \(\mathit{xs}\) be a list of length \(n\) over a linearly ordered type. Then the total time cost accumulated by the timed insertion sort of \(\mathit{xs}\) is at most \(n^2\).

Let \((n,e)\) be an RSA public key belonging to a secret key that also supplies distinct primes \(p\) and \(q\) with \(n = pq\), a private exponent \(d\), and a natural number \(k\) satisfying \(ed = 1 + k(p-1)(q-1)\). Then for every message \(m \in \mathbb {N}\), decrypting the encryption of \(m\) returns the class of \(m\) modulo \(n\): in \(\mathbb {Z}/n\mathbb {Z}\) we have \(\bigl(\bar m^{\, e}\bigr)^{d} = \bar m\).