outputsubdirectory of your current directory.
f x) has a cost of 1, which is embedded into the let-expression with
incon a value of a
reton the result, to lift it into the
costmonad, and we change the type signature to return a
costtype (with a cost of 0 since that is the cost
x, and the other of
reton the result.
inc 2) is 2.
cost b 0becomes
cost b 2:
fand an argument
xand then applies it again on the result:
retgives a cost of 0) while the elaborated code will (since it will add
inc 3to account for the costs of all the function applications).
b, a function
f, and another argument
x, and applies
trueor twice if
applyOncegives a cost of 2, while
applyTwicegives a cost of 3, so we have a collision of costs.
inc 1to the
applyOnce f xclasue to account for the difference between the costs, which would give both clauses of the
if-then-elsea cost of 3:
onceOrTwicefunction itself - to do so we first elaborate the function, which gives us:
thenclause has 4 applications, while the
elseclause has 3, and since the syntactic cost of an
if-then-elseis 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 7into the let-expression.
foowhich would first double a number and then add 7 to the result, by composing the above functions:
foo? trying to simply compose
doubleand lifting the result will now fail to typecheck:
incs we know that the cost of both
add7is 3, so we modify their types in the original code:
foo? trying to simply give it a cost of 5 will fail:
add7into account as well.
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.
doubleis 3, the cost of
add7is 3, and the syntactic cost of
foois 5, adding them all together gives us a cost of 11:
costtype - we apply
reton the base case, and bind the recursion step:
cost int 0:
factis 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.
factagain - we immediately see a problem - the cost of
ret 1is always 0, while the cost of
fact_c (m-1), which can't be 0, so we have 2 pattern matching clauses with different costs.
match-withmust return a result of the same type.
incwe can just use
incRet, which combines the 2:
incRetto the first clause (since the total syntactic cost for a
match-withis 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:
m = 0)?
incRet (10 * m) 1is 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