2.5. 추가 편의 기능
2.5.1. 중첩된 액션
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. do를 위한 유연한 레이아웃
Lean에서 do 표현식은 공백에 민감합니다. do 안의 각 IO 액션이나 지역 바인딩은 각자 별도의 줄에서 시작해야 하며, 모두 같은 들여쓰기를 가져야 합니다. do는 거의 모든 경우 이와 같이 작성해야 합니다. 하지만 드물게는 공백과 들여쓰기를 직접 제어해야 할 때가 있으며, 작은 액션 여러 개를 한 줄에 두는 것이 편리할 때도 있습니다. 이러한 경우에는 줄바꿈을 세미콜론으로, 들여쓰기를 중괄호로 대신할 수 있습니다.
예를 들어, 다음 프로그램들은 모두 동등합니다:
-- This version uses only whitespace-sensitive layout
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}!"-- This version is as explicit as possible
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}!"
}-- This version uses a semicolon to put two actions on the same line
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. #eval로 IO 액션 실행하기
Lean의 #eval 명령은 IO 액션을 단순히 평가하는 데 그치지 않고 실행하는 데 사용할 수 있습니다. 일반적으로 Lean 파일에 #eval 명령을 추가하면 Lean은 주어진 표현식을 평가하고, 그 결과값을 문자열로 변환한 다음, 해당 문자열을 툴팁과 정보 창에 표시합니다. #eval은 IO 액션을 문자열로 변환할 수 없다는 이유로 실패하는 대신, 액션을 실행하여 그 부수 효과를 수행합니다. 실행 결과가 Unit 값인 ()이면 결과 문자열이 표시되지 않지만, 결과가 문자열로 변환할 수 있는 타입이면 Lean은 그 결과값을 표시합니다.
이것은 IO 액션 자체를 나타내는 불투명한 표현이 아니라, 그 액션을 실행하여 생성된 출력입니다. 다시 말해, IO 액션에 대해 #eval은 주어진 표현식을 평가하는 동시에 그 결과로 나온 액션 값을 실행합니다.
IO 액션을 #eval로 빠르게 테스트하는 방식은 전체 프로그램을 컴파일하고 실행하는 방식보다 훨씬 편리할 수 있습니다. 하지만 몇 가지 제약이 있습니다. 예를 들어, 표준 입력에서 읽으면 그냥 빈 입력이 반환됩니다. 또한 IO 액션은 Lean이 사용자에게 제공하는 진단 정보를 갱신해야 할 때마다 다시 실행되며, 이는 예측할 수 없는 시점에 일어날 수 있습니다. 예를 들어, 파일을 읽고 쓰는 액션은 예상치 못한 때에 파일을 읽고 쓸 수 있습니다.