2.2. Step By Step🔗

do 블록은 한 번에 한 줄씩 실행할 수 있다. 앞 절의 프로그램에서 시작하자:

let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropEndWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"

2.2.1. Standard IO🔗

첫 번째 줄은 let stdin ← IO.getStdin이고, 나머지는 다음과 같다:

let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropEndWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"

←를 사용하는 let 문을 실행하려면 먼저 화살표 오른쪽의 식(이 경우 IO.getStdin)을 평가한다. 이 식은 단순한 변수이므로 그 값을 조회한다. 그 결과는 내장 원시 IO 동작이다. 다음으로 이 IO 동작을 실행하면, IO.FS.Stream 타입인 표준 입력 스트림을 나타내는 값이 나온다. 그런 다음 표준 입력을 화살표 왼쪽의 이름(여기서는 stdin)에 do 블록의 나머지 부분 동안 연결한다.

두 번째 줄인 let stdout ← IO.getStdout도 비슷하게 진행된다. 먼저 IO.getStdout 식을 평가해 표준 출력을 반환할 IO 동작을 얻는다. 다음으로 이 동작을 실행해 실제로 표준 출력을 반환한다. 마지막으로 이 값을 do 블록의 나머지 부분 동안 stdout이라는 이름에 연결한다.

2.2.2. Asking a Question🔗

이제 stdin과 stdout을 찾았으므로 블록의 나머지는 질문과 답으로 이루어진다:

stdout.putStrLn "How would you like to be addressed?"
let input ← stdin.getLine
let name := input.dropEndWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"

블록의 첫 문장인 stdout.putStrLn "How would you like to be addressed?"은 하나의 식으로 이루어진다. 식을 실행하려면 먼저 평가해야 한다. 이 경우 IO.FS.Stream.putStrLn의 타입은 IO.FS.Stream → String → IO Unit이다. 즉 스트림과 문자열을 받아 IO 동작을 반환하는 함수다. 이 식은 함수 호출에 접근자 표기법을 사용한다. 이 함수에는 표준 출력 스트림과 문자열이라는 두 인수를 적용한다. 식의 값은 문자열과 줄 바꿈 문자를 출력 스트림에 쓸 IO 동작이다. 이 값을 얻었으므로 다음 단계는 이를 실행하는 것이며, 그러면 문자열과 줄 바꿈이 실제로 stdout에 기록된다. 식만으로 이루어진 문장은 새 변수를 도입하지 않는다.

블록의 다음 문장은 let input ← stdin.getLine이다. IO.FS.Stream.getLine의 타입은 IO.FS.Stream → IO String이므로, 스트림에서 문자열을 반환할 IO 동작으로 가는 함수다. 다시 말해 접근자 표기법의 예다. 이 IO 동작을 실행하면 프로그램은 사용자가 입력 한 줄을 완전히 입력할 때까지 기다린다. 사용자가 “David”라고 쓴다고 하자. 그 결과로 얻은 줄("David\n")을 input에 연결하며, 여기서 이스케이프 시퀀스 \n은 줄 바꿈 문자를 나타낸다.

let name := input.dropEndWhile Char.isWhitespace
stdout.putStrLn s!"Hello, {name}!"

다음 줄인 let name := input.dropEndWhile Char.isWhitespace는 let 문이다. 이 프로그램의 다른 let 문과 달리 ← 대신 :=를 사용한다. 이는 식은 평가하지만 그 결과값이 IO 동작일 필요는 없고 실행하지도 않는다는 뜻이다. 이 경우 String.dropEndWhile은 문자열과 패턴을 받아, 문자열 끝에서 패턴과 일치하는 모든 부분 문자열을 제거한 문자열 슬라이스를 반환한다. 예를 들어,

#eval "Hello!!!".dropEndWhile (· == '!')

다음 결과를 낸다.

Hello

그리고

#eval "Hello... ".dropEndWhile (fun c => not (c.isAlphanum))

다음 결과를 낸다.

Hello

이 결과에서는 문자열 오른쪽에서 영숫자가 아닌 문자가 모두 제거되었다. 현재 프로그램 줄에서는 줄 바꿈을 포함한 공백 문자를 입력 문자열 오른쪽에서 제거해 David를 얻고, 이를 블록의 나머지 부분 동안 name에 연결한다.

2.2.3. Greeting the User🔗

do 블록에서 실행할 것이 이제 한 문장만 남았다:

stdout.putStrLn s!"Hello, {name}!"

putStrLn의 문자열 인수는 문자열 보간으로 구성되어 "Hello, David!" 문자열을 만든다. 이 문장은 식이므로 평가하면 이 문자열을 줄 바꿈과 함께 표준 출력에 출력할 IO 동작이 나온다. 식을 평가한 뒤 결과로 얻은 IO 동작을 실행하면 인사가 출력된다.

2.2.4. `IO` Actions as Values🔗

위 설명만으로는 식을 평가하는 것과 IO 동작을 실행하는 것을 구분해야 하는 이유가 잘 보이지 않을 수 있다. 어차피 각 동작은 만들어지자마자 바로 실행되기 때문이다. 다른 언어에서 하듯 평가 중에 효과를 바로 수행하면 되지 않을까?

답은 두 가지다. 첫째, 평가와 실행을 분리하면 프로그램에서 어떤 함수가 부수 효과를 일으킬 수 있는지 명시해야 한다. 효과가 없는 프로그램 부분은 프로그래머의 머릿속에서든 Lean의 형식 증명 기능을 사용해서든 수학적으로 추론하기가 훨씬 쉬우므로, 이러한 분리는 버그를 더 쉽게 피하게 해 준다. 둘째, 모든 IO 동작을 생겨나는 즉시 실행할 필요는 없다. 동작을 수행하지 않고 언급할 수 있으므로 일반 함수를 제어 구조로 사용할 수 있다.

예를 들어 twice 함수는 IO 동작을 인수로 받아 그 동작을 두 번 실행할 새 동작을 반환한다.

def twice (action : IO Unit) : IO Unit := do
  action
  action

다음을 실행하면

twice (IO.println "shy")

다음 결과가 나온다.

shy
shy

이 내용이 출력된다. 이를 일반화하면 기반 동작을 임의의 횟수만큼 실행하는 버전을 만들 수 있다:

def nTimes (action : IO Unit) : Nat → IO Unit
  | 0 => pure ()
  | n + 1 => do
    action
    nTimes action n

Nat.zero의 기본 경우 결과는 pure ()다. pure 함수는 부수 효과가 없지만 pure의 인수를 반환하는 IO 동작을 만든다. 여기서는 그 인수가 Unit의 생성자다. 아무것도 하지 않고 흥미로운 것도 반환하지 않는 동작인 pure ()는 한편으로는 지극히 따분하지만 다른 한편으로는 매우 유용하다. 재귀 단계에서는 do 블록으로 먼저 action을 실행하고 그다음 재귀 호출의 결과를 실행하는 동작을 만든다. Hello Hello Hello #eval nTimes (IO.println "Hello") 3을 실행하면 다음 출력이 나온다:

Hello
Hello
Hello

함수를 제어 구조로 사용할 수 있을 뿐 아니라 IO 동작이 일급 값이라는 사실 덕분에 나중에 실행할 수 있도록 자료 구조에 저장할 수도 있다. 예를 들어 countdown 함수는 Nat을 받아 아직 실행하지 않은 IO 동작의 목록을 반환하며, 각 Nat마다 하나씩 들어 있다:

def countdown : Nat → List (IO Unit)
  | 0 => [IO.println "Blast off!"]
  | n + 1 => IO.println s!"{n + 1}" :: countdown n

이 함수에는 부수 효과가 없으며 아무것도 출력하지 않는다. 예를 들어 인수에 적용한 뒤 결과 동작 목록의 길이를 확인할 수 있다:

def from5 : List (IO Unit) := countdown 5

이 목록에는 원소가 여섯 개 있다(각 숫자에 하나씩이고, 0에 해당하는 "Blast off!" 동작이 하나 더 있다):

#eval from5.length

runActions 함수는 동작 목록을 받아 이를 순서대로 모두 실행하는 하나의 동작을 만든다:

def runActions : List (IO Unit) → IO Unit
  | [] => pure ()
  | act :: actions => do
    act
    runActions actions

그 구조는 nTimes와 본질적으로 같지만, Nat.succ마다 하나의 동작을 실행하는 대신 각 List.cons 아래의 동작을 실행한다. 마찬가지로 runActions 자체가 동작을 실행하지는 않는다. 동작을 실행할 새 동작을 만들며, 그 동작은 main의 일부로 실행될 위치에 놓아야 한다:

def main : IO Unit := runActions from5

이 프로그램을 실행하면 다음 출력이 나온다:

countdown

5
4
3
2
1
Blast off!

이 프로그램을 실행하면 어떤 일이 일어날까? 첫 단계는 main을 평가하는 것이다. 다음과 같이 진행된다:

                  mainrunActions from5runActions (countdown 5)runActions
  [IO.println "5",
   IO.println "4",
   IO.println "3",
   IO.println "2",
   IO.println "1",
   IO.println "Blast off!"]do IO.println "5"
   IO.println "4"
   IO.println "3"
   IO.println "2"
   IO.println "1"
   IO.println "Blast off!"
   pure ()

그 결과로 얻은 IO 동작은 do 블록이다. 그다음 do 블록의 각 단계를 한 번에 하나씩 실행하면 예상한 출력이 나온다. 마지막 단계인 pure ()에는 효과가 없으며, runActions 정의에 기본 경우가 필요하기 때문에 들어 있을 뿐이다.

2.2.5. Exercise🔗

다음 프로그램의 실행 과정을 종이에 한 단계씩 적어 가며 추적하라:

def main : IO Unit := do
  let englishGreeting := IO.println "Hello!"
  IO.println "Bonjour!"
  englishGreeting

프로그램의 실행을 추적하면서 식을 평가하는 때와 IO 동작을 실행하는 때를 식별하라. IO 동작을 실행해 부수 효과가 발생하면 이를 기록하라. 그런 다음 Lean으로 프로그램을 실행해 부수 효과에 대한 예측이 맞았는지 다시 확인하라.