`List.foldl` だと早期リターンしないが `List.foldlM` だとできるという例

[Seasawher]

Functional Programming in Lean の 7.1 の演習問題を解いているときに見つけた例。(本文にこれはない)

/- # foldl だと早期リターンしないが、foldM で早期リターンさせる例 -/

/-- 設定情報。コマンドラインツールの設定など -/
structure Config where
  useASCII : Bool := false
  hideDotFiles : Bool := true
  deriving Repr

/-- コマンドライン引数をパースする関数 -/
def configFromArgs (args : List String) : Option Config :=
  dbg_trace "repeated..." -- 再帰関数のカウントのために挿入
  match args with
  | [] => some {}
  | "--ascii" :: args => do
    let cfg ← configFromArgs args
    return {cfg with useASCII := true}
  | "--all" :: args => do
    let cfg ← configFromArgs args
    return {cfg with hideDotFiles := false}
  | _ => none

-- 一回で即終了する
#eval configFromArgs ["--foo", "--bar", "--all", "--ascii"]

/-- foldl を使って書き換えたバージョン。再帰を foldl が行ってくれるようになって、コードの繰り返しが減った。 -/
def configFromArgs' (args : List String) : Option Config :=
  args.foldl (init := some {}) fun cfg arg => do
    dbg_trace "repeated..."
    let config ← cfg
    match arg with
    | "--ascii" => some {config with useASCII := true}
    | "--all" => some {config with hideDotFiles := false}
    | _ => none

-- 早期リターンできていない
#eval configFromArgs' ["--foo", "--bar", "--all", "--ascii"]

/-- 早期リターンを実現すべく foldlM で書き直したバージョン -/
def configFromArgs'' (args : List String) : Option Config :=
  args.foldlM (init := {}) fun cfg arg => do
    dbg_trace "repeated..."
    match arg with
    | "--ascii" => some {cfg with useASCII := true}
    | "--all" => some {cfg with hideDotFiles := false}
    | _ => none

-- 早期リターンできるようになった！！
-- 同時に、再帰を foldM に押し込めることにも成功している
#eval configFromArgs'' ["--foo", "--bar", "--all", "--ascii"]