- 1.Compositional Cost - which is declared by thedeveloper and verified by the type system
- 2.Syntactic Cost - which is computed by the elaborator
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
cost A mto indicate that a term of this type represents a value of type A which has taken at most
msteps to evaluate.
Mhas the type
cost A mwe say that M is a costed term, with a cost of m.
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
>>=) has the type signature:
bind: cost a m -> (a -> cost b n) -> cost b (m+n)
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.
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.
- 1.That the term returns an output which is wrapped in the costmonad.
- 2.That all the syntactic cost is accounted for.