Code Reviews

Stream: general

[Shubham Kumar 🦀 (he/him)]

I was looking for a topic related to writing code looking/idiomatic code in lean4, is it ok if I create a new one?

The following code is for AoC Day1 I wasn't sure if I should put in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Advent.20of.20Code.3F if it is I'll close this topic

def dedup [BEq α] (lst : List α) : List α :=
  List.foldl (fun acc x =>
    match acc with
    | [] => x :: acc
    | hd :: _ => if hd == x then acc else x :: acc
  ) [] lst
  |> List.reverse

def CharToString (ch : Char) : String :=
  String.str "" ch

def removeEmptyStrings (lst : List String) : List String :=
  List.filter (fun s => s != "") lst

def splitAtDigitsHelper
  (state : String × List String)
  (ch : Char) : String × List String :=
  let (word, lst) := state
  if Char.isDigit ch then
    -- if character digit found change word to empty string
    -- append character as a string to the list
    -- append it before the word that is generated
    ("", List.append lst [ word, CharToString ch ])
  else
    -- if character not a digit keep appending character to the word
    (String.append word (CharToString ch), lst)

def splitAtDigits (s : String) : List String :=
  let initState := ("", [])
  String.foldl splitAtDigitsHelper initState s
  |> fun (first, lst) => List.append lst [first]
  |> removeEmptyStrings

def isStringDigit (s : String) : Bool :=
  match String.toNat? s with
  | none => false
  | some _ => true

def filterListStringDigit (lst : List String) : List String :=
  List.filter isStringDigit lst

def eliminateAllExceptFirstLast (lst : List String) : List String :=
  let first := List.head? lst
  let last := List.getLast? lst
  match first, last with
  | none, none => []
  | some first, some last => [first, last]
  | _, _ => []

def ListToNat (n : Nat) (lst : List String) : Nat :=
  let StringToNat s :=
    match String.toNat? s with
    | none => 0
    | some n => n

  match lst with
  | [] => n
  | hd :: tl => ListToNat (10 * n + StringToNat hd) tl

def getNumbers (lst : List String) : List Nat :=
  List.map (fun s =>
   splitAtDigits s |>
   filterListStringDigit |>
   eliminateAllExceptFirstLast |>
   (ListToNat 0)) lst

def toSum (lst : List Nat) : Nat :=
  List.foldl (fun acc n => acc + n) 0 lst

def WordToNumber s :=
  match s with
  | "one" => "1"
  | "two" => "2"
  | "three" => "3"
  | "four" => "4"
  | "five" => "5"
  | "six" => "6"
  | "seven" => "7"
  | "eight" => "8"
  | "nine" => "9"
  | _ => s

def firstPass (listOfList : List (List String)) : List (List String) :=
  List.map (List.map WordToNumber) listOfList

def substringExtract (start : Nat) (finish : Nat) (s : String) : String  :=
  let start := String.Pos.mk start
  let finish := String.Pos.mk finish
  let substring := String.toSubstring s
  Substring.extract substring start finish
  |> Substring.toString

def getRest (at_ : Nat) (s : String) : String :=
  let at_ := String.Pos.mk at_
  let last := String.Pos.mk (String.length s)
  let substring := String.toSubstring s
  Substring.extract substring at_ last
  |> Substring.toString

def getWord (s : String) (startIndex : Nat) (endIndex : Nat) : String :=
  substringExtract startIndex endIndex s

def getNDigitWord (s : String) (index : Nat) (N : Nat) : String :=
  getWord s index (index + N) |> WordToNumber

def getNDigitIndexedWords (s : String) (N : Nat) : List (Nat × String) :=
  List.range (String.length s - 1)
  |> List.map (fun index => (index, getNDigitWord s index N))
  |> List.filter (fun (_, word) => isStringDigit word)

def get3DigitIndexWords (s : String) : List (Nat × String) :=
  getNDigitIndexedWords s 3

def get4DigitIndexWords (s : String) : List (Nat × String) :=
  getNDigitIndexedWords s 4

def get5DigitIndexWords (s : String) : List (Nat × String) :=
  getNDigitIndexedWords s 5

def concatDigitsInOrder (s : String) : List String :=
  let indexedThreeDigitWords := get3DigitIndexWords s
  let indexedFourDigitWords := get4DigitIndexWords s
  let indexedFiveDigitWords := get5DigitIndexWords s
  let indexedDigitWords := indexedThreeDigitWords ++ indexedFourDigitWords ++ indexedFiveDigitWords

  List.toArray indexedDigitWords
  |> flip Array.qsort (fun (a, _) (b, _) => a < b)
  |> Array.toList
  |> List.map Prod.snd

def getFirstAndLastOfList? (lst : List α) : Option (α × α) :=
  match List.head? lst, List.getLast? lst with
  | some x, some y => some (x, y)
  | _, _ => none

def secondPass (listOfList : List (List String)) : Nat :=
  let f acc digit :=
    if isStringDigit digit then
      acc ++ [digit]
    else
      acc ++ concatDigitsInOrder digit |> dedup

  let sum acc x :=
    let first := String.toNat? (Prod.fst x)
    let second := String.toNat? (Prod.snd x)

    match first, second with
    | some x, some y => acc + (10 * x + y)
    | _, _ => acc

  listOfList
  |> List.map (List.foldl f [])
  |> List.filterMap getFirstAndLastOfList?
  |> List.foldl sum 0

def day1Part1Fn (path : String) : IO Nat := do
  let input <- IO.FS.readFile path
  pure (String.splitOn input "\n" |> getNumbers |> toSum)

def day1Part2Fn (path : String) : IO Nat := do
  let input <- IO.FS.readFile path
  String.splitOn input "\n"
  |> List.map splitAtDigits
  |> firstPass
  |> secondPass
  |> pure

[Jannis Limperg]

Some suggestions:

• You can use dot notation much more aggressively. For example, List.filter ... lst can be written as lst.filter ..., and similar throughout.
• ListToNat and WordToNumber should be listToNat and wordToNumber. Only types are capitalised.
• Chains of list transformations, e.g. in secondPass, are not as efficient in Lean as they are in Haskell because Lean doesn't optimise away the intermediate lists. Also, arrays are just generally faster in most cases. Probably doesn't matter for this problem, but something to keep in mind.

[Shubham Kumar 🦀 (he/him)]

Jannis Limperg said:

Some suggestions:

• You can use dot notation much more aggressively. For example, List.filter ... lst can be written as lst.filter ..., and similar throughout.
• ListToNat and WordToNumber should be listToNat and wordToNumber. Only types are capitalised.
• Chains of list transformations, e.g. in secondPass, are not as efficient in Lean as they are in Haskell because Lean doesn't optimise away the intermediate lists. Also, arrays are just generally faster in most cases. Probably doesn't matter for this problem, but something to keep in mind.

Thanks! I forgot that I've skipped on camel case in those 2 functions

What is the best alternative for writing chain transformations in Lean? Any specifc style that you can suggest?

[ohhaimark]

firstPass and List.map splitAtDigits could be fused I think.
... |>.map (g ∘ f) instead of ... |>.map f |>.map g

[Shubham Kumar 🦀 (he/him)]

Makes sense, to avoid list unboxing 2 times right?

Thanks for the suggestion :D

ohhaimark said:

firstPass and List.map splitAtDigits could be fused I think.
... |>.map (g ∘ f) instead of ... |>.map f |>.map g

[Jannis Limperg]

Yeah, hand-fusing the transformations basically. It's ugly but more efficient. You could also explore the monadic for loops (which can be used in pure code with Id.run do, where Id is the identity monad). They let you write your folds like in C, which is arguably more natural for complicated folds.

[Kyle Miller]

@Shubham Kumar 🦀 (he/him) Is dedup just supposed to remove consecutive duplicates, or all duplicates? I noticed #eval dedup [1,2,3,1] returns [1,2,3,1]

[Kyle Miller]

Made some changes and added comments where I did.

comments

/-- Remove consecutive deuplicates. -/
def dedup [BEq α] (lst : List α) : List α :=
  match lst with
  | [] => []
  | x :: x' :: xs => if x == x' then dedup (x :: xs) else x :: dedup (x' :: xs)
  | x :: xs => x :: dedup xs

/-- Remove all duplicates. -/
def dedup' [BEq α] (lst : List α) : List α :=
  match lst with
  | [] => []
  | x :: xs => x :: (dedup' xs).filter (· != x)

#eval dedup [1,1,2,3,1] -- [1, 2, 3, 1]
#eval dedup' [1,2,3,1] -- [1, 2, 3]

-- Use toString
def CharToString (ch : Char) : String := toString ch

def removeEmptyStrings (lst : List String) : List String :=
  lst.filter (· != "") -- dot notation, can use `(· != "")` for the `fun`.

def splitAtDigitsHelper -- style, four spaces for arguments so you can tell where the function body starts
    (state : String × List String)
    (ch : Char) : String × List String :=
  let (word, lst) := state
  if ch.isDigit then -- dot notation
    ("", lst ++ [ word, toString ch ]) -- `++` for `List.append
  else
    (s!"{word}{ch}", lst) -- use `s!""` strings for convenience, but could use `++`

def splitAtDigits (s : String) : List String :=
  let initState := ("", [])
  String.foldl splitAtDigitsHelper initState s
  |> fun (first, lst) => lst ++ [first] -- `++`
  |> removeEmptyStrings

-- I see a lot of appending to the end of a `List`. This is not an efficient way to manipulate.
-- lists. Either work in reverse (append to the front) or work with `Array`, where so
-- long as you have a single reference to the array it's efficient to push to the end.

-- Dot notation, removed match. We don't really need it, since we could write `(·.toNat?.isSome)`
-- for this function.
def isStringDigit (s : String) : Bool := s.toNat?.isSome

def filterListStringDigit (lst : List String) : List String :=
  lst.filter isStringDigit -- dot notation

def eliminateAllExceptFirstLast (lst : List String) : List String :=
  -- No need for `let` variables. Saves confusion with `first`/`last` having different meanings
  -- throughout the function.
  match lst.head?, lst.getLast? with
  | none, none => []
  | some first, some last => [first, last]
  | _, _ => []

-- Swap argument order, make accumulator variable default to 0.
-- Another common pattern is to define an aux function that takes this second argument.
def ListToNat (lst : List String) (n : Nat := 0) : Nat :=
  let StringToNat s := s.toNat?.getD 0 -- `getD` rather than `match`

  match lst with
  | [] => n
  | hd :: tl => ListToNat tl (10 * n + StringToNat hd)

def getNumbers (lst : List String) : List Nat :=
  -- dot notation saves some parentheses
  lst.map fun s =>
   splitAtDigits s |>
   filterListStringDigit |>
   eliminateAllExceptFirstLast |>
   ListToNat -- here we can use default variable

def toSum (lst : List Nat) : Nat :=
  -- I like using `(init := ...)` for clarity
  lst.foldl (init := 0) (· + ·) -- rather than `fun`

def WordToNumber s :=
  match s with
  | "one" => "1"
  | "two" => "2"
  | "three" => "3"
  | "four" => "4"
  | "five" => "5"
  | "six" => "6"
  | "seven" => "7"
  | "eight" => "8"
  | "nine" => "9"
  | _ => s

def firstPass (listOfList : List (List String)) : List (List String) :=
  listOfList.map (List.map WordToNumber) -- dot notation

-- No need to go through `Substring`. `String.extract` already does the same logic.
-- Also, using byte indices `start`/`finish` is suspicious design-wise, if this weren't just for AoC
def substringExtract (start : Nat) (finish : Nat) (s : String) : String  :=
  s.extract ⟨start⟩ ⟨finish⟩ -- angle brackets for `String.Pos.mk`

def getRest (at_ : Nat) (s : String) : String :=
  -- String.length is not the last position. This is giving the number of UTF-8 characters,
  -- not the number of bytes. Use `String.endPos`
  s.extract ⟨at_⟩ s.endPos

def getWord (s : String) (startIndex : Nat) (endIndex : Nat) : String :=
  substringExtract startIndex endIndex s

def getNDigitWord (s : String) (index : Nat) (N : Nat) : String :=
  getWord s index (index + N) |> WordToNumber

def getNDigitIndexedWords (s : String) (N : Nat) : List (Nat × String) :=
  List.range (String.length s - 1)
  |>.map (fun index => (index, getNDigitWord s index N)) -- `|>.map` does dot notation
  |>.filter (fun (_, word) => isStringDigit word)

-- Why define these? You don't seem to be gaining anything by specializing the function
-- def get3DigitIndexWords (s : String) : List (Nat × String) :=
--   getNDigitIndexedWords s 3

-- def get4DigitIndexWords (s : String) : List (Nat × String) :=
--   getNDigitIndexedWords s 4

-- def get5DigitIndexWords (s : String) : List (Nat × String) :=
--   getNDigitIndexedWords s 5

def concatDigitsInOrder (s : String) : List String :=
  -- I don't see a point in having the intermediate `lets` you had, since their names sort
  -- of are their expressions.
  let indexedDigitWords := getNDigitIndexedWords s 3 ++ getNDigitIndexedWords s 4 ++ getNDigitIndexedWords s 5

  -- Going back and forth between List and Array costs time and memory.
  -- It would likely be better to stick with Array the whole time if possible.
  List.toArray indexedDigitWords
  --|> (Array.qsort · (fun (a, _) (b, _) => a < b)) -- One option rather than `flip`
  |>.qsort (fun (a, _) (b, _) => a < b) -- A nicer option I think
  |>.toList -- dot notation
  |>.map Prod.snd

def getFirstAndLastOfList? (lst : List α) : Option (α × α) :=
  -- The `match` was fine, but this is a perfect place too for Applicative functors
  Prod.mk <$> List.head? lst <*> List.getLast? lst

def secondPass (listOfList : List (List String)) : Nat :=
  let f acc digit :=
    if isStringDigit digit then
      acc ++ [digit]
    else
      acc ++ concatDigitsInOrder digit |> dedup
      -- Do you mean `dedup` to apply to the whole experssion or just what comes after `++`?
      -- Right now it's the whole `acc ++ ...`

  let sum acc x :=
    let first := String.toNat? (Prod.fst x)
    let second := String.toNat? (Prod.snd x)

    -- getD can simplify this from the `match`
    acc + (10 * first.getD 0 + second.getD 0)

  listOfList -- Dot notations
  |>.map (List.foldl f [])
  |>.filterMap getFirstAndLastOfList?
  |>.foldl sum 0

def day1Part1Fn (path : String) : IO Nat := do
  let input <- IO.FS.readFile path
  -- `return` saves parentheses
  -- can use dot notation
  return input.splitOn "\n" |> getNumbers |> toSum

def day1Part2Fn (path : String) : IO Nat := do
  let input <- IO.FS.readFile path
  -- I think it's clearer with `return` up front rather than `|> pure` at the end
  return input.splitOn "\n"
    |> List.map splitAtDigits
    |> firstPass
    |> secondPass

[Shubham Kumar 🦀 (he/him)]

Kyle Miller said:

Shubham Kumar 🦀 (he/him) Is dedup just supposed to remove consecutive duplicates, or all duplicates? I noticed #eval dedup [1,2,3,1] returns [1,2,3,1]

no I think you caught an error in my logic, I wanted to remove all the duplicates.
Also thanks for the detailed review for the next problem I'll try to include all of them :pray:

[Shubham Kumar 🦀 (he/him)]

Is there a better way by using dot notation to write the following function?

  let toBlank (str : String) := str.map (fun ch =>
      match ch with
      | ':' => ' '
      | ',' => ' '
      | ';' => ' '
      | _   => ch
    )

[Shubham Kumar 🦀 (he/him)]

Also is there a way to use filterMap on Strings, using Substring or String.Iterator? Because essentially I want to filterMap a string but strings are immutable (I'm guessing) so changing in size would not work with the constraint that length remains constant (again guessing)

[Alex J. Best]

Not dot notation but you can save your fingers some typing with

  let toBlank (str : String) := str.map (
      fun
      | ':' | ',' | ';' => ' '
      | _   => ch
    )

[Shubham Kumar 🦀 (he/him)]

Alex J. Best said:

Not dot notation but you can save your fingers some typing with

  let toBlank (str : String) := str.map (
      fun
      | ':' | ',' | ';' => ' '
      | _   => ch
    )

Thanks @Alex J. Best :pray:

[Joachim Breitner]

Did you mean

  let toBlank (str : String) := str.map (
      fun
      | ':' | ',' | ';' => ' '
      | ch  => ch
    )

Also maybe these ugly parentheses aren't needed, didn't check.

[Yaël Dillies]

You can use dot notation as such

  let toBlank : String := .map fun
      | ':' | ',' | ';' => ' '
      | ch  => ch

[Shubham Kumar 🦀 (he/him)]

Yaël Dillies said:

You can use dot notation as such

  let toBlank : String := .map fun
      | ':' | ',' | ';' => ' '
      | ch  => ch

Thanks @Yaël Dillies !

[Shubham Kumar 🦀 (he/him)]

So @Yaël Dillies I am getting an error if I constraint the output type

type mismatch
  String.map fun x =>
    match x with
    | Char.ofNat 58 => Char.ofNat 32
    | Char.ofNat 44 => Char.ofNat 32
    | Char.ofNat 59 => Char.ofNat 32
    | ch => ch
has type
  String → String : Type
but is expected to have type
  String : Type Lean 4

[Yaël Dillies]

Ah sorry, it should of course be String → String, not String.

[Shubham Kumar 🦀 (he/him)]

Yeah that makes sense! sorry my mistake :smile:

[Yaël Dillies]

So either

  let toBlank : String → String := .map fun
      | ':' | ',' | ';' => ' '
      | ch  => ch

or

  let toBlank := String.map fun
      | ':' | ',' | ';' => ' '
      | ch  => ch

[Shubham Kumar 🦀 (he/him)]

so I had a question I was trying to use dot notation for the following function

def filterNoise lst :=
  let filterChars := fun
    | ';' | ':' | ',' => none
    | ch => some ch
  let filterString (str : String) : String :=
    let charList : List Char :=
      str.toList |>.filterMap filterChars
    charList.foldl (init := "") String.push

-- instead of using lst.map filterString
  List.map filterString lst

But using lst.map filterString results in the following error

invalid field notation, type is not of the form (C ...) where C is a constant
  lst
has type
  ?m.6 Lean 4

[Shubham Kumar 🦀 (he/him)]

why is that? Semantically they should be the same right?

[Yaël Dillies]

This just tells you that Lean doesn't know what the type of lst is, hence it can't look up any dot notation!

[Yaël Dillies]

def filterNoise (lst : List _) := should work.

[Shubham Kumar 🦀 (he/him)]

ah ok, I didn't understand the error. Thanks @Yaël Dillies again :pray: