Lean으로 배우는 함수형 프로그래밍

2.1. 프로그램 실행하기🔗

Lean 프로그램을 실행하는 가장 간단한 방법은 Lean 실행 파일에 --run 옵션을 지정하는 것입니다. Hello.lean이라는 파일을 만들고 다음 내용을 입력하십시오.

def main : IO Unit := IO.println "Hello, world!"

그런 다음 명령줄에서 다음을 실행하십시오:

$ lean --run Hello.lean

이 프로그램은 Hello, world!을 출력하고 종료합니다.

2.1.1. 인사말 프로그램의 구조🔗

Lean을 --run 옵션과 함께 실행하면 Lean은 프로그램의 main 정의를 호출합니다. 명령줄 인자를 받지 않는 프로그램에서 main의 타입은 IO Unit이어야 합니다. 이는 main이 함수가 아니라는 뜻인데, 그 타입에 화살표(→)가 없기 때문입니다. main은 부수 효과를 일으키는 함수가 아니라, 수행할 효과들에 대한 기술로 이루어져 있습니다.

앞 장에서 다룬 것처럼, Unit은 가장 단순한 귀납적 타입입니다. 이 타입에는 인자를 받지 않는 unit이라는 생성자 하나만 있습니다. C 계열 언어에는 아무 값도 반환하지 않는 void 함수라는 개념이 있습니다. Lean에서는 모든 함수가 인자를 받고 값을 반환하며, 의미 있는 인자나 반환값이 없다는 것은 대신 Unit 타입을 사용하여 나타낼 수 있습니다. Bool이 1비트의 정보를 나타낸다면, Unit은 0비트의 정보를 나타냅니다.

IO α는 실행되면 예외를 던지거나 α 타입의 값을 반환하는 프로그램의 타입입니다. 이 프로그램은 실행 도중 부수 효과를 일으킬 수 있습니다. 이러한 프로그램을 IO 액션이라고 부릅니다. Lean은 표현식의 평가와 IO 액션의 실행을 구분합니다. 평가는 변수에 값을 대입하고 부수 효과 없이 하위 표현식을 축약하는 수학적 모델을 엄격히 따르는 반면, 실행은 외부 시스템에 의존하여 세상과 상호작용합니다. IO.println은 문자열을 받아 IO 액션을 반환하는 함수이며, 이 액션은 실행되면 주어진 문자열을 표준 출력에 씁니다. 이 액션은 문자열을 내보내는 과정에서 환경으로부터 딱히 의미 있는 정보를 읽어 오지 않으므로, IO.println의 타입은 String → IO Unit입니다. 만약 이 액션이 의미 있는 무언가를 반환한다면, 그 사실은 IO 액션의 타입이 Unit이 아닌 다른 타입이라는 점으로 드러날 것입니다.

2.1.2. 함수형 프로그래밍 대 부수 효과🔗

Lean의 계산 모델은 수학적 표현식의 평가에 기반하며, 여기서 변수에는 시간이 지나도 변하지 않는 값이 정확히 하나 주어집니다. 표현식을 평가한 결과는 변하지 않으며, 같은 표현식을 다시 평가하면 항상 같은 결과가 나옵니다.

반면에 유용한 프로그램은 외부 세계와 상호작용해야 합니다. 입력도 출력도 하지 않는 프로그램은 사용자에게 데이터를 요청하거나, 디스크에 파일을 만들거나, 네트워크 연결을 열 수 없습니다. Lean은 Lean 자신으로 작성되었으며, Lean 컴파일러는 당연히 파일을 읽고, 파일을 만들고, 텍스트 편집기와 상호작용합니다. 같은 표현식이 항상 같은 결과를 내는 언어가 디스크에서 파일을 읽는 프로그램을 어떻게 지원할 수 있을까요? 그 파일의 내용은 시간이 지나면서 바뀔 수도 있는데 말입니다.

이 겉보기 모순은 부수 효과를 조금 다르게 생각하면 해결할 수 있습니다. 커피와 샌드위치를 파는 카페를 상상해 보십시오. 이 카페에는 직원이 두 명 있습니다. 한 명은 주문을 처리하는 요리사이고, 다른 한 명은 카운터에서 손님을 응대하며 주문서를 넣는 직원입니다. 요리사는 무뚝뚝한 사람으로, 바깥세상과는 어떤 접촉도 하지 않기를 무척 바라지만, 이 카페를 유명하게 만든 음식과 음료를 한결같이 만들어 내는 데에는 아주 뛰어납니다. 하지만 그렇게 하려면 요리사에게는 평화와 고요가 필요하며, 대화로 방해를 받아서는 안 됩니다. 카운터 직원은 친절하지만 주방 일에는 전혀 소질이 없습니다. 손님은 카운터 직원과 소통하고, 카운터 직원은 실제 요리를 모두 요리사에게 맡깁니다. 알레르기 여부를 확인하는 것처럼 요리사가 손님에게 물어볼 것이 있으면, 요리사는 카운터 직원에게 작은 쪽지를 보냅니다. 그러면 카운터 직원이 손님과 이야기한 뒤 그 결과를 적은 쪽지를 요리사에게 다시 전달합니다.

이 비유에서 요리사는 Lean 언어에 해당합니다. 요리사는 주문을 받으면 요청받은 것을 충실하고 일관되게 만들어 냅니다. 카운터 직원은 바깥 세계와 상호 작용하며 결제를 받고, 음식을 내주고, 손님과 대화를 나눌 수 있는 주변 런타임 시스템입니다. 두 직원은 함께 일하면서 식당의 모든 기능(함수)을 해내지만, 각자의 책임은 나뉘어 있으며 각자가 가장 잘하는 일을 맡아 수행합니다. 손님을 멀리함으로써 요리사가 정말 훌륭한 커피와 샌드위치를 만드는 데 집중할 수 있는 것처럼, Lean에 부수 효과가 없기 때문에 프로그램을 형식적인 수학적 증명의 일부로 사용할 수 있습니다. 또한 구성 요소 사이에 미묘한 결합을 만들어 내는 숨겨진 상태 변경이 없으므로, 프로그래머가 프로그램의 각 부분을 서로 떼어 놓고 이해하는 데에도 도움이 됩니다. 요리사의 메모는 Lean 표현식을 평가하여 만들어지는 IO 액션을 나타내며, 카운터 직원의 답변은 효과로부터 다시 전달되는 값을 나타냅니다.

이러한 부수 효과 모델은 Lean 언어와 그 컴파일러, 런타임 시스템(RTS)을 모두 합친 전체가 동작하는 방식과 상당히 비슷합니다. C로 작성된 런타임 시스템의 프리미티브가 모든 기본 효과를 구현합니다. 프로그램을 실행하면 RTS는 main 액션을 호출하고, 이 액션은 실행할 새로운 IO 액션을 RTS에 반환합니다. RTS는 이 액션들을 실행하며, 계산을 수행할 때는 사용자의 Lean 코드에 위임합니다. Lean 내부의 관점에서 보면 프로그램에는 부수 효과가 없으며, IO 액션은 수행할 작업을 기술한 것일 뿐입니다. 프로그램 사용자라는 외부의 관점에서 보면, 프로그램의 핵심 로직에 대한 인터페이스를 이루는 부수 효과 계층이 존재합니다.

2.1.3. 실전 함수형 프로그래밍🔗

Lean의 부수 효과를 이해하는 또 다른 유용한 방법은 IO 액션을 세계 전체를 인자로 받아 값과 새로운 세계의 쌍을 반환하는 함수로 간주하는 것입니다. 이 경우 표준 입력에서 텍스트 한 줄을 읽는 것은 정말로 순수 함수입니다. 매번 다른 세계가 인자로 주어지기 때문입니다. 표준 출력에 텍스트 한 줄을 쓰는 것도 순수 함수입니다. 함수가 반환하는 세계가 처음 시작할 때의 세계와 다르기 때문입니다. 다만 프로그램은 세계를 절대 재사용하지 않도록, 그리고 새로운 세계를 반환하지 못하는 일이 없도록 주의해야 합니다—결국 이는 시간 여행이나 세계의 종말에 해당하기 때문입니다. 추상화 경계를 신중하게 설정하면 이러한 방식의 프로그래밍을 안전하게 만들 수 있습니다. 모든 기본 IO 액션이 하나의 세계를 받아 새로운 세계를 반환하고, 이 불변 조건을 보존하는 도구로만 이들을 조합할 수 있다면 이 문제는 발생할 수 없습니다.

이 모델은 구현할 수 없습니다. 결국 우주 전체를 Lean 값으로 바꾸어 메모리에 올릴 수는 없기 때문입니다. 하지만 세계를 나타내는 추상적인 토큰을 사용하면 이 모델의 변형을 구현할 수 있습니다. 프로그램이 시작될 때 프로그램에는 세계 토큰이 주어집니다. 그런 다음 이 토큰은 IO 기본 연산에 전달되고, 기본 연산이 반환한 토큰도 마찬가지로 다음 단계로 전달됩니다. 프로그램이 끝나면 토큰은 운영 체제에 반환됩니다.

이 부수 효과 모델은 RTS가 수행할 작업을 기술한 것으로서의 IO 액션이 Lean 내부에서 어떻게 표현되는지를 잘 설명합니다. 실제 세계를 변환하는 실제 함수는 추상화 장벽 뒤에 숨겨져 있습니다. 그러나 실제 프로그램은 대개 효과 하나만이 아니라 일련의 효과로 이루어집니다. 프로그램이 여러 효과를 사용할 수 있도록 Lean에는 do 표기법이라는 하위 언어가 있으며, 이를 통해 이러한 기본 IO 액션을 안전하게 조합하여 더 크고 유용한 프로그램을 만들 수 있습니다.

2.1.4. IO 액션 조합하기🔗

대부분의 유용한 프로그램은 출력을 생성할 뿐만 아니라 입력도 받습니다. 나아가 프로그램은 입력 데이터를 계산의 일부로 사용하여 입력에 따라 결정을 내리기도 합니다. HelloName.lean이라는 다음 프로그램은 사용자에게 이름을 물은 다음 인사를 건넵니다:

def main : IO Unit := 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}!"

이 프로그램에서 main 액션은 do 블록으로 이루어져 있습니다. 이 블록에는 일련의 문장이 들어 있으며, 각 문장은 (let으로 도입되는) 지역 변수일 수도 있고 실행될 액션일 수도 있습니다. SQL을 데이터베이스와 상호작용하기 위한 특수 목적 언어로 볼 수 있듯이, do 문법은 Lean 안에서 명령형 프로그램을 모델링하는 데 쓰이는 특수 목적 하위 언어로 볼 수 있습니다. do 블록으로 만든 IO 액션은 문장을 순서대로 실행하는 방식으로 실행됩니다.

이 프로그램은 이전 프로그램과 같은 방식으로 실행할 수 있습니다:

lean --run HelloName.lean

사용자가 David라고 응답하면, 프로그램과의 상호작용 세션은 다음과 같습니다:

How would you like to be addressed? David Hello, David!

타입 시그니처 줄은 Hello.lean의 것과 똑같습니다:

def main : IO Unit := do

유일한 차이점은 명령 시퀀스를 시작하는 키워드인 do로 끝난다는 것입니다. 키워드 do 뒤에 오는 들여쓰기된 각 줄은 모두 같은 명령 시퀀스에 속합니다.

처음 두 줄은 다음과 같습니다:

let stdin ← IO.getStdin let stdout ← IO.getStdout

stdin 핸들과 stdout 핸들을 각각 라이브러리 액션 IO.getStdin과 IO.getStdout을 실행하여 가져옵니다. do 블록 안에서 let은 일반 표현식에서와는 약간 다른 의미를 가집니다. 일반적으로 let의 지역 정의는 그 지역 정의 바로 뒤에 오는 단 하나의 표현식에서만 사용할 수 있습니다. do 블록 안에서는 let으로 도입된 지역 바인딩을 바로 다음 문장뿐만 아니라 do 블록의 나머지 모든 문장에서 사용할 수 있습니다. 또한 let은 보통 :=를 사용하여 정의되는 이름과 그 정의를 연결하지만, do 안의 일부 let 바인딩은 그 대신 왼쪽 화살표(← 또는 <-)를 사용합니다. 화살표를 사용한다는 것은 표현식의 값이 실행되어야 할 IO 액션이며, 그 액션의 결과가 지역 변수에 저장된다는 뜻입니다. 다시 말해, 화살표 오른쪽 표현식의 타입이 IO α이면, do 블록의 나머지 부분에서 그 변수의 타입은 α입니다. IO.getStdin과 IO.getStdout이 IO 액션인 이유는 프로그램 안에서 stdin과 stdout을 지역적으로 재정의할 수 있게 하기 위해서이며, 이는 편리할 수 있습니다. 만약 이들이 C에서처럼 전역 변수였다면 이를 재정의할 의미 있는 방법이 없었겠지만, IO 액션은 실행될 때마다 다른 값을 반환할 수 있습니다.

do 블록의 다음 부분은 사용자에게 이름을 묻는 역할을 합니다:

stdout.putStrLn "How would you like to be addressed?" let input ← stdin.getLine let name := input.dropEndWhile Char.isWhitespace

첫 번째 줄은 질문을 stdout에 쓰고, 두 번째 줄은 stdin에서 입력을 요청하며, 세 번째 줄은 입력받은 줄의 끝에 있는 줄바꿈 문자와 그 밖의 끝 공백 문자를 제거합니다. name의 정의에는 ←가 아니라 :=를 사용합니다. String.dropEndWhile은 IO 액션이 아니라 문자열에 대한 일반 함수이기 때문입니다.

마지막으로, 프로그램의 마지막 줄은 다음과 같습니다.

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

이 함수는 문자열 보간을 사용해 주어진 이름을 인사말 문자열에 넣고, 그 결과를 stdout에 출력합니다.