Heinrich Apfelmus apfelmus at quantentunnel.de
Sat Dec 5 14:15:40 UTC 2015

```Dear Joachim,

you probably already know the basics of lazy evaluation, but to fix
conventions, allow me to plug a tutorial of mine:

As you mentioned, reasoning about time usage is not entirely
straightforward, since expressions may be evaluated partially. Chris
Okasaki's thesis/book does treat this problem in chapter 6, in order to
clarify what amortization means in a language with persistent data
structures, and why lazy evaluation is very useful for that.

The main idea is that to each constructor of a data structure, we assign
a cost, which is a number of "debits". Whenever we evaluate a
constructor to WHNF, we have to pay the number of debits assigned to it.
Then, the debits that we have paid so far will always be an upper bound
on the time that we have spent evaluating the expression so far.

For instance, the `length` function creates an integer whose assigned
number of debits is twice the sum of the debits of each constructor in
the input list.

http://apfelmus.nfshost.com/articles/debit-method.html

Ultimately, the point of the debit method is to reflect the time needed
for evaluation  of an expression (a notion from operational semantics)
in the value that this expression represents (a notion from denotational
semantics).

Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com

Joachim Durchholz wrote:
> Hi all,
>
> Stuff like big-Oh space and time complexity of a function.
>
> What I'm mostly after is how to organize complexity reasoning given
> non-strict evaluation. In that situation, a function's complexity
> depends on what subexpressions of the parameters have already been
> evaluated, so you get rather complicated conditional formulae, and you
> also need to somehow express what parts of a passed-in parameter may get
> evaluated under what conditions.
> Is there even a good notation for that kind of stuff? Is there advice on
> how to organize the code to make performance formulae manageable?
>
> Example: Performance of
>   length xs
> Turns out it is the number of items in xs, plus whatever you need to
> evaluate the list spine, as far as the list spine elements have not yet
> been evaluated (but you do not need to evaluate the list items).
> I have no idea how to even write that down. What notation to use so one
> can formally reason about it.
>
> Any pointers?
>
> Regards,
> Jo

```