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 옵션과 함께 호출되면, 프로그램의 main 정의를 호출합니다. 명령줄 인자를 받지 않는 프로그램에서는 main이 IO Unit 타입을 가져야 합니다. 이는 main이 함수가 아니라는 것을 의미합니다. 그 타입에는 화살표(→)가 없기 때문입니다. 부수 효과가 있는 함수인 대신, main은 수행할 효과에 대한 설명으로 구성됩니다.

앞 장에서 논의했듯이, Unit은 가장 단순한 귀납적 타입입니다. 이 타입은 인자를 전혀 받지 않는 unit이라는 단일 생성자를 가지고 있습니다. C 계통의 언어들에는 값을 전혀 반환하지 않는 void 함수라는 개념이 있습니다. Lean에서 모든 함수는 인자를 받아 값을 반환하며, 흥미로운 인자나 반환값이 없다는 사실은 대신 Unit 타입을 사용하여 나타낼 수 있습니다. Bool이 정보의 단일 비트를 나타낸다면, 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 표현식을 평가하여 만들어지는 IO 액션을 나타내며, 카운터 직원의 답변은 효과로부터 반환되는 값을 나타냅니다.

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

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

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

이 모델은 구현할 수 없습니다. 결국 우주 전체를 Lean 값으로 변환하여 메모리에 담을 수는 없습니다. 하지만 세계를 나타내는 추상 토큰을 사용하여 이 모델의 변형을 구현하는 것은 가능합니다. 프로그램이 시작되면, 세계 토큰(world token)이 제공됩니다. 이 토큰은 이후 IO 원시 함수(primitive)에 전달되며, 이들이 반환한 토큰 역시 같은 방식으로 다음 단계에 전달됩니다. 프로그램이 끝나면 토큰은 운영체제로 반환됩니다.

이러한 부작용 모델은 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에 씁니다.