2.5. Additional Conveniences
2.5.1. Nested Actions
feline의 많은 함수에는 IO 동작의 결과에 이름을 붙인 뒤 즉시 한 번만 사용하는 반복적인 패턴이 나타난다.
예를 들어 dump에서는 다음과 같다:
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
let stdout ← IO.getStdout
stdout.write buf
dump stream
stdout에 이 패턴이 나타난다:
let stdout ← IO.getStdout
stdout.write buf
마찬가지로 fileStream에는 다음 코드 조각이 들어 있다:
let fileExists ← filename.pathExists
if not fileExists then
Lean이 do 블록을 컴파일할 때 괄호 바로 아래에 있는 왼쪽 화살표로 이루어진 식은 가장 가까운 바깥쪽 do로 끌어 올려지고, 그 결과는 고유한 이름에 바인딩된다.
이 고유한 이름은 식이 있던 자리를 대신한다.
따라서 dump를 다음과 같이 작성할 수도 있다:
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
(← IO.getStdout).write buf
dump stream
이 버전의 dump는 한 번만 사용하는 이름을 도입하지 않으므로 프로그램을 크게 단순화할 수 있다.
Lean이 중첩된 식의 문맥에서 끌어 올린 IO 동작을 중첩 동작이라고 한다.
같은 기법으로 fileStream도 단순화할 수 있다:
def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
if not (← filename.pathExists) then
(← IO.getStderr).putStrLn s!"File not found: {filename}"
pure none
else
let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
pure (some (IO.FS.Stream.ofHandle handle))
이 경우에도 중첩 동작을 사용해 handle라는 지역 이름을 없앨 수 있지만, 그 결과 식이 길고 복잡해진다.
중첩 동작을 사용하는 것이 흔히 좋은 방식이기는 해도, 중간 결과에 이름을 붙이는 편이 도움이 될 때도 있다.
하지만 중첩 동작은 주변 do 블록에 있는 IO 동작을 짧게 표기한 것일 뿐이라는 점을 기억해야 한다.
동작을 실행할 때 발생하는 부수 효과는 여전히 같은 순서로 일어나며, 부수 효과의 실행이 식의 평가와 뒤섞이지도 않는다.
따라서 if의 분기에서는 중첩 동작을 끌어 올릴 수 없다.
이 점이 혼란스러울 수 있는 예로, 실행되었다는 사실을 세상에 알린 뒤 데이터를 반환하는 다음 보조 정의를 살펴보자:
def getNumA : IO Nat := do
(← IO.getStdout).putStrLn "A"
pure 5def getNumB : IO Nat := do
(← IO.getStdout).putStrLn "B"
pure 7
이 정의들은 사용자 입력을 검증하거나 데이터베이스를 읽거나 파일을 여는 더 복잡한 IO 코드를 대신한다고 생각하자.
숫자 A가 5이면 0을 출력하고, 그렇지 않으면 숫자 B를 출력하는 프로그램은 다음과 같이 작성할 수 있다:
def test : IO Unit := do
let a : Nat := if (← getNumA) == 5 then 0 else (← getNumB)
(← IO.getStdout).putStrLn s!"The answer is {a}"이 프로그램은 다음 프로그램과 동등하다:
def test : IO Unit := do
let x ← getNumA
let y ← getNumB
let a : Nat := if x == 5 then 0 else y
(← IO.getStdout).putStrLn s!"The answer is {a}"
이 프로그램은 getNumA의 결과가 5와 같은지와 관계없이 getNumB를 실행한다.
이런 혼란을 막기 위해 do 안의 한 줄 자체가 아닌 if에서는 중첩 동작을 사용할 수 없으며, 다음 오류 메시지가 나온다:
2.5.2. Flexible Layouts for do
Lean에서 do 식은 공백에 민감하다.
do 안의 각 IO 동작이나 지역 바인딩은 각각 자신의 줄에서 시작해야 하며, 모두 같은 들여쓰기를 사용해야 한다.
거의 모든 do 사용은 이렇게 작성해야 한다.
하지만 드물게 공백과 들여쓰기를 수동으로 제어해야 하거나, 여러 작은 동작을 한 줄에 두는 편이 편리할 때가 있다.
이 경우 줄 바꿈은 세미콜론으로, 들여쓰기는 중괄호로 바꿀 수 있다.
예를 들어 다음 프로그램은 모두 동등하다:
-- 이 버전은 공백에 민감한 배치만 사용한다
def main : IO Unit := do
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let name := (← stdin.getLine).trimAscii
stdout.putStrLn s!"Hello, {name}!"-- 이 버전은 가능한 한 명시적으로 작성했다
def main : IO Unit := do {
let stdin ← IO.getStdin;
let stdout ← IO.getStdout;
stdout.putStrLn "How would you like to be addressed?";
let name := (← stdin.getLine).trimAscii;
stdout.putStrLn s!"Hello, {name}!"
}-- 이 버전은 세미콜론으로 두 동작을 같은 줄에 둔다
def main : IO Unit := do
let stdin ← IO.getStdin; let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let name := (← stdin.getLine).trimAscii
stdout.putStrLn s!"Hello, {name}!"
관용적인 Lean 코드에서는 do와 함께 중괄호를 사용하는 일이 매우 드물다.
2.5.3. Running IO Actions With #eval
Lean의 #eval 명령은 IO 동작을 단순히 평가하는 대신 실행하는 데 사용할 수 있다.
보통 Lean 파일에 #eval 명령을 추가하면 Lean은 주어진 식을 평가하고, 결과값을 문자열로 변환한 뒤, 그 문자열을 도구 설명과 정보 창에 제공한다.
IO 동작을 문자열로 변환할 수 없어 실패하는 대신, #eval은 동작을 실행해 부수 효과를 수행한다.
실행 결과가 Unit 값 ()이면 결과 문자열을 표시하지 않지만, 문자열로 변환할 수 있는 타입이면 Lean이 결과값을 표시한다.
이는 동작 자체의 불투명한 표현이 아니라 IO 동작을 실행해서 나온 출력이다.
다시 말해 IO 동작에 대해 #eval은 주어진 식을 평가하고 그 결과 동작 값을 실행하기도 한다.
#eval으로 IO 동작을 빠르게 테스트하면 전체 프로그램을 컴파일하고 실행하는 것보다 훨씬 편리할 수 있다.
하지만 몇 가지 제한이 있다.
예를 들어 표준 입력을 읽으면 단순히 빈 입력을 반환한다.
또한 Lean이 사용자에게 제공하는 진단 정보를 갱신해야 할 때마다 IO 동작을 다시 실행하며, 이는 예측할 수 없는 시점에 일어날 수 있다.
예를 들어 파일을 읽고 쓰는 동작이 예상치 않게 파일을 읽거나 쓸 수 있다.