Central to the analysis of contracts cost is the notion of a cost model.
A cost model for a language assigns a natural number to each closed term in the language in such a way that the term should take at most this number of "abstract steps" to evaluate, this natural number is called the cost of that term (relative to that cost model).
The abstract steps could be, for example, beta-reductions, so if the cost of a term M is n it would take at most n beta-reductions to reduce M to a normal form with the chosen evaluation strategy of the language.
The cost is defined recursively on the structure of the term, and it could depend on the values of some of its subterms, so we can think of the cost as a term in the language which evalutes to a natural number.
We use the notation
for the cost of the term M.
Notice how the cost of both function abstraction and applied let clause is 0 - that's because function abstraction is in a weak head normal form - it's not evaluated further until it is applied on an argument, so as far as the execution environment is concerned it is already a value, so it won't be evaluated further; The cost of applied let clause is 0 as well, since an applied let expression if equivalent to a beta redex where the argument is itself a lambda (
is equivalent to
), so it is considered the same; In both cases the cost of the body of the function is internalized, through the use of inc (which would be explained later).
In practice the actual cost (relative to the cost model) is not computed directly, instead - the cost is decomposed into 2 components:
- 1.Compositional Cost - which is declared by thedeveloper and verified by the type system
- 2.Syntactic Cost - which is computed by the elaborator
In fact - given general recursion it is impossible to automatically compute the cost of any arbitrary term in the language.
Another deviation from the cost model is that the cost we give in practice is an upper bound on the cost given by the cost model, because it is easier to compute, but since the cost model itself is an upper bound on the number of steps the approximation we use in practice still gives a valid upper bound.
The syntactic cost is given to terms by virtue of their form, and acts as a seed which the compositional cost later propogates into the program through the type system.
Given a cost model we define a special type constructor
costto indicate that a term of type
A m, where
Ais a type and
mis a natural number, would take at most
msteps to produce a value of type
Dually - we use the type
cost A mto indicate that a term of this type represents a value of type A which has taken at most
msteps to evaluate.
When a term
Mhas the type
cost A mwe say that M is a costed term, with a cost of m.
When a function
fhas the type
A -> cost B mwe say that
fis a costed function, with a cost of
m, which means that when given an input of type
msteps to produce an output of type
costtype constructor behaves as a an indexed monad, indexed over the additive monoid of the natural numbers, so whenever you compose (using Kleisli composition) 2 costed functions
f : B -> cost C nand
g : A -> cost B myou get a function of type
A -> cost C (m + n)where the cost is the sum of the costs of
The bind operator (
>>=) has the type signature:
bind: cost a m -> (a -> cost b n) -> cost b (m+n)
In practice - the
costmonad in ZF* is implemented as the identity monad, where the index could be set arbitrarily, so as far as ZF* is concerned - it is up to the developer to honestly declare the costs of terms.
The validity of the cost of a term is not fully enforced by the compiler!
The compiler only makes sure that the costs are composed correctly.
To enforce the validity of the costs we combine the compiler with an elaborator, which would be explained in detail later on.
To lift a term into the monad we use the
retfunction, which is the unit of the monad and has the type
ret : a -> cost a 0. Since the
retfunction gives a term a cost of
0, we use the function
inc : (m:nat) -> cost a n -> cost a (n+m)to increase the declared cost of a term.
The cost monad can only ensure that costs are composed correctly, but it cannot enforce the declared costs to conform to the cost model - it completely trusts the developer to declare costs honestly.
In order to actually enforce the cost model, we use a device called the elaborator.
The elaborator scans the syntax trees of the terms and recursively sums up the cost of each branch, adding additional constant cost with each clause and primitive operation.
Eventually, when the elaborator reaches either a lambda expression, or a let expression (which could be a top-level let) - it embeds the accumulated cost of the body of the expression into the body, by replacing it with an application of the inc function, along with the accumulated cost, on the body; this ensures 2 things:
- 1.That the term returns an output which is wrapped in the costmonad.
- 2.That all the syntactic cost is accounted for.