4.7.1. Encoding Side Effects🔗

Lean은 순수 함수형 언어다. 이는 가변 변수, 로깅, 예외 같은 부수 효과를 포함하지 않는다는 뜻이다. 하지만 대부분의 부수 효과는 함수와 귀납 타입 또는 구조체를 조합해 인코딩할 수 있다. 예를 들어 가변 상태는 초기 상태를 받아 최종 상태와 결과의 쌍을 반환하는 함수로 인코딩할 수 있고, 예외는 성공적인 종료와 오류를 위한 생성자를 갖는 귀납 타입으로 인코딩할 수 있다.

인코딩된 효과의 각 집합은 하나의 타입이다. 따라서 프로그램이 이런 인코딩된 효과를 사용하면 그 사실이 타입에 드러난다. 함수형 프로그래밍은 프로그램이 효과를 사용할 수 없다는 뜻이 아니라, 어떤 효과를 사용하는지에 대해 정직해야 한다는 뜻이다. Lean의 타입 서명은 함수가 기대하는 인수의 타입과 반환하는 결과의 타입뿐 아니라 사용할 수 있는 효과도 설명한다.

4.7.2. The Monad Type Class🔗

어디서든 효과를 허용하는 언어에서도 순수 함수형 프로그램을 작성할 수 있다. 예를 들어 2 + 3은 아무 효과도 없는 유효한 Python 프로그램이다. 마찬가지로 효과가 있는 프로그램을 결합하려면 효과가 발생해야 하는 순서를 표현하는 방법이 필요하다. 결국 변수를 수정하기 전과 후 중 언제 예외가 던져지는지는 중요하다.

Monad 타입 클래스는 이 두 가지 중요한 성질을 포착한다. 두 메서드를 가진다. pure는 효과가 없는 프로그램을 나타내고, bind는 효과가 있는 프로그램을 순서대로 연결한다. Monad 인스턴스의 계약은 bind와 pure가 실제로 순수 계산과 순서 연결을 포착하도록 보장한다.

4.7.3. do-Notation for Monads🔗

IO에만 국한되지 않고 do 표기법은 어떤 모나드에서도 작동한다. 모나드를 사용하는 프로그램을 문장 중심 언어를 연상시키는 방식으로 작성하게 하며, 문장들이 차례로 연결된다. 또한 do 표기법은 중첩 동작 같은 여러 편리한 축약형을 제공한다. do로 작성한 프로그램은 내부적으로 >>=를 적용하는 형태로 변환된다.

4.7.4. Custom Monads🔗

언어마다 제공하는 부수 효과의 집합이 다르다. 대부분의 언어에는 가변 변수와 파일 입출력이 있지만, 모두가 예외 같은 기능을 제공하는 것은 아니다. 다른 언어는 Icon의 검색 기반 프로그램 실행, Scheme과 Ruby의 연속(continuation), Common Lisp의 재개 가능한 예외처럼 드물거나 고유한 효과를 제공한다. 효과를 모나드로 인코딩하면 프로그램이 언어가 제공하는 효과 집합에 제한되지 않는다는 장점이 있다. Lean은 어떤 모나드로도 편리하게 프로그래밍할 수 있도록 설계되었으므로, 프로그래머는 주어진 애플리케이션에 의미가 있는 부수 효과 집합을 정확히 자유롭게 선택할 수 있다.

4.7.5. The IO Monad🔗

현실 세계에 영향을 줄 수 있는 프로그램은 Lean에서 IO 동작으로 작성한다. IO는 많은 모나드 중 하나다. IO 모나드는 상태와 예외를 인코딩하며, 상태는 세계의 상태를 추적하는 데 사용하고 예외는 실패와 복구를 모델링한다.