Lean으로 하는 함수형 프로그래밍

2.2. 단계별로🔗

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. 표준 입출력🔗

첫 번째 줄은 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입니다. 그러면 표준 입력은 나머지 do 블록 동안 화살표 왼쪽의 이름(여기서는 stdin)과 연결됩니다.

두 번째 줄인 let stdout ← IO.getStdout를 실행하는 과정도 이와 유사하게 진행됩니다. 먼저 IO.getStdout 표현식이 평가되어 표준 출력을 반환할 IO 액션이 산출됩니다. 다음으로, 이 액션이 실행되어 실제로 표준 출력을 반환합니다. 마지막으로 이 값은 do 블록의 나머지 부분에서 stdout이라는 이름과 연결됩니다.

2.2.2. 질문하기🔗

이제 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. 사용자에게 인사하기🔗

do 블록에서 실행할 것으로 남은 것은 단일 문장뿐입니다:

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

putStrLn의 문자열 인수는 문자열 보간을 통해 구성되며, 그 결과로 "Hello, David!" 문자열이 생성됩니다. 이 문장은 표현식이므로, 표준 출력에 이 문자열을 줄바꿈과 함께 출력할 IO 액션을 산출하도록 평가됩니다. 표현식이 평가되고 나면, 그 결과로 나온 IO 액션이 실행되어 인사말이 출력됩니다.

2.2.4. 값으로서의 IO 액션🔗

위 설명만으로는 표현식을 평가하는 것과 IO 액션을 실행하는 것 사이의 구분이 왜 필요한지 알기 어려울 수 있습니다. 결국 각 액션은 생성된 직후 즉시 실행됩니다. 다른 언어에서 하듯이 평가 도중에 그냥 효과를 수행하지 않는 이유는 무엇일까요?

그 답은 두 가지입니다. 첫째로, 평가(evaluation)와 실행(execution)을 분리한다는 것은 프로그램이 어떤 함수가 부수 효과(side effect)를 가질 수 있는지를 명시적으로 나타내야 한다는 것을 의미합니다. 프로그램에서 효과가 없는 부분은 프로그래머의 머릿속에서든 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을 받아 각 Nat마다 하나씩, 아직 실행되지 않은 IO 액션의 리스트를 반환합니다:

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
6

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

이 프로그램을 실행하면 다음과 같은 출력이 나타납니다.

countdown5 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. 연습문제🔗

다음 프로그램의 실행 과정을 종이에 단계별로 적어 보십시오:

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

프로그램의 실행을 단계별로 살펴보면서, 표현식이 평가되는 시점과 IO 액션이 실행되는 시점을 파악하십시오. IO 액션을 실행하면 부수 효과가 발생하는데, 이를 기록해 두십시오. 이 작업을 마친 후, Lean으로 프로그램을 실행하여 부작용에 대한 여러분의 예측이 올바른지 다시 확인해 보십시오.