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

Lean은 순수 함수형 언어입니다. 이는 가변 변수, 로깅, 예외와 같은 부작용을 포함하지 않는다는 것을 의미합니다. 하지만 대부분의 부수 효과는 함수와 귀납적 타입 또는 구조체의 조합을 사용하여 인코딩될 수 있습니다. 예를 들어, 가변 상태(mutable state)는 초기 상태를 최종 상태와 결과의 쌍으로 매핑하는 함수로 인코딩할 수 있으며, 예외는 성공적인 종료와 오류에 대한 생성자를 가진 귀납적 타입으로 인코딩할 수 있습니다.

인코딩된 이펙트의 각 집합은 하나의 타입입니다. 그 결과, 프로그램이 이러한 인코딩된 효과를 사용하면 이는 해당 타입에 드러납니다. 함수형 프로그래밍은 프로그램이 효과를 사용할 수 없다는 것을 의미하지 않으며, 단지 어떤 효과를 사용하는지에 대해 정직할 것을 요구할 뿐입니다. Lean의 타입 시그니처는 함수가 기대하는 인자들의 타입과 반환하는 결과의 타입뿐만 아니라, 그 함수가 사용할 수 있는 효과가 무엇인지도 나타냅니다.

4.7.2. 모나드 타입 클래스🔗

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

타입 클래스 Monad는 이 두 가지 중요한 속성을 담아냅니다. 여기에는 두 가지 메서드가 있습니다: pure는 효과가 없는 프로그램을 나타내며, bind는 효과가 있는 프로그램을 순차적으로 실행합니다. Monad 인스턴스에 대한 계약은 bind와 pure가 실제로 순수 계산과 순차 실행을 포착하도록 보장합니다.

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

IO에 국한되지 않고, do-표기법은 모든 모나드에 대해 작동합니다. 이는 모나드를 사용하는 프로그램을 문장이 차례로 이어지는 문장 지향 언어와 유사한 스타일로 작성할 수 있게 해줍니다. 또한, do-표기법은 중첩된 액션과 같은 여러 추가적인 편리한 축약형을 사용할 수 있게 해줍니다. do로 작성된 프로그램은 내부적으로 >>=의 적용으로 변환됩니다.

4.7.4. 커스텀 모나드🔗

언어마다 서로 다른 부작용 집합을 제공합니다. 대부분의 언어는 가변 변수와 파일 입출력 기능을 갖추고 있지만, 예외와 같은 기능은 모든 언어에 있는 것은 아닙니다. 다른 언어들은 Icon의 탐색 기반 프로그램 실행, Scheme과 Ruby의 컨티뉴에이션, Common Lisp의 재개 가능한 예외처럼 드물거나 독특한 효과를 제공합니다. 모나드로 효과를 인코딩하는 것의 장점은 프로그램이 언어에서 제공하는 효과의 집합에 제한되지 않는다는 것입니다. Lean은 어떤 모나드로든 프로그래밍하기 편리하도록 설계되었기 때문에, 프로그래머는 주어진 애플리케이션에 적합한 부수 효과의 집합을 정확히 자유롭게 선택할 수 있습니다.

4.7.5. IO 모나드🔗

실세계에 영향을 미칠 수 있는 프로그램은 Lean에서 IO 액션으로 작성됩니다. IO는 여러 모나드 중 하나입니다. IO 모나드는 상태와 예외를 인코딩하며, 상태는 세계의 상태를 추적하는 데 사용되고 예외는 실패와 복구를 모델링합니다.