6.4. do의 추가 기능
Lean의 do-표기법은 모나드를 사용하는 프로그램을 명령형 프로그래밍 언어와 비슷한 문법으로 작성할 수 있게 해 줍니다. do-표기법은 모나드를 사용하는 프로그램을 위한 편리한 문법을 제공할 뿐만 아니라, 특정 모나드 트랜스포머를 사용하기 위한 문법도 제공합니다.
6.4.1. 단일 분기 if
모나드 안에서 작업할 때 흔히 쓰는 패턴은 어떤 조건이 참일 때만 부수 효과를 수행하는 것입니다. 예를 들어 countLetters는 글자가 모음인지 자음인지 검사하며, 둘 다 아닌 글자는 상태에 아무런 영향을 주지 않습니다. 이는 else 분기가 아무런 효과도 없는 pure ()로 평가되도록 하는 방식으로 표현됩니다:
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 -- modified or non-English letter
pure ()
else throw (.notALetter c)
loop cs
loop str.toList
if가 표현식이 아니라 do 블록 안의 문장으로 쓰일 때는 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-블록을 자동으로 재작성하여, 해당 do-블록이 작성된 모나드 위에 지역 트랜스포머를 추가해야 합니다.
6.4.2. 조기 반환
표준 라이브러리에는 리스트에서 특정 검사를 통과하는 첫 번째 항목을 반환하는 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
명령형 언어의 조기 반환(early return)은 현재 스택 프레임만 해제할 수 있는 예외와 다소 비슷합니다. 조기 반환과 예외는 모두 코드 블록의 실행을 종료하며, 사실상 주변 코드를 던져진 값으로 대체합니다. 내부적으로 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. 반복문
가변 상태를 가진 모든 프로그램을 상태를 인자로 전달하는 프로그램으로 다시 작성할 수 있듯이, 모든 반복문은 재귀 함수로 다시 작성할 수 있습니다. 한편으로 보면 List.find?는 재귀 함수로 볼 때 가장 명확합니다. 무엇보다 그 정의가 리스트의 구조를 그대로 반영하기 때문입니다. 머리가 검사를 통과하면 그것을 반환해야 하고, 그렇지 않으면 꼬리에서 찾아야 합니다. 더 이상 남은 항목이 없으면 답은 none입니다. 다른 한편으로 보면 List.find?는 반복문으로 볼 때 가장 명확합니다. 무엇보다 이 프로그램은 조건을 만족하는 항목을 찾을 때까지 항목을 차례로 살펴보고, 찾으면 그 시점에 종료하기 때문입니다. 반복문이 값을 반환하지 않은 채 종료되면 답은 none입니다.
6.4.3.1. 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
5보다 작은 각 수에 대해 IO.println을 실행하는 작업은 ForM으로 수행할 수 있습니다:
#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 파일의 내용은 다음과 같습니다:
test-dataHello!!!!!!12345abc123Ok
ForMIO.lean에 저장된 이 프로그램을 실행하면 다음과 같은 결과가 출력됩니다.
lean --run ForMIO.lean < test-dataHello!
abc123
Ok
6.4.3.2. 반복 중단하기
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)간단한 테스트를 통해 이 해법이 작동함을 확인할 수 있습니다:
#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테스트해 보면 이전 버전과 똑같이 동작함을 확인할 수 있습니다:
#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
for 루프는 break 외에도 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) 경계일 수도 있습니다. 열린 경계는 범위에 포함되지 않고, 닫힌 경계는 범위에 포함됩니다. 범위에는 경계가 없을 수도 있습니다. 이 경우 범위는 무한히 이어지거나, 해당 타입의 최솟값 또는 최댓값에 도달할 때까지 이어집니다.
범위(range)는 여러 타입으로 표현되며, 이 타입들은 각 범위의 경계를 나타내는 명명 규칙을 따릅니다. 각 타입의 이름은 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)실행하면 다음과 같은 결과가 나옵니다:
다음 코드는 'l'부터 'p'까지의 문자를 표시합니다:
#eval do
for letter in 'l'...='p' do
IO.println letter
마지막으로, for 루프는 in 절을 쉼표로 구분하여 여러 컬렉션을 병렬로 순회할 수 있습니다. 루프는 첫 번째 컬렉션의 원소가 모두 소진되면 멈추므로, 다음 선언은:
def parallelLoop := do
for x in ["currant", "gooseberry", "rowan"], y in 'a'...'e' do
IO.println (x, y)다음 세 줄을 출력합니다:
#eval parallelLoop
많은 자료 구조는 원소가 컬렉션에서 꺼내졌다는 근거를 루프 본문에 추가로 제공하는, 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. 가변 변수
조기 return, else가 없는 if, for 루프 외에도 Lean은 do 블록 안에서 지역 가변 변수를 지원합니다. 내부적으로 이러한 가변 변수는 실제 가변 변수로 구현되는 것이 아니라 StateT와 동등한 코드로 디슈거링됩니다. 이번에도 함수형 프로그래밍을 사용해 명령형 프로그래밍을 흉내 냅니다.
지역 가변 변수는 일반 let 대신 let mut으로 도입합니다. 항등 모나드 Id를 사용해 아무런 효과도 도입하지 않고 do-문법을 쓸 수 있게 한 정의 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 found := found + 1
go ys
return found
found를 변경하려고 하면 다음과 같은 오류가 발생합니다:
이는 재귀 함수가 항등 모나드에서 작성되었고, 변수가 도입된 do-블록의 모나드만 StateT로 변환되기 때문입니다.
6.4.5. 무엇이 do 블록으로 간주됩니까?
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
x := x + 1
other
하지만 ←를 사용해 이름을 정의하는 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
x := 5
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 + 1example : Id Unit := do
let mut x := 0
if x > 2 then do
x := x + 1example : Id Unit := do
let mut x := 0
match true with
| true => x := x + 1
| false => x := 17example : 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 + yexample : Id Unit := do
let mut x := 0
unless 1 < 5 do
x := x + 16.4.6. 명령형 프로그래밍인가, 함수형 프로그래밍인가?
Lean의 do 표기법이 제공하는 명령형 기능 덕분에 많은 프로그램을 Rust, Java, C# 같은 언어로 작성한 대응 프로그램과 매우 비슷하게 작성할 수 있습니다. 이러한 유사성은 명령형 알고리즘을 Lean으로 옮길 때 매우 편리하며, 어떤 작업은 그저 명령형으로 생각하는 것이 가장 자연스럽습니다. 모나드와 모나드 트랜스포머의 도입으로 순수 함수형 언어에서도 명령형 프로그램을 작성할 수 있게 되었으며, (지역적으로 변환되었을 수도 있는) 모나드를 위한 전용 문법인 do 표기법 덕분에 함수형 프로그래머는 두 세계의 장점을 모두 누릴 수 있습니다. 즉, 불변성이 제공하는 강력한 추론 원리와 타입 시스템을 통한 사용 가능한 효과의 엄격한 제어가, 효과를 사용하는 프로그램을 익숙하고 읽기 쉽게 만들어 주는 문법 및 라이브러리와 결합됩니다. 모나드와 모나드 트랜스포머 덕분에 함수형 프로그래밍과 명령형 프로그래밍의 구분은 관점의 문제가 됩니다.
6.4.7. 연습 문제
-
doList함수 대신for를 사용하도록doug를 다시 작성하십시오. -
이 절에서 소개한 기능을 사용해 코드를 개선할 수 있는 다른 부분이 있습니까? 있다면 그 기능을 사용해 보십시오!