IO Mutable Array

Stream: lean4

[dudubao2007]

Is there an O(1) random-access and random-modification Array in the IO Monad in Lean 4 like C's array and Haskell's IOArray?

[Marc Huisinga]

Array is that if you are using it linearly (you can check this e.g. via dbgTraceIfShared)

[Marc Huisinga]

Or more explicitly: If the reference count is 1, Lean will update arrays in-place.

[dudubao2007]

I'm sorry that I can't understand that. o(╥﹏╥)o
For example, I want to count the primes from 1 to n using Euler's sieve.
How can I write that just like in the procedural style?

[Marc Huisinga]

Here's a more simple example:

def mapa [Inhabited α] (xs : Array α) (f : α → α) : Array α := Id.run do
  let mut xs := xs
  for i in [0:xs.size] do
    xs := dbgTraceIfShared "this will print something if xs has rc > 1" xs
    xs := xs.set! i (f xs[i])
  return xs

def foo (init n : Nat) : Nat := Id.run do
  let mut xs := #[]
  for i in [0:n] do
    xs := xs.push init
  xs := dbgTraceIfShared "this will print something if xs has rc > 1" xs
  xs := mapa xs (· + 1)
  return xs[0]

#eval foo 3 100000

[Marc Huisinga]

mapa will mutate the array in-place if xs has a reference count of 1 (i.e. it is not shared).

[dudubao2007]

I see. Thank you a lot! :heart:

[dudubao2007]

def euler (n : Nat) : Nat := Id.run do
  let mut ip := Array.mk <| [false, false] ++ List.replicate (n-1) true
  let mut prime := #[]
  let mut cnt := 0
  for i in [2:n+1] do
    if ip[i] then
      cnt := cnt + 1
      prime := prime.push i
    for j in [0:cnt] do
      if i * prime[j] > n then break
      ip := ip.set! (i * prime[j]) false
      if i % prime[j] == 0 then break
  return cnt

#eval euler 1000000

Sorry to bother.
Is it a normal phenomenon that calculating euler 10^6 takes 4 secs and euler 10^7 causes stack overflow?

[Henrik Böving]

You are using eval instead of compiling your code so you shouldn't expect too good of a performance yeah

[dudubao2007]

Oh :joy: , thank you. It takes 0.3 secs to calculate euler 10^6. However, it stills causes stack overflow to calculate euler 10^7.

[Marc Huisinga]

That might be List.replicate

[Henrik Böving]

Yeah, also note that using Array.mk on a List adds an additional O(n) to your runtime since the array consructor has to iterate over the list.

[dudubao2007]

Should I use "push"?

[Henrik Böving]

If you want to achieve as much performance as possible you should simply not use List at all.

[Mauricio Collares]

I guess the question is "What is the fastest way of creating an array with N elements, all equal to some value V"?

[dudubao2007]

Yes. :+1: :smiley:

[Marc Huisinga]

Try mkArray (n-1) true

[Marc Huisinga]

I.e. #[false, false] ++ mkArray (n-1) true or with less copying

let mut ip := mkArray (n+1) true
ip := ip.set! 0 false
ip := ip.set! 1 false

[dudubao2007]

Thanks. I have trouble finding suitable library functions. Is there a way to search a library function by its type(like Haskell's Hoogle)?

[dudubao2007]

Marc Huisinga said:

I.e. #[false, false] ++ mkArray (n-1) true or with less copying

let mut ip := mkArray (n+1) true
ip := ip.set! 0 false
ip := ip.set! 1 false

It only takes 0.18 secs to calc euler 10^6. Thank you! :big_smile:

[Henrik Böving]

There is #find which is made for proof search but I guess it could also find regular functions, apart from that we only have search by name here right now: https://leanprover-community.github.io/mathlib4_docs/ getting a hoogle like thing working is definitely on my List as well at some point but it would require an actual Lean backend instead of just generating HTML via Lean which is a whole different complexity class.

[Marc Huisinga]

Note that you need Mathlib4 for #find