4.4. 모나드를 위한 `do`-표기법🔗

모나드에 기반한 API는 매우 강력하지만, 익명 함수와 함께 >>=를 명시적으로 사용하는 것은 여전히 다소 번잡합니다. HAdd.hAdd에 대한 명시적 호출 대신 중위 연산자를 사용하는 것처럼, Lean은 모나드를 사용하는 프로그램을 더 쉽게 읽고 쓸 수 있게 해주는 do-표기법이라는 모나드용 구문을 제공합니다. 이는 IO로 프로그램을 작성할 때 사용하는 것과 완전히 동일한 do-표기법이며, IO 역시 모나드입니다.

Hello, World!에서는 do 구문을 사용하여 IO 액션을 결합했지만, 이러한 프로그램의 의미는 직접적으로 설명되었습니다. 모나드로 프로그래밍하는 방법을 이해한다는 것은 이제 do가 어떻게 기저 모나드 연산자들의 사용으로 변환되는지에 대해 설명할 수 있음을 의미합니다.

do의 첫 번째 번역은 do 안의 유일한 문장이 단일 표현식 E인 경우에 사용됩니다. 이 경우, do가 제거되므로

do E

다음으로 변환됩니다

E

두 번째 번역은 do의 첫 번째 문장이 화살표가 있는 let이어서 지역 변수를 바인딩할 때 사용됩니다. 이는 바로 그 동일한 변수를 바인딩하는 함수와 함께 >>=를 사용하는 것으로 변환되므로

do let x ← E₁
   Stmt
   …
   Eₙ

~로 변환됩니다

E₁ >>= fun x =>
  do Stmt
     …
     Eₙ

do 블록의 첫 번째 문장이 표현식일 경우, 이는 Unit을 반환하는 모나드 액션으로 간주되므로, 함수는 Unit 생성자와 매칭되며

do E₁
   Stmt
   …
   Eₙ

다음으로 변환됩니다

E₁ >>= fun () =>
  do Stmt
     …
     Eₙ

마지막으로, do 블록의 첫 번째 문장이 :=를 사용하는 let인 경우, 변환된 형태는 일반적인 let 표현식이 되므로

do let x := E₁
   Stmt
   …
   Eₙ

로 변환됩니다

let x := E₁
do Stmt
   …
   Eₙ

firstThirdFifthSeventh에 대한, Monad 클래스를 사용하는 정의는 다음과 같습니다:

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α)
    (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

do-표기법을 사용하면 훨씬 더 읽기 쉬워집니다:

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α)
    (xs : List α) : m (α × α × α × α) := do
  let first ← lookup xs 0
  let third ← lookup xs 2
  let fifth ← lookup xs 4
  let seventh ← lookup xs 6
  pure (first, third, fifth, seventh)

Monad 타입 클래스가 없다면, 트리의 노드에 번호를 매기는 함수 number는 다음과 같이 작성되었습니다:

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => ok BinTree.leaf
    | BinTree.branch left x right =>
      helper left ~~> fun numberedLeft =>
      get ~~> fun n =>
      set (n + 1) ~~> fun () =>
      helper right ~~> fun numberedRight =>
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

Monad와 do를 사용하면 그 정의가 훨씬 덜 번잡합니다:

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => pure BinTree.leaf
    | BinTree.branch left x right => do
      let numberedLeft ← helper left
      let n ← get
      set (n + 1)
      let numberedRight ← helper right
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

IO에서 do가 제공하는 모든 편의 기능은 다른 모나드와 함께 사용할 때도 동일하게 사용할 수 있습니다. 예를 들어, 중첩된 액션도 모든 모나드에서 동작합니다. mapM의 원래 정의는 다음과 같았습니다:

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)

do-표기법을 사용하면 다음과 같이 작성할 수 있습니다:

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs => do
    let hd ← f x
    let tl ← mapM f xs
    pure (hd :: tl)

중첩된 액션을 사용하면 원래의 비모나드적 map과 거의 같은 길이로 작성할 수 있습니다:

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs => do
    pure ((← f x) :: (← mapM f xs))

중첩된 액션을 사용하면 number를 훨씬 더 간결하게 만들 수 있습니다:

def increment : State Nat Nat := do
  let n ← get
  set (n + 1)
  pure n

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => pure BinTree.leaf
    | BinTree.branch left x right => do
      pure
        (BinTree.branch
          (← helper left)
          ((← increment), x)
          (← helper right))
  (helper t 0).snd

4.4.1. 연습 문제🔗

evaluateM와 그 헬퍼들, 그리고 다양한 구체적 사용 사례들을 명시적인 >>= 호출 대신 do-표기법을 사용하도록 다시 작성하십시오.
firstThirdFifthSeventh를 중첩된 액션을 사용하여 다시 작성하십시오.

4.4. 모나드를 위한 do-표기법🔗

4.4.1. 연습 문제🔗

4.4. 모나드를 위한 `do`-표기법🔗