performance of `stream`

Stream: general

[Yury G. Kudryashov]

Once we move stream from core to mathlib (see #9988), I'm going to review stream API (there are some duplicates, lots of lemmas should be @[simp] etc). Since it is used in meta code, probably I should not make performance worse that it is now. So, I have a few questions:

1. Is there an easy way to benchmark a single function? Something like %timeit in Jupyter notebooks.

2. How much does Lean cache? E.g., if I have
   ```
   def f1 : ℕ → ℕ
   | 0 := 1
   | (n + 1) := f1 n + 5

   def g1 (f : ℕ → ℕ) : ∀ n, list ℕ
   | 0 := []
   | (n + 1) := g1 n ++ [f n]

   #eval g1 f1 10
   `` then how many times will it compute f 2`?

3. Am I right that stream is designed to be used with recursively defined functions, so I should assume that stream.nth is probably not $O(1)$?

[Mario Carneiro]

I'm not aware of any code that uses stream. It is not particularly computationally efficient. Well, it's a function type, so it is as computationally efficient as the functions you use to build it, but if you just chain cons or something you will get linear time functions. Lean does not do any kind of memoization here, so a function is run exactly as many times as you call it. In your example, you call f1 9, f1 8, ..., f1 0, and each f1 n calls all previous values, so f1 2 is called a total of 8 times. You can verify this by putting trace in the computation of f1.

[Yury G. Kudryashov]

I saw an import data.streamin control.fix and assumed that it is used for some purpose.

[Mario Carneiro]

Ah, I suspected it might be Simon's doing. He likes FP style programs

[Yury G. Kudryashov]

Another file that imports data.stream is system.random.basic.

[Yury G. Kudryashov]

Am I right that I may refactor stream without computational complexity in mind?

[Mario Carneiro]

I tried commenting out everything that depends on stream in control.fix, control.lawful_fix, and system.random.basic and it seems that there are no other consequences in tactic, meta and system

[Mario Carneiro]

the material that is there is mostly theoretical, e.g. connecting it to omega-CPO's and part. I thought that it might get used by slim_check in its sampleable type class but the fact that commenting it out has no consequences says otherwise

[Yury G. Kudryashov]

Thank you!