4.4. `do`-Notation for Monads🔗

모나드 기반 API는 매우 강력하지만 익명 함수와 함께 >>=를 명시적으로 사용하면 여전히 다소 장황하다. HAdd.hAdd를 명시적으로 호출하는 대신 중위 연산자를 사용하는 것처럼, Lean은 do 표기법이라는 모나드용 문법을 제공한다. 이를 사용하면 모나드를 사용하는 프로그램을 더 쉽게 읽고 쓸 수 있다. 이는 IO 프로그램을 작성할 때 사용하는 바로 그 do 표기법이며, IO도 모나드다.

안녕, 세계!에서는 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. Exercises🔗

evaluateM와 그 보조 함수, 여러 구체적인 사용 사례를 >>=의 명시적 호출 대신 do 표기법을 사용하도록 다시 작성하라.
중첩 동작을 사용해 firstThirdFifthSeventh를 다시 작성하라.

4.4. do-Notation for Monads🔗

4.4.1. Exercises🔗

4.4. `do`-Notation for Monads🔗