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ₙ

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

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` 표기법🔗