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-블록의 문(statement)인 경우에는, 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" 표현식은 "Hello, David"로 평가되며, 단순히 "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에 도달할 때까지만 순회하는 함수를 작성하려면 중간에 루프를 멈출 수단이 필요합니다. 이를 달성하는 한 가지 방법은 OptionT 모나드 트랜스포머와 함께 ForM을 사용하는 것입니다. 첫 번째 단계는 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
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
failurerange는 하한부터 상한까지 어떤 타입의 연속된 원소들의 나열을 나타냅니다. 경계는 open(열림)일 수 있으며 이 경우 경계는 범위에 포함되지 않고, closed(닫힘)일 수 있으며 이 경우 경계는 범위에 포함됩니다. 범위는 무한히 이어지거나 타입의 최솟값 또는 최댓값에 도달할 때까지 이어지는 형태로 상하한이 없을 수도 있습니다.
범위(range)는 경계를 나타내는 명명 규칙을 따르는 여러 타입들로 표현됩니다. 각 타입의 이름은 R로 시작하며, 그다음 두 글자가 각각 하한과 상한을 결정합니다:
-
o는 열린 경계(open bound)를 나타내며, 경계 값이 포함되지 않음을 의미합니다. -
c는 경계 값이 포함되는 닫힌 경계(closed bound)를 나타냅니다. -
i는 범위를 제한하지 않는 무한 경계를 나타냅니다.
예를 들어, Std.Rco Nat 타입은 하한을 포함하지만 상한을 제외하는 좌폐우개(left-closed right-open) 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 루프와 함께 범위(range)를 사용하여 해당 범위에서 값을 뽑아낼 수 있습니다. 이 프로그램은 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으로 도입합니다. 아무 이펙트도 도입하지 않으면서 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 found := found + 1
go ys
return found
found를 변경하려 시도하면 다음과 같은 오류가 발생합니다:
이는 재귀 함수가 항등 모나드로 작성되어 있고, 변수가 도입되는 do-블록의 모나드만 StateT로 변환되기 때문입니다.
6.4.5. do 블록으로 간주되는 것은 무엇입니까?
do-표기법의 많은 기능은 단일 do-블록에만 적용됩니다. 조기 반환은 현재 블록을 종료시키며, 가변 변수는 자신이 정의된 블록 내에서만 변경될 수 있습니다. 이를 효과적으로 사용하려면 무엇이 "같은 블록"으로 간주되는지 아는 것이 중요합니다.
일반적으로, do 키워드 뒤에 오는 들여쓰기 블록은 하나의 블록으로 취급되며, 그 바로 아래에 있는 일련의 문장들은 해당 블록의 일부입니다. 블록에 포함되어 있으면서도 독립적인 블록에 속한 문(statement)은 해당 블록의 일부로 간주되지 않습니다. 다만 정확히 무엇을 같은 블록으로 간주할지를 규정하는 규칙은 다소 미묘하므로, 몇 가지 예시를 살펴볼 필요가 있습니다. 이 규칙의 정확한 특성은 가변 변수를 사용하는 프로그램을 만들어 놓고 어디까지 변경이 허용되는지 확인함으로써 검증할 수 있습니다. 이 프로그램에는 가변 변수와 명백히 같은 블록에 있는 변경(mutation)이 포함되어 있습니다:
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를 다시 작성하십시오. -
이 절에서 소개한 기능을 사용하여 코드를 개선할 다른 기회가 있습니까? 그렇다면 사용하십시오!