2.6. Summary
2.6.1. Evaluation vs Execution
부수 효과는 파일 읽기, 예외 발생, 산업용 기계 작동처럼 수학적 표현식의 평가를 넘어서는 프로그램 실행의 측면이다.
대부분의 언어는 평가 중 부수 효과를 허용하지만 Lean은 그렇지 않다.
대신 Lean에는 부수 효과를 사용하는 프로그램의 설명을 나타내는 IO라는 타입이 있다.
이 설명은 언어의 런타임 시스템이 실행하며, 런타임 시스템은 특정 계산을 수행하도록 Lean 표현식 평가기를 호출한다.
IO α 타입의 값을 IO 동작이라고 한다.
가장 단순한 동작은 인수를 반환하고 실제 부수 효과가 없는 pure다.
IO 동작은 전체 세계를 인수로 받아 부수 효과가 일어난 새 세계를 반환하는 함수로 이해할 수도 있다.
이면에서 IO 라이브러리는 세계가 복제·생성·소멸되지 않도록 보장한다.
세계 전체는 메모리에 담기에는 너무 크므로 이 부수 효과 모델을 실제로 구현할 수는 없다. 대신 실제 세계를 프로그램에서 전달하는 토큰으로 나타낼 수 있다.
프로그램이 시작되면 IO 동작인 main을 실행한다.
main은 다음 세 타입 중 하나일 수 있다.
2.6.2. do Notation
Lean 표준 라이브러리는 파일 읽기·쓰기와 표준 입력·출력 상호작용 같은 효과를 나타내는 기본 IO 동작을 제공한다.
이 기본 IO 동작은 부수 효과가 있는 프로그램의 설명을 작성하기 위한 내장 도메인 특화 언어인 do 표기로 더 큰 IO 동작을 구성한다.
do 표현식은 다음과 같은 문장의 시퀀스를 포함한다.
-
IO동작을 나타내는 표현식, -
let과:=를 사용하는 일반 지역 정의(정의한 이름은 주어진 표현식의 값을 가리킨다), 또는 -
let과←를 사용하는 지역 정의(정의한 이름은 주어진 표현식의 값을 실행한 결과를 가리킨다).
do로 작성한 IO 동작은 한 번에 한 문장씩 실행한다.
또한 do 바로 아래에 있는 if와 match 표현식은 각 분기가 자체 do를 가진 것으로 암묵적으로 취급한다.
do 표현식 안에서 중첩 동작은 괄호 바로 아래에 왼쪽 화살표가 있는 표현식이다.
Lean 컴파일러는 이를 가장 가까운 바깥 do로 암묵적으로 올린다. 이 블록은 match나 if 표현식 분기의 일부일 수도 있다. 그리고 중첩 동작에 고유한 이름을 부여한다.
이 고유한 이름이 중첩 동작의 원래 위치를 대신한다.
2.6.3. Compiling and Running Programs
main 정의가 있는 단일 파일 Lean 프로그램은 lean --run FILE로 실행할 수 있다.
간단한 프로그램을 시작하기에는 좋지만 대부분의 프로그램은 결국 실행 전에 컴파일해야 하는 여러 파일 프로젝트로 발전한다.
Lean 프로젝트는 의존성 정보와 빌드 구성을 포함한 라이브러리·실행 파일 모음인 패키지로 조직한다.
패키지는 Lean 빌드 도구인 Lake로 설명한다.
새 디렉터리에 Lake 패키지를 만들려면 lake new를, 현재 디렉터리에 만들려면 lake init을 사용하라.
Lake 패키지 구성은 또 다른 도메인 특화 언어다.
프로젝트를 빌드하려면 lake build를 사용하라.
2.6.4. Partiality
표현식 평가의 수학적 모델을 따르면 모든 표현식에 값이 있어야 한다.
따라서 데이터 타입의 모든 생성자를 다루지 못하는 불완전한 패턴 매칭과 무한 루프에 빠질 수 있는 프로그램은 허용되지 않는다.
Lean은 모든 match 표현식이 모든 경우를 다루고 모든 재귀 함수가 구조적으로 재귀적이거나 명시적인 종료 증명을 가지도록 보장한다.
그러나 POSIX 스트림처럼 잠재적으로 무한한 데이터를 처리하는 실제 프로그램에는 무한 루프 가능성이 필요하다.
Lean은 탈출구를 제공한다. 정의에 partial을 표시한 함수는 종료할 필요가 없다.
그 대신 대가가 따른다.
타입이 Lean 언어의 일급 부분이므로 함수는 타입을 반환할 수 있다.
그러나 함수의 무한 루프가 타입 검사기를 무한 루프에 빠뜨릴 수 있으므로 부분 함수는 타입 검사 중 평가하지 않는다.
또한 수학적 증명은 부분 함수의 정의를 살펴볼 수 없으므로 부분 함수를 사용하는 프로그램은 형식 증명에 훨씬 덜 적합하다.