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의 분기(branch)에서 끌어올려질 수 없습니다.
이것이 혼란스러울 수 있는 예시를 살펴보기 위해, 실행되었음을 세상에 알린 후 데이터를 반환하는 다음과 같은 헬퍼 정의를 생각해 보십시오:
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이 제공된 표현식을 평가하고, 그 결과값을 문자열로 변환한 다음, 해당 문자열을 툴팁과 정보 창에 제공합니다. IO 액션을 문자열로 변환할 수 없기 때문에 실패하는 대신, #eval은 이를 실행하여 부작용을 수행합니다. 실행 결과가 Unit 값 ()인 경우 결과 문자열이 표시되지 않지만, 문자열로 변환할 수 있는 타입인 경우에는 Lean이 결과값을 표시합니다.
이것은 IO 액션 자체를 나타내는 불투명한 표현이 아니라, 그 액션을 실행하여 만들어진 출력입니다. 다시 말해, IO 동작에 대해 #eval은 제공된 식을 평가하는 동시에 그 결과로 나온 동작 값을 실행합니다.
#eval을 사용해 IO 동작을 빠르게 테스트하는 것은 전체 프로그램을 컴파일하고 실행하는 것보다 훨씬 편리할 수 있습니다. 하지만 몇 가지 제약이 있습니다. 예를 들어, 표준 입력으로부터 읽어 들이면 단순히 빈 입력을 반환합니다. 또한 Lean이 사용자에게 제공하는 진단 정보를 업데이트해야 할 때마다 IO 액션이 재실행되며, 이는 예측할 수 없는 시점에 발생할 수 있습니다. 예를 들어 파일을 읽고 쓰는 동작은 예상치 못한 방식으로 그렇게 할 수 있습니다.