2.1. Running a Program
Lean 프로그램을 실행하는 가장 간단한 방법은 Lean 실행 파일에 --run 옵션을 주는 것이다.
Hello.lean이라는 파일을 만들고 다음 내용을 입력하라.
def main : IO Unit := IO.println "Hello, world!"
그런 다음 명령줄에서 다음을 실행하라.
$ lean --run Hello.lean
프로그램은 Hello, world!을 출력하고 종료한다.
2.1.1. Anatomy of a Greeting
Lean을 --run 옵션과 함께 호출하면 프로그램의 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. Functional Programming vs Effects
Lean의 계산 모델은 시간이 지나도 변하지 않는 값을 변수에 정확히 하나씩 부여하는 수학적 표현식의 평가에 기반한다. 표현식 평가의 결과는 변하지 않으며 같은 표현식을 다시 평가하면 항상 같은 결과를 얻는다.
반면 유용한 프로그램은 세계와 상호작용해야 한다. 입력도 출력도 수행하지 않는 프로그램은 사용자에게 데이터를 요청하거나 디스크에 파일을 만들거나 네트워크 연결을 열 수 없다. Lean은 자기 자신으로 작성되었고 Lean 컴파일러는 파일을 읽고 만들며 텍스트 편집기와 상호작용한다. 같은 표현식이 항상 같은 결과를 내는 언어가 시간이 지나며 내용이 바뀔 수 있는 디스크 파일을 읽는 프로그램을 어떻게 지원할 수 있을까?
이 겉보기 모순은 부수 효과를 조금 다르게 생각하면 해결할 수 있다. 커피와 샌드위치를 파는 카페를 상상해 보자. 이 카페에는 주문을 처리하는 요리사와 고객을 응대하고 주문서를 전달하는 카운터 직원이라는 두 직원이 있다. 요리사는 외부 세계와 접촉하기를 몹시 싫어하는 무뚝뚝한 사람이지만 카페의 음식과 음료를 한결같이 잘 만든다. 그러려면 요리사에게 평온과 고요가 필요하며 대화로 방해받아서는 안 된다. 카운터 직원은 친절하지만 주방 일에는 완전히 서툴다. 고객은 카운터 직원과 상호작용하고, 직원은 실제 요리를 모두 요리사에게 맡긴다. 알레르기 확인처럼 요리사가 고객에게 물어볼 것이 있으면 카운터 직원에게 쪽지를 보내고, 직원은 고객에게 물어본 뒤 결과를 쪽지로 요리사에게 전달한다.
이 비유에서 요리사는 Lean 언어다.
주문을 받으면 요리사는 요청받은 것을 충실하고 일관되게 내놓는다.
카운터 직원은 세계와 상호작용하며 결제를 받고 음식을 내고 고객과 대화할 수 있는 주변 런타임 시스템이다.
두 직원은 함께 식당의 모든 기능을 수행하지만 각자 가장 잘하는 일을 맡도록 책임을 나눈다.
고객을 멀리해야 요리사가 훌륭한 커피와 샌드위치에 집중할 수 있듯, Lean에 부수 효과가 없으면 프로그램을 형식적 수학 증명의 일부로 사용할 수 있다.
또한 구성 요소 사이에 미묘한 결합을 만드는 숨은 상태 변경이 없으므로 프로그래머가 프로그램의 각 부분을 서로 독립적으로 이해하는 데 도움이 된다.
요리사의 쪽지는 Lean 표현식을 평가해 만들어지는 IO 동작을 나타내고, 카운터 직원의 답장은 효과에서 전달되어 돌아오는 값이다.
이 부수 효과 모델은 Lean 언어와 컴파일러, 런타임 시스템(RTS)의 전체 묶음이 작동하는 방식과 매우 비슷하다.
C로 작성한 런타임 시스템의 기본 요소가 모든 기본 효과를 구현한다.
프로그램을 실행할 때 RTS는 main 동작을 호출하고, 이 동작은 실행할 새 IO 동작을 RTS에 반환한다.
RTS는 이 동작을 실행하며 계산은 사용자의 Lean 코드에 맡긴다.
Lean의 내부 관점에서 프로그램에는 부수 효과가 없고 IO 동작은 수행할 작업의 설명일 뿐이다.
프로그램 사용자라는 외부 관점에서는 프로그램의 핵심 논리에 대한 인터페이스를 만드는 부수 효과 계층이 있다.
2.1.3. Real-World Functional Programming
Lean의 부수 효과를 생각하는 또 다른 유용한 방법은 IO 동작을 전체 세계를 인수로 받아 값과 새 세계를 함께 반환하는 함수로 보는 것이다.
이 경우 표준 입력에서 한 줄을 읽는 것은 매번 다른 세계를 인수로 받으므로 순수 함수다.
표준 출력에 한 줄을 쓰는 것도 함수가 반환하는 세계가 시작할 때의 세계와 다르므로 순수 함수다.
프로그램은 세계를 절대 재사용하지 않고 새 세계 반환을 빠뜨리지 않도록 주의해야 한다. 그렇지 않으면 시간 여행이나 세계의 종말에 해당하기 때문이다.
신중한 추상화 경계를 두면 이 프로그래밍 방식을 안전하게 만들 수 있다.
모든 기본 IO 동작이 한 세계를 받고 새 세계를 반환하며 이 불변식을 보존하는 도구로만 결합된다면 문제는 발생하지 않는다.
이 모델은 구현할 수 없다. 우주 전체를 Lean 값으로 바꾸어 메모리에 둘 수 없기 때문이다. 그러나 세계를 나타내는 추상 토큰을 사용한 변형 모델은 구현할 수 있다. 프로그램이 시작하면 세계 토큰을 제공한다. 이 토큰을 IO 기본 요소에 전달하고, 기본 요소가 반환한 토큰을 다음 단계에 다시 전달한다. 프로그램이 끝나면 토큰을 운영 체제에 반환한다.
이 부수 효과 모델은 RTS가 수행할 작업의 설명인 IO 동작을 Lean 내부에 표현하는 방식을 잘 설명한다.
실제 세계를 변환하는 함수는 추상화 장벽 뒤에 있다.
하지만 실제 프로그램은 보통 하나가 아닌 효과의 시퀀스로 이루어진다.
여러 효과를 사용하도록 Lean의 하위 언어인 do 표기가 기본 IO 동작을 안전하게 결합해 더 크고 유용한 프로그램을 만들게 한다.
2.1.4. Combining IO Actions
대부분의 유용한 프로그램은 출력을 만들 뿐 아니라 입력도 받는다.
또한 입력을 계산의 일부로 사용해 입력에 따라 결정을 내리기도 한다.
다음 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
라이브러리 동작 IO.getStdin과 IO.getStdout을 각각 실행해 stdin, stdout 핸들을 가져온다.
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에 쓴다.