4.7.1. 부수 효과 인코딩하기🔗

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

인코딩된 효과의 각 집합은 하나의 타입입니다. 따라서 프로그램이 이렇게 인코딩된 효과를 사용하면, 그 사실이 프로그램의 타입에 드러납니다. 함수형 프로그래밍은 프로그램이 효과를 사용할 수 없다는 뜻이 아닙니다. 단지 어떤 효과를 사용하는지에 대해 정직하기를 요구할 뿐입니다. Lean의 타입 시그니처는 함수가 기대하는 인자의 타입과 반환하는 결과의 타입뿐만 아니라, 함수가 사용할 수 있는 효과가 무엇인지도 나타냅니다.

4.7.2. 모나드 타입 클래스🔗

효과를 어디에서나 허용하는 언어에서도 순수 함수형 프로그램을 작성할 수 있습니다. 예를 들어, 2 + 3은 효과가 전혀 없는 올바른 Python 프로그램입니다. 마찬가지로, 효과가 있는 프로그램들을 조합하려면 효과가 일어나야 하는 순서를 명시할 방법이 필요합니다. 어쨌든 예외가 변수를 수정하기 전에 발생하는지, 수정한 후에 발생하는지는 중요한 문제입니다.

타입 클래스 Monad는 이 두 가지 중요한 속성을 담아냅니다. 이 타입 클래스에는 두 개의 메서드가 있습니다. pure는 효과가 없는 프로그램을 나타내고, bind는 효과가 있는 프로그램들을 순서대로 연결합니다. Monad 인스턴스에 대한 규약은 bind와 pure가 실제로 순수한 계산과 순차 실행을 담아내도록 보장합니다.

4.7.3. 모나드를 위한 do-표기법🔗

do 표기법은 IO에만 국한되지 않고 모든 모나드에서 동작합니다. 이 표기법을 사용하면 모나드를 사용하는 프로그램을 문장이 차례로 이어지는, 문장 지향 언어를 연상시키는 스타일로 작성할 수 있습니다. 또한 do 표기법은 중첩된 액션과 같은 여러 가지 편리한 축약 표기를 추가로 제공합니다. do로 작성된 프로그램은 내부적으로 >>=의 적용으로 변환됩니다.

4.7.4. 사용자 정의 모나드🔗

언어마다 제공하는 부수 효과의 종류가 다릅니다. 대부분의 언어에는 가변 변수와 파일 I/O가 있지만, 모든 언어에 예외 같은 기능이 있는 것은 아닙니다. 또 어떤 언어는 Icon의 탐색 기반 프로그램 실행, Scheme과 Ruby의 컨티뉴에이션, Common Lisp의 재개 가능한 예외처럼 드물거나 고유한 효과를 제공합니다. 모나드로 효과를 인코딩하면 프로그램이 언어가 제공하는 효과에만 국한되지 않는다는 장점이 있습니다. Lean은 어떤 모나드로든 편리하게 프로그래밍할 수 있도록 설계되었으므로, 프로그래머는 각 애플리케이션에 알맞은 부수 효과의 집합을 정확히 골라 자유롭게 선택할 수 있습니다.

4.7.5. IO 모나드🔗

실세계에 영향을 줄 수 있는 프로그램은 Lean에서 IO 액션으로 작성합니다. IO는 여러 모나드 중 하나일 뿐입니다. IO 모나드는 상태와 예외를 표현합니다. 상태는 세계의 상태를 추적하는 데 쓰이고, 예외는 실패와 복구를 모델링합니다.