lazy list

Stream: Is there code for X?

[Asei Inoue]

I want to implement Haskell's transpose function:

image.png

However, Lean's standard List does not have an equivalent to the repeat function, so it cannot be implemented straightforwardly. How can I implement this with the policy of using a lazy list?

[Asei Inoue]

If a lazy list is not used, it can be implemented as follows.

/-- Version compensated by default value to match the longer one -/
def List.zipWith' {α β γ : Type} (f : α → β → γ) [Inhabited α] [Inhabited β] (xs : List α) (ys : List β) : List γ :=
  match xs, ys with
  | [], [] => []
  | [], y :: ys => f default y :: List.zipWith' f [] ys
  | x :: xs, [] => f x default :: List.zipWith' f xs []
  | x :: xs, y :: ys => f x y :: List.zipWith' f xs ys

def transpose {α : Type} [Inhabited α] (xs : List (List α)) : List (List α) :=
  match xs with
  | [] => []
  | xs :: xss => List.zipWith' (· :: ·) xs (transpose xss)

#guard transpose [[1, 2, 3], [4, 5, 6], [7, 8, 9]] = [[1, 4, 7], [2, 5, 8], [3, 6, 9]]

#guard transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]

[Aaron Liu]

You could use docs#Stream'.Seq

[Asei Inoue]

can we eval an element of Seq?

[Aaron Liu]

What do you mean by "eval"?

[Asei Inoue]

pass to #eval command

[Aaron Liu]

What would happen if you passed an infinite list?

[Robin Arnez]

If you care about a lazy list in general, MLList from batteries might be what you want (not usable for proofs but more or less efficient at runtime).

[Asei Inoue]

could you give me an example of using MLList?

[Robin Arnez]

Something like this:

import Batteries.Data.MLList

partial def repeatTillInfinity (x : α) : MLList Id α :=
  MLList.squash fun _ => MLList.cons x (repeatTillInfinity x)

/--
info: [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3]
-/
#guard_msgs in
#eval (repeatTillInfinity 3).takeAsList 20

[Kim Morrison]

(There's also more functionality on MLList in https://github.com/kim-em/lean-monadic-list, contributions welcome.)