# Contract Examples

## Preliminary Notes

To **verify** the following examples use:

To **elaborate** and verify the elaborated result use:

The elaborated file will appear within the `output`

subdirectory of your current directory.

In order for most of the examples to work you need to add the following lines at the beginning of your code:

## Simple Example

Let's create a simple function which takes a function and an argument and applies the function on the argument:

Elaborating the function will yield the following:

That's because function application (`f x`

) has a cost of 1, which is embedded into the let-expression with `inc`

.

However - trying to compile this function will result in a typing error

because you can only apply

`inc`

on a value of a`cost`

type.

To fix it we modify the function to use `ret`

on the result, to lift it into the `cost`

monad, and we change the type signature to return a `cost`

type (with a cost of 0 since that is the cost `ret`

gives):

Now elaborating the function will yield the following:

That's because now we have **2 applications**, one of `f`

on `x`

, and the other of `ret`

on the result.

Now the compilation would **still fail** with a typing error:

That's because while the declared cost is 0, the **inferred** cost (due to the addition of `inc 2`

) is 2.

To fix that we now have to declare the **correct** cost within the type, to account for the increment, so `cost b 0`

becomes `cost b 2`

:

Now that the syntactic cost is accounted for the program will compile.

## Aggregated Syntactic Cost

The following function takes a function `f`

and an argument `x`

and applies `f`

on `x`

and then applies it again on the result:

Elaborating this function will yield the following:

The increment by 2 is due to the fact there are 2 applications.

Again - this format won't do, and to be able to compile the elaborated program we have to lift the result into the cost monad and account for the additional costs:

which will be elaborated as:

Notice that this time we've predicted the increased elaborated cost in advance, so the original code won't compile (since `ret`

gives a cost of 0) while the elaborated code will (since it will add `inc 3`

to account for the costs of all the function applications).

In practice - **you won't be able to modify the elaborated code**, since the elaboration is done automatically when activating a contract, so instead you need to elaborate it locally, look at the result, and then modify the **original code** so it would compile right after the elaboration.

## Multiple Clauses

Now let's create another function - which takes a boolean `b`

, a function `f`

, and another argument `x`

, and applies `f`

on `x`

**once** if `b`

is `true`

or **twice** if `b`

is `false`

.

We'll use the previously defined functions to do so:

What should be the declared cost of this function?

`applyOnce`

gives a cost of **2**, while `applyTwice`

gives a cost of **3**, so we have a **collision of costs**.

To reconcile the collision we manually insert `inc 1`

to the `applyOnce f x`

clasue to account for the difference between the costs, which would give both clauses of the `if-then-else`

a cost of **3**:

However - we still need to account for the syntactic cost of the `onceOrTwice`

function itself - to do so we first elaborate the function, which gives us:

That is beacuse the `then`

clause has **4 applications**, while the `else`

clause has **3**, and since the syntactic cost of an `if-then-else`

is defined as **3** + the maximal syntactic cost out of both clauses, which is **4** in this case, we get a total syntactic cost of **7**, which is embedded with an `inc 7`

into the let-expression.

Now to account for the additional cost of **7** we change the declared cost of the function to **10**:

The elaborated code will now compile.

## Composition

Let's define 2 simple functions on the natural numbers - a function which takes a number and doubles it and a function which adds 7 to a number:

We'll also define a function `foo`

which would first double a number and then add 7 to the result, by composing the above functions:

The code will compile just fine, but not the elaboration.

To pass the elaboration we need to make sure all the functions are costed by lifting the results into the `cost`

monad:

What about `foo`

? trying to simply compose `add7`

and `double`

and lifting the result will now fail to typecheck:

That's because we've changed the return type of the functions, so to compose them we have to use the **bind operator** (`>>=`

):

Now elaboration would still fail, so we have to account for the syntactic cost as well - let's look at the elaborated code:

By looking at the `inc`

s we know that the cost of both `double`

and `add7`

is 3, so we modify their types in the original code:

What is the cost of `foo`

? trying to simply give it a cost of 5 will **fail**:

That's because we now have to take the costs of `double`

and `add7`

into account as well.

Recall that the type of the bind operator is: `cost a m -> (a -> cost b n) -> cost b (m+n)`

, so it sums up the costs, which means that's exactly what we have to do.

Since the cost of `double`

is **3**, the cost of `add7`

is **3**, and the syntactic cost of `foo`

is **5**, adding them all together gives us a cost of **11**:

Now the elaborated code will compile.

## Recursion

The cost analysis becomes more complex once you introduce recursion.

The following function computes the factorial of a natural number:

Trying to elaborate this function will fail, since it doesn't return a `cost`

type.

To make sure the result is of a `cost`

type - we apply `ret`

on the base case, and bind the recursion step:

We might prefer to use some syntactic sugar to make the code look nicer:

What should be the return type of the new function? we can start with `cost int 0`

:

Now the elaborated code will not compile, but it will give us some hints on how to specify the cost correctly:

We might be tempted to assign a cost of **10** to the function, but that won't do - if the cost of `fact`

is **10** then `fact (m - 1)`

will have a cost of **10** and after accounting for the incremented syntactic cost (which is added by `inc 10`

) we'll get that the **actual** cost of the function is **20**.

In fact - assuming **any** constant cost will yield a **contradiction**, since we'll always get another 10 steps added to what we've started with, which indicates that it is impossible to assign a constant cost to the function.

How do we resolve it? by making the cost **parametric** in the size of the input, by using **dependent types**.

First we explicitly declare the **name** of the input parameter **in the type**:

Then we can use this name within the cost expression, for example like this:

But this won't do - we have to figure out the actual dependency of the cost on the parameter.

Let's assume for now the cost is some function `fact_c`

on `m`

:

Looking at the definition of `fact`

again - we immediately see a problem - the cost of `ret 1`

is always **0**, while the cost of `fact (m-1)`

is `fact_c (m-1)`

, which **can't be 0**, so we have 2 pattern matching clauses with different costs.

This will result in a typing error when we try to compile the code, since all clauses of a `match-with`

must return a result of the same type.

To fix that we need to add the difference to the first clause, like this (notice this is a modification of the original code, **not** the elaborated code):

Instead of using `ret`

and then `inc`

we can just use `incRet`

, which combines the 2:

Now we have to figure out what `fact_c`

is.

Since the elaborator adds **10** to the cost, and this value didn't change with the addition of the `incRet`

to the first clause (since the total syntactic cost for a `match-with`

is determined only by the syntactically heaviest clause, which is still the second clause), we get **10** added to the cost **with each call to the function**, which means that the **base case** has **at least** a cost of **10**, and with each **recursion step** another **10** is added, so we get the following recurrence relation:

What is the base case (for `m = 0`

)?

Since we know it is **at least 10** (since the cost is increased by 10 and it can never be decreased), we can try assigning it to be 10, which gives us the solution:

So let's try it:

Now the function is elaborated to:

The program now compiles successfully, which indicates that the cost is now correct.

The keen-sighted reader will notice that the first clause `incRet (10 * m) 1`

is operationally equivalent to `ret 1`

, since the only case in which this clause is executed is when `m = 0`

, but since all clauses must return a result of the same type, no matter if they are executed or not, the only way to pass the type checker is by explicitly handling the cost for all possible values of `m`

.

Last updated