2.6.1. 평가와 실행🔗

부수 효과(side effect)는 파일 읽기, 예외 발생, 산업용 기계 작동과 같이 수학적 표현식의 평가를 넘어서는 프로그램 실행의 측면들입니다. 대부분의 언어는 평가 도중 부수 효과가 발생하는 것을 허용하지만, 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 표현식은 다음과 같을 수 있는 일련의 statements(문장)를 포함합니다:

• 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 언어의 일급 요소이므로, 함수는 타입을 반환할 수 있습니다. 하지만 부분 함수는 타입 검사 중에 평가되지 않는데, 함수 내의 무한 루프가 타입 검사기를 무한 루프에 빠뜨릴 수 있기 때문입니다. 게다가 수학적 증명은 부분 함수의 정의를 조사할 수 없으므로, 이를 사용하는 프로그램은 형식적 증명에 훨씬 덜 적합하게 됩니다.