2.6.1. 평가와 실행🔗

부수 효과는 파일 읽기, 예외 던지기, 산업용 기계 작동시키기처럼 수학적 표현식의 평가를 넘어서는 프로그램 실행의 측면을 말합니다. 대부분의 언어는 평가 도중 부수 효과가 일어나는 것을 허용하지만, Lean은 그렇지 않습니다. 대신 Lean에는 부수 효과를 사용하는 프로그램의 기술을 나타내는 IO라는 타입이 있습니다. 그런 다음 이러한 기술은 언어의 런타임 시스템이 실행하며, 런타임 시스템은 특정 계산을 수행하기 위해 Lean 표현식 평가기를 호출합니다. IO α 타입의 값을 IO 액션이라고 부릅니다. 가장 단순한 것은 pure로, 인자를 그대로 반환하며 실제 부수 효과는 전혀 없습니다.

IO 액션은 세계 전체를 인자로 받아 부수 효과가 일어난 새로운 세계를 반환하는 함수로 이해할 수도 있습니다. 내부적으로 IO 라이브러리는 세계가 결코 복제되거나 생성되거나 파괴되지 않도록 보장합니다. 우주 전체는 너무 커서 메모리에 담을 수 없으므로 이러한 부수 효과 모델을 실제로 구현할 수는 없지만, 현실 세계를 프로그램 곳곳으로 전달되는 토큰으로 표현할 수는 있습니다.

프로그램이 시작되면 IO 액션 main이 실행됩니다. main은 다음 세 가지 타입 중 하나를 가질 수 있습니다:

• main : IO Unit은 명령줄 인자를 읽을 수 없고 항상 종료 코드 0을 반환하는 단순한 프로그램에 사용되며,

• main : IO UInt32는 인자 없이 성공 또는 실패를 알릴 수 있는 프로그램에 사용되며,

• main : List String → IO UInt32는 명령줄 인자를 받고 성공 또는 실패를 알리는 프로그램에 사용됩니다.

2.6.2. do 표기법🔗

Lean 표준 라이브러리는 파일 읽기와 쓰기, 표준 입력 및 표준 출력과의 상호 작용과 같은 효과를 나타내는 여러 기본 IO 액션을 제공합니다. 이러한 기본 IO 액션은 do 표기법을 사용하여 더 큰 IO 액션으로 조합되며, 이 표기법은 부수 효과가 있는 프로그램의 설명을 작성하기 위한 내장 도메인 특화 언어입니다. do 표현식은 일련의 문장을 포함하며, 각 문장은 다음 중 하나일 수 있습니다:

• IO 액션을 나타내는 표현식,

• let과 :=를 사용하여 정의된 이름이 주어진 표현식의 값을 가리키는 일반적인 지역 정의, 또는

• let과 ←를 사용하여 정의된 이름이 주어진 표현식의 값을 실행한 결과를 가리키는 지역 정의.

do로 작성된 IO 액션은 한 번에 한 문장씩 실행됩니다.

또한 do 바로 아래에 나오는 if와 match 표현식은 각 분기마다 자신만의 do를 가진 것으로 암묵적으로 간주됩니다. do 표현식 내부에서 중첩 액션은 괄호 바로 안에 왼쪽 화살표가 있는 표현식입니다. Lean 컴파일러는 이들을 가장 가까이 감싸는 do로 암묵적으로 끌어올리고 고유한 이름을 부여합니다. 이 블록은 match나 if 표현식의 한 분기에 암묵적으로 속한 것일 수도 있습니다. 그런 다음 이 고유한 이름이 중첩된 액션이 원래 있던 자리를 대체합니다.

2.6.3. 프로그램 컴파일 및 실행🔗

main 정의가 있는 단일 파일로 된 Lean 프로그램은 lean --run FILE로 실행할 수 있습니다. 간단한 프로그램이라면 이 방법으로 시작하는 것도 좋지만, 대부분의 프로그램은 결국 실행하기 전에 컴파일해야 하는 여러 파일로 된 프로젝트로 발전하게 됩니다.

Lean 프로젝트는 패키지로 구성됩니다. 패키지는 라이브러리와 실행 파일의 모음으로, 의존성 정보와 빌드 설정을 함께 담고 있습니다. 패키지는 Lean 빌드 도구인 Lake를 사용하여 기술합니다. 새 디렉터리에 Lake 패키지를 만들려면 lake new를 사용하고, 현재 디렉터리에 만들려면 lake init을 사용하십시오. Lake 패키지 설정은 또 하나의 도메인 특화 언어입니다. 프로젝트를 빌드하려면 lake build를 사용하십시오.

2.6.4. 부분성🔗

표현식 평가의 수학적 모델을 따르면 모든 표현식이 반드시 값을 가져야 합니다. 따라서 데이터 타입의 생성자를 모두 다루지 못하는 불완전한 패턴 매칭도, 무한 루프에 빠질 수 있는 프로그램도 허용되지 않습니다. Lean은 모든 match 표현식이 모든 경우를 다루는지, 그리고 모든 재귀 함수가 구조적 재귀이거나 명시적인 종료 증명을 갖추고 있는지 확인합니다.

하지만 일부 실제 프로그램은 POSIX 스트림처럼 무한할 수도 있는 데이터를 다루기 때문에 무한히 반복될 수 있어야 합니다. Lean은 탈출구를 제공합니다. 정의에 partial 표시가 붙은 함수는 종료하지 않아도 됩니다. 여기에는 대가가 따릅니다. Lean 언어에서 타입은 일급 요소이므로 함수가 타입을 반환할 수 있습니다. 그러나 부분 함수는 타입 검사 중에 평가되지 않습니다. 함수 안의 무한 루프 때문에 타입 검사기까지 무한 루프에 빠질 수 있기 때문입니다. 또한 수학적 증명은 부분 함수의 정의를 들여다볼 수 없으므로, 부분 함수를 사용하는 프로그램은 형식적으로 증명하기가 훨씬 어렵습니다.