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 액션을 실행하는 것을 왜 구분해야 하는지 이해하기 어려울 수 있습니다. 어차피 각 액션은 만들어지자마자 곧바로 실행됩니다. 다른 언어에서처럼 평가하는 동안 그냥 효과를 수행하면 되지 않겠습니까?

답은 두 가지입니다. 첫째, 평가와 실행을 분리하면 어떤 함수가 부수 효과를 가질 수 있는지를 프로그램에 명시적으로 드러내야 합니다. 프로그램에서 효과가 없는 부분은 프로그래머가 머릿속으로 따지든 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으로 프로그램을 실행하여 부수 효과에 대한 예측이 맞았는지 다시 확인하십시오.