6.4. More do Features🔗

Lean의 do 표기는 명령형 프로그래밍 언어와 비슷한 방식으로 모나드를 사용하는 프로그램을 작성하는 문법을 제공한다. do 표기는 모나드 프로그램을 편리하게 작성하게 할 뿐 아니라, 특정 모나드 변환기를 사용하는 문법도 제공한다.

6.4.1. Single-Branched `if`🔗

모나드를 사용할 때 흔히 쓰는 패턴은 어떤 조건이 참일 때만 부수 효과를 수행하는 것이다. 예를 들어 countLetters는 모음이나 자음인지 검사하며, 어느 쪽도 아닌 문자는 상태에 영향을 주지 않는다. 이는 효과가 없는 pure ()를 else 분기의 결과로 만드는 것으로 표현한다.

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  let rec loop (chars : List Char) := do
    match chars with
    | [] => pure ()
    | c :: cs =>
      if c.isAlpha then
        if vowels.contains c then
          modify fun st => {st with vowels := st.vowels + 1}
        else if consonants.contains c then
          modify fun st => {st with consonants := st.consonants + 1}
        else -- 수정되었거나 영어가 아닌 문자
          pure ()
      else throw (.notALetter c)
      loop cs
  loop str.toList

do 블록의 if가 표현식이 아니라 문이면 else pure ()를 생략해도 되며, Lean이 이를 자동으로 삽입한다. 다음 countLetters 정의는 완전히 동등하다.

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  let rec loop (chars : List Char) := do
    match chars with
    | [] => pure ()
    | c :: cs =>
      if c.isAlpha then
        if vowels.contains c then
          modify fun st => {st with vowels := st.vowels + 1}
        else if consonants.contains c then
          modify fun st => {st with consonants := st.consonants + 1}
      else throw (.notALetter c)
      loop cs
  loop str.toList

상태 모나드를 사용해 어떤 모나드 검사 조건을 만족하는 리스트 원소의 수를 세는 프로그램은 다음과 같이 작성할 수 있다.

def count [Monad m] [MonadState Nat m] (p : α → m Bool) : List α → m Unit
  | [] => pure ()
  | x :: xs => do
    if ← p x then
      modify (· + 1)
    count p xs

마찬가지로 if not E1 then STMT...는 unless E1 do STMT...로 바꿔 쓸 수 있다. 모나드 검사를 만족하지 않는 원소의 수를 세는 count의 반대 함수는 if를 unless로 바꾸어 작성할 수 있다.

def countNot [Monad m] [MonadState Nat m] (p : α → m Bool) : List α → m Unit
  | [] => pure ()
  | x :: xs => do
    unless ← p x do
      modify (· + 1)
    countNot p xs

한 갈래 if와 unless를 이해하는 데 모나드 변환기를 생각할 필요는 없다. 이들은 누락된 분기를 pure ()로 바꿀 뿐이다. 그러나 이 절의 나머지 확장 기능은 Lean이 do 블록을 자동으로 다시 써서, 블록이 작성된 모나드 위에 국소 변환기를 추가하게 한다.

6.4.2. Early Return🔗

표준 라이브러리에는 어떤 검사를 만족하는 리스트의 첫 원소를 반환하는 함수 List.find?가 들어 있다. Option이 모나드라는 사실을 사용하지 않는 간단한 구현은 재귀 함수로 리스트를 순회하고, 원하는 원소를 찾으면 if로 반복을 멈춘다.

def List.find? (p : α → Bool) : List α → Option α
  | [] => none
  | x :: xs =>
    if p x then
      some x
    else
      find? p xs

명령형 언어에는 보통 함수 실행을 중단하고 어떤 값을 호출자에게 즉시 반환하는 return 키워드가 있다. Lean의 do 표기에서도 이를 사용할 수 있다. return은 do 블록의 실행을 중단하며, return의 인자가 모나드에서 반환할 값이 된다. 즉 List.find?를 다음과 같이 작성할 수도 있다.

def List.find? (p : α → Bool) : List α → Option α
  | [] => failure
  | x :: xs => do
    if p x then return x
    find? p xs

명령형 언어의 조기 반환은 현재 스택 프레임만 풀 수 있는 예외와 조금 비슷하다. 조기 반환과 예외는 모두 코드 블록의 실행을 종료하고, 사실상 주변 코드를 던져진 값으로 바꾼다. Lean의 조기 반환은 내부적으로 ExceptT의 한 형태를 사용해 구현된다. 조기 반환을 사용하는 각 do 블록은 (tryCatch 함수의 의미에서) 예외 처리기로 감싸진다. 조기 반환은 값을 예외로 던지는 것으로 번역되고, 처리기는 던져진 값을 잡아 즉시 반환한다. 즉 do 블록의 원래 반환값 타입이 예외 타입으로도 사용된다.

이를 구체적으로 살펴보면, 예외 타입과 반환 타입이 같을 때 보조 함수 runCatch는 모나드 변환기 스택 맨 위의 ExceptT 한 층을 제거한다.

def runCatch [Monad m] (action : ExceptT α m α) : m α := do
  match ← action with
  | Except.ok x => pure x
  | Except.error x => pure x

조기 반환을 사용하는 List.find?의 do 블록은 runCatch를 사용해 감싸고 조기 반환을 throw로 바꾸어 조기 반환을 사용하지 않는 do 블록으로 번역된다.

def List.find? (p : α → Bool) : List α → Option α
  | [] => failure
  | x :: xs =>
    runCatch do
      if p x then throw x else pure ()
      monadLift (find? p xs)

조기 반환이 유용한 또 다른 상황은 인자나 입력이 잘못되면 일찍 종료하는 명령줄 애플리케이션이다. 많은 프로그램은 본문으로 진행하기 전에 인자와 입력을 검증하는 부분으로 시작한다. 다음 인사 프로그램 hello-name 버전은 명령줄 인자가 제공되지 않았는지 확인한다.

def main (argv : List String) : IO UInt32 := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  let stderr ← IO.getStderr

  unless argv == [] do
    stderr.putStrLn s!"Expected no arguments, but got {argv.length}"
    return 1

  stdout.putStrLn "How would you like to be addressed?"
  stdout.flush

  let name := (← stdin.getLine).trimAscii
  if name.isEmpty then
    stderr.putStrLn s!"No name provided"
    return 1

  stdout.putStrLn s!"Hello, {name}!"

  return 0

인자 없이 실행하고 David라는 이름을 입력하면 이전 버전과 같은 결과가 나온다.

lean --run EarlyReturn.lean

How would you like to be addressed?

David

Hello, David!

이름을 답변 대신 명령줄 인자로 제공하면 오류가 발생한다.

lean --run EarlyReturn.lean David

Expected no arguments, but got 1

이름을 제공하지 않으면 다른 오류가 발생한다.

lean --run EarlyReturn.lean

How would you like to be addressed?

No name provided

조기 반환을 사용하는 프로그램은 다음과 같이 조기 반환을 사용하지 않는 버전처럼 제어 흐름을 중첩할 필요가 없다.

def main (argv : List String) : IO UInt32 := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  let stderr ← IO.getStderr

  if argv != [] then
    stderr.putStrLn s!"Expected no arguments, but got {argv.length}"
    pure 1
  else
    stdout.putStrLn "How would you like to be addressed?"
    stdout.flush

    let name := (← stdin.getLine).trimAscii
    if name.isEmpty then
      stderr.putStrLn s!"No name provided"
      pure 1
    else
      stdout.putStrLn s!"Hello, {name}!"
      pure 0

Lean의 조기 반환과 명령형 언어의 조기 반환 사이의 중요한 차이는 Lean의 조기 반환이 현재 do 블록에만 적용된다는 점이다. 함수 정의 전체가 같은 do 블록 안에 있으면 이 차이는 중요하지 않다. 그러나 다른 구조 아래에서 do가 나타나면 차이가 드러난다. 예를 들어 다음과 같이 greet를 정의했다고 하자.

def greet (name : String) : String :=
  "Hello, " ++ Id.run do return name

표현식 greet "David"는 "David"만이 아니라 "Hello, David"로 평가된다.

6.4.3. Loops🔗

가변 상태를 가진 모든 프로그램을 상태를 인자로 전달하는 프로그램으로 다시 쓸 수 있듯이, 모든 반복문을 재귀 함수로 다시 쓸 수 있다. 한 관점에서 List.find?는 재귀 함수로 보는 것이 가장 분명하다. 정의가 리스트의 구조를 그대로 반영하기 때문이다. 머리가 검사를 통과하면 반환하고, 그렇지 않으면 꼬리에서 찾는다. 더 이상 원소가 남지 않으면 답은 none이다. 다른 관점에서 List.find?는 반복문으로 보는 것이 가장 분명하다. 프로그램이 만족스러운 원소를 찾을 때까지 순서대로 원소를 확인하고, 찾으면 종료하기 때문이다. 반환하지 않은 채 반복이 종료되면 답은 none이다.

6.4.3.1. Looping with ForM🔗

Lean에는 컨테이너 타입을 순회하는 방법을 설명하는 타입 클래스가 있다. 이 클래스는 ForM이라고 한다.

class ForM (m : Type u → Type v) (γ : Type w₁)
    (α : outParam (Type w₂)) where
  forM (coll : γ) (f : α → m PUnit) : m PUnit

이 클래스는 상당히 일반적이다. 매개변수 m은 원하는 효과를 허용하며 보통 모나드이고, γ는 순회할 컬렉션이며, α는 컬렉션 원소의 타입이다. 보통 m은 어떤 모나드든 될 수 있지만, 예를 들어 IO에서만 순회를 지원하는 자료 구조도 만들 수 있다. 메서드 forM은 컬렉션과 각 원소에 대해 효과를 실행할 동작을 받아 그 동작들을 실행한다.

List의 인스턴스는 m을 어떤 모나드든 될 수 있게 하고, γ를 List α로 설정하며, 클래스의 α를 리스트에 들어 있는 α와 같게 한다.

def List.forM [Monad m] : List α → (α → m PUnit) → m PUnit
  | [], _ => pure ()
  | x :: xs, action => do
    action x
    forM xs action

instance [Monad m] : ForM m (List α) α where
  forM := List.forM

doug의 함수 doList는 리스트에 대한 forM이다. forM을 사용하면 countLetters를 훨씬 짧게 만들 수 있다.

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  forM str.toList fun c => do
    if c.isAlpha then
      if vowels.contains c then
        modify fun st => {st with vowels := st.vowels + 1}
      else if consonants.contains c then
        modify fun st => {st with consonants := st.consonants + 1}
    else throw (.notALetter c)

Many의 인스턴스도 매우 비슷하다.

def Many.forM [Monad m] : Many α → (α → m PUnit) → m PUnit
  | Many.none, _ => pure ()
  | Many.more first rest, action => do
    action first
    forM (rest ()) action

instance [Monad m] : ForM m (Many α) α where
  forM := Many.forM

γ가 어떤 타입이든 될 수 있으므로 ForM은 다형적이지 않은 컬렉션도 지원할 수 있다. 아주 간단한 컬렉션으로 주어진 수보다 작은 자연수를 역순으로 나열하는 것을 들 수 있다.

structure AllLessThan where
  num : Nat

이 컬렉션의 ForM 연산자는 더 작은 Nat 각각에 제공된 동작을 적용한다.

def AllLessThan.forM [Monad m]
    (coll : AllLessThan) (action : Nat → m Unit) :
    m Unit :=
  let rec countdown : Nat → m Unit
    | 0 => pure ()
    | n + 1 => do
      action n
      countdown n
  countdown coll.num

instance [Monad m] : ForM m AllLessThan Nat where
  forM := AllLessThan.forM

ForM을 사용하면 5보다 작은 각 수에 IO.println을 실행할 수 있다.

4
3
2
1
0
#eval forM { num := 5 : AllLessThan } IO.println

특정 모나드에서만 작동하는 ForM 인스턴스의 예로 표준 입력 같은 IO 스트림에서 읽은 줄을 순회하는 인스턴스를 들 수 있다.

structure LinesOf where
  stream : IO.FS.Stream

partial def LinesOf.forM
    (readFrom : LinesOf) (action : String → IO Unit) :
    IO Unit := do
  let line ← readFrom.stream.getLine
  if line == "" then return ()
  action line
  forM readFrom action

instance : ForM IO LinesOf String where
  forM := LinesOf.forM

스트림이 유한하다는 보장이 없으므로 LinesOf.forM 정의에는 partial 표시가 붙어 있다. 이 경우 IO.FS.Stream.getLine은 IO 모나드에서만 작동하므로 반복에 다른 모나드를 사용할 수 없다.

이 예제 프로그램은 이 반복 구조를 사용해 문자를 포함하지 않는 줄을 걸러 낸다.

def main (argv : List String) : IO UInt32 := do
  if argv != [] then
    IO.eprintln "Unexpected arguments"
    return 1

  forM (LinesOf.mk (← IO.getStdin)) fun line => do
    if line.any (·.isAlpha) then
      IO.print line

  return 0

test-data 파일의 내용은 다음과 같다.

                  File: test-dataHello!!!!!!12345abc123Ok

ForMIO.lean에 저장된 이 프로그램을 호출하면 다음 출력이 나온다.

lean --run ForMIO.lean < test-data

Hello!
abc123
Ok

6.4.3.2. Stopping Iteration🔗

ForM으로 반복을 일찍 종료하기는 어렵다. AllLessThan의 Nat들을 3에 도달할 때까지만 순회하는 함수를 작성하려면 반복 중간에 멈출 방법이 필요하다. 한 가지 방법은 ForM을 OptionT 모나드 변환기와 함께 사용하는 것이다. 첫 단계는 반환값과 변환된 계산의 성공 여부에 관한 정보를 모두 버리는 OptionT.exec를 정의하는 것이다.

def OptionT.exec [Applicative m] (action : OptionT m α) : m Unit :=
  action *> pure ()

그런 다음 Alternative의 OptionT 인스턴스에서 실패를 이용해 반복을 일찍 종료할 수 있다.

def countToThree (n : Nat) : IO Unit :=
  let nums : AllLessThan := ⟨n⟩
  OptionT.exec (forM nums fun i => do
    if i < 3 then failure else IO.println i)

간단한 테스트로 이 해법이 작동함을 확인할 수 있다.

6
5
4
3
#eval countToThree 7

그러나 이 코드는 읽기가 그다지 쉽지 않다. 반복을 일찍 종료하는 일은 흔하므로 Lean은 이를 쉽게 만드는 추가 문법 설탕을 제공한다. 같은 함수를 다음과 같이 작성할 수도 있다.

def countToThree (n : Nat) : IO Unit := do
  let nums : AllLessThan := ⟨n⟩
  for i in nums do
    if i < 3 then break
    IO.println i

테스트해 보면 앞선 버전과 똑같이 작동함을 알 수 있다.

6
5
4
3
#eval countToThree 7

for ...in ...do ... 문법은 ForIn이라는 타입 클래스의 사용으로 문법 설탕이 제거된다. 이 타입 클래스는 상태와 조기 종료를 추적하는, 다소 더 복잡한 ForM의 변형이다. 표준 라이브러리는 ForM 인스턴스를 ForIn 인스턴스로 바꾸는 ForM.forIn이라는 어댑터를 제공한다. 이 어댑터는 내부적으로 StateT와 ExceptT를 사용하므로, 특정 모나드 하나가 아니라 모나드 변환기로 만든 모나드와 함께 ForM 인스턴스를 사용할 수 있어야 한다. ForM 인스턴스에 기반한 for 반복문을 사용하려면 AllLessThan과 Nat을 적절히 바꾸어 다음과 같은 내용을 추가하라.

instance [Monad m] : ForIn m AllLessThan Nat where
  forIn := ForM.forIn

for 반복문에서도 조기 반환을 지원한다. 조기 반환이 있는 do 블록을 예외 모나드 변환기를 사용하는 형태로 번역하는 방식은, 앞서 OptionT로 반복을 멈춘 것과 마찬가지로 ForM 아래에서도 잘 작동한다. 다음 List.find? 버전은 두 기능을 모두 사용한다.

def List.find? (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if p x then return x
  failure

break뿐 아니라 for 반복문은 한 반복에서 나머지 본문을 건너뛰는 continue도 지원한다. List.find?를 다르게(하지만 혼란스럽게) 작성하면 검사 조건을 만족하지 않는 원소를 건너뛸 수 있다.

def List.find? (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if not (p x) then continue
    return x
  failure

범위(range)는 어떤 타입의 연속된 원소들을 하한부터 상한까지 나타낸다. 경계는 열린(open) 경계일 수 있으며 이 경우 경계값은 범위에 포함되지 않는다. 또는 닫힌(closed) 경계일 수 있으며 이 경우 경계값이 포함된다. 범위는 무한히 이어지거나 해당 타입의 최솟값 또는 최댓값에 도달할 때까지 이어지는 무경계일 수도 있다.

범위는 경계를 설명하는 명명 규칙을 따르는 타입들의 모음으로 나타낸다. 각 타입의 이름은 R로 시작하고, 다음 두 글자가 각각 하한과 상한을 결정한다.

o는 경계값이 포함되지 않는 열린 경계를 나타낸다.
c는 경계값이 포함되는 닫힌 경계를 나타낸다.
i는 범위를 제한하지 않는 무한 경계를 나타낸다.

예를 들어 Std.Rco Nat 타입은 하한을 포함하고 상한을 제외하는 좌측 닫힘·우측 열림 Nat 수열을 나타내며, Std.Roi Nat은 하한 바로 위에서 시작하는 무한 Nat 수열을 나타낸다. 무한 경계가 항상 무한 범위를 만드는 것은 아니다. 예를 들어 Std.Rio Nat에는 하한이 없지만 Nat 자체에 0이라는 고유한 하한이 있으므로 수열은 유한하다.

Lean에는 각 경계를 지정할 수 있는 범위 생성 전용 문법이 있다. 범위는 경계 사이에 점 세 개를 놓아 지정하며, 경계 자체는 특정 값이나 무경계를 나타내는 별표로 지정할 수 있다. 예를 들어 3부터 10까지의 범위는 3...10으로 쓰며 타입은 Std.Rco Nat이다. 범위는 기본적으로 좌측 닫힘·우측 열림이다. 즉 3...10은 3을 포함하지만 10은 포함하지 않는다. 이 기본값은 재정의할 수 있다. <는 열린 상한이나 하한을 지정하고, =는 닫힌 상한을 지정한다. 3<...=10은 3을 포함하지 않고 10을 포함한다. 반면 3...=10은 둘 다 포함하고 3<...10은 둘 다 포함하지 않는다. 3<...=10의 타입은 Std.Roc Nat이고, 3<...10의 타입은 Std.Roo Nat이다. *...5 범위에는 0, 1, 2, 3, 4가 들어가며, 3...*에는 3 이상인 모든 자연수가 들어간다.

범위는 항상 오름차순이다. 범위의 하한이 상한보다 크면 역순으로 진행하는 대신 어떤 값도 포함하지 않는다. 예를 들어 10...3은 비어 있다.

적절한 타입 클래스 인스턴스가 있으면 범위를 for 반복문과 함께 사용해 범위에서 값을 꺼낼 수 있다. 이 프로그램은 4부터 8까지의 짝수를 출력한다.

def fourToEight : IO Unit := do
  for i in 2...5 do
    IO.println (i * 2)

실행 결과는 다음과 같다.

4
6
8

이 프로그램은 'l'부터 'p'까지의 문자를 출력한다.

l
m
n
o
p
#eval do
  for letter in 'l'...='p' do
    IO.println letter

l
m
n
o
p

마지막으로 for 반복문은 in 절을 쉼표로 구분해 여러 컬렉션을 병렬로 순회할 수 있다. 첫 번째 컬렉션의 원소가 먼저 소진되면 반복이 멈추므로 다음 선언은

def parallelLoop := do
  for x in ["currant", "gooseberry", "rowan"], y in 'a'...'e' do
    IO.println (x, y)

세 줄의 출력을 만든다.

(currant, a)
(gooseberry, b)
(rowan, c)
#eval parallelLoop

(currant, a)
(gooseberry, b)
(rowan, c)

많은 자료 구조는 ForIn 타입 클래스의 확장 버전을 구현해, 원소가 컬렉션에서 나온 것이라는 증거를 반복문 본문에 추가한다. 원소 이름 앞에 증거의 이름을 제공하면 이를 사용할 수 있다. 이 함수는 배열의 모든 원소와 인덱스를 함께 출력하며, 컴파일러는 증거 h 덕분에 배열 조회가 모두 안전하다는 것을 알아낼 수 있다.

def printArray [ToString α] (xs : Array α) : IO Unit := do
  for h : i in 0...xs.size do
    IO.println s!"{i}:\t{xs[i]}"

이 예에서 h는 i ∈ 0...xs.size라는 증거이며, xs[i]가 안전한지 검사하는 전술은 이를 i < xs.size라는 증거로 바꿀 수 있다.

6.4.4. Mutable Variables🔗

조기 return, else 없는 if, for 반복문 외에도 Lean은 do 블록 안의 국소 가변 변수를 지원한다. 내부적으로 이 가변 변수들은 실제 가변 변수로 구현되는 대신 StateT와 동등한 코드로 문법 설탕이 제거된다. 여기서도 함수형 프로그래밍으로 명령형 프로그래밍을 모사한다.

국소 가변 변수는 일반 let 대신 let mut으로 도입한다. 효과를 도입하지 않고 do 문법을 사용할 수 있도록 항등 모나드 Id를 사용하는 two 정의는 2를 센다.

def two : Nat := Id.run do
  let mut x := 0
  x := x + 1
  x := x + 1
  return x

이 코드는 StateT를 사용해 1을 두 번 더하는 정의와 동등하다.

def two : Nat :=
  let block : StateT Nat Id Nat := do
    modify (· + 1)
    modify (· + 1)
    return (← get)
  let (result, _finalState) := block 0
  result

국소 가변 변수는 모나드 변환기를 위한 편리한 문법을 제공하는 do 표기의 다른 기능들과도 잘 작동한다. three 정의는 원소가 세 개인 리스트의 원소 수를 센다.

def three : Nat := Id.run do
  let mut x := 0
  for _ in [1, 2, 3] do
    x := x + 1
  return x

마찬가지로 six은 리스트의 원소를 더한다.

def six : Nat := Id.run do
  let mut x := 0
  for y in [1, 2, 3] do
    x := x + y
  return x

List.count는 어떤 검사를 만족하는 리스트 원소의 수를 센다.

def List.count (p : α → Bool) (xs : List α) : Nat := Id.run do
  let mut found := 0
  for x in xs do
    if p x then found := found + 1
  return found

국소 가변 변수는 StateT를 명시적으로 국소 사용하기보다 편리하고 읽기 쉬울 수 있다. 그러나 명령형 언어의 제한 없는 가변 변수와 같은 모든 능력을 갖지는 않는다. 특히 변수가 도입된 do 블록 안에서만 수정할 수 있다. 따라서 예를 들어 for 반복문을 그와 동등한 재귀 보조 함수로 바꿀 수 없다. 다음 List.count 버전은

def List.count (p : α → Bool) (xs : List α) : Nat := Id.run do
  let mut found := 0
  let rec go : List α → Id Unit
    | [] => pure ()
    | y :: ys => do
      if p y then Variable `found` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `found`, consider using `let found` insteadfound := found + 1
      go ys
  return found

found를 수정하려 하면 다음 오류가 난다.

Variable `found` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `found`, consider using `let found` instead

재귀 함수가 항등 모나드로 작성되었고, 변수의 도입부가 있는 do 블록의 모나드만 StateT로 변환되기 때문이다.

6.4.5. What counts as a `do` block?🔗

do 표기의 많은 기능은 하나의 do 블록에만 적용된다. 조기 반환은 현재 블록을 종료하고, 가변 변수는 정의된 블록에서만 수정할 수 있다. 이를 효과적으로 사용하려면 무엇이 “같은 블록”으로 간주되는지 아는 것이 중요하다.

일반적으로 do 키워드 뒤의 들여쓰기 블록이 블록으로 간주되며, 그 바로 아래의 문장열은 해당 블록의 일부다. 블록 안에 들어 있더라도 독립된 블록의 문장은 그 블록의 일부로 간주되지 않는다. 그러나 정확히 무엇을 같은 블록으로 간주하는지를 정하는 규칙은 다소 미묘하므로 몇 가지 예를 살펴보자. 가변 변수를 가진 프로그램을 만들고 어디에서 변수가 수정되는지 확인하면 규칙의 정확한 성격을 시험할 수 있다. 다음 프로그램에는 가변 변수와 분명히 같은 블록에 있는 수정이 있다.

example : Id Unit := do
  let mut x := 0
  x := x + 1

:=를 사용해 이름을 정의하는 let 문의 일부인 do 블록에서 수정이 일어나면 그 수정은 해당 블록의 일부로 간주되지 않는다.

example : Id Unit := do
  let mut x := 0
  let other := do
    Variable `x` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `x`, consider using `let x` insteadx := x + 1
  other

Variable `x` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `x`, consider using `let x` instead

그러나 ←를 사용해 이름을 정의하는 let 문 아래의 do 블록은 주변 블록의 일부로 간주된다. 다음 프로그램은 받아들여진다.

example : Id Unit := do
  let mut x := 0
  let other ← do
    x := x + 1
  pure other

마찬가지로 함수의 인자로 나타나는 do 블록은 주변 블록과 독립적이다. 다음 프로그램은 받아들여지지 않는다.

example : Id Unit := do
  let mut x := 0
  let addFour (y : Id Nat) := Id.run y + 4
  addFour do
    Variable `x` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `x`, consider using `let x` insteadx := 5

Variable `x` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `x`, consider using `let x` instead

do 키워드가 완전히 불필요하다면 새 블록을 도입하지 않는다. 다음 프로그램은 받아들여지며 이 절의 첫 프로그램과 동등하다.

example : Id Unit := do
  let mut x := 0
  do x := x + 1

do 아래 분기의 내용(match나 if가 도입하는 분기 등)은 불필요한 do를 추가했는지와 관계없이 주변 블록의 일부로 간주된다. 다음 프로그램은 모두 받아들여진다.

example : Id Unit := do
  let mut x := 0
  if x > 2 then
    x := x + 1

example : Id Unit := do
  let mut x := 0
  if x > 2 then do
    x := x + 1

example : Id Unit := do
  let mut x := 0
  match true with
  | true => x := x + 1
  | false => x := 17

example : Id Unit := do
  let mut x := 0
  match true with
  | true => do
    x := x + 1
  | false => do
    x := 17

마찬가지로 for와 unless 문법의 일부로 나타나는 do는 해당 문법의 일부일 뿐이며 새로운 do 블록을 도입하지 않는다. 다음 프로그램도 받아들여진다.

example : Id Unit := do
  let mut x := 0
  for y in 1...5 do
   x := x + y

example : Id Unit := do
  let mut x := 0
  unless 1 < 5 do
    x := x + 1

6.4.6. Imperative or Functional Programming?🔗

Lean의 do 표기가 제공하는 명령형 기능 덕분에 많은 프로그램이 Rust, Java, C# 같은 언어의 대응 프로그램과 매우 비슷해진다. 이 유사성은 명령형 알고리즘을 Lean으로 옮길 때 편리하며, 어떤 작업은 명령형으로 생각하는 것이 가장 자연스럽다. 모나드와 모나드 변환기를 도입하면 순수 함수형 언어로 명령형 프로그램을 작성할 수 있다. (필요하면 국소적으로 변환되는) 모나드를 위한 특수 문법인 do 표기는 함수형 프로그래머가 두 방식의 장점을 모두 누리게 한다. 불변성이 주는 강한 추론 원리와 타입 시스템을 통한 효과 제어를, 효과를 사용하는 프로그램을 익숙하고 읽기 쉽게 만드는 문법·라이브러리와 결합한다. 모나드와 모나드 변환기를 사용하면 함수형 프로그래밍과 명령형 프로그래밍의 구분은 관점의 문제가 된다.

6.4.7. Exercises🔗

doList 함수 대신 for를 사용하도록 doug를 다시 작성하라.
이 절에서 소개한 기능으로 코드를 개선할 다른 기회가 있는가? 있다면 적용하라!