Functional Programming in Lean

6.6. Summary🔗

6.6.1. Combining Monads🔗

모나드를 처음부터 작성할 때 각 효과를 모나드에 추가하는 방식을 설명하는 설계 패턴을 사용한다. 리더 효과는 모나드 타입을 리더 환경에서 출발하는 함수로 만들어 추가하고, 상태 효과는 초기 상태에서 최종 상태와 짝지은 값으로 가는 함수를 포함해 추가한다. 실패나 예외는 반환 타입에 합 타입을 포함해 추가하고 로깅이나 다른 출력은 반환 타입에 곱 타입을 포함해 추가한다. 기존 모나드를 반환 타입의 일부로 만들어 그 효과를 새 모나드에 포함할 수도 있다.

이 설계 패턴을 재사용 가능한 소프트웨어 구성 요소 라이브러리로 만든 것이 모나드 변환기다. 모나드 변환기는 어떤 기반 모나드에 효과를 추가한다. 모나드 변환기는 더 단순한 모나드 타입을 인수로 받아 강화된 모나드 타입을 반환한다. 최소한 모나드 변환기는 다음 인스턴스를 제공해야 한다.

  1. 내부 타입이 이미 모나드라고 가정하는 Monad 인스턴스

  2. 내부 모나드의 동작을 변환된 모나드로 옮기는 MonadLift 인스턴스

모나드 변환기는 다형적 구조체나 귀납적 데이터 타입으로 구현할 수도 있지만, 대개 기반 모나드 타입에서 강화된 모나드 타입으로 가는 함수로 구현한다.

6.6.2. Type Classes for Effects🔗

일반적인 설계 패턴은 특정 효과를 가진 모나드, 그 효과를 다른 모나드에 추가하는 모나드 변환기, 효과에 대한 일반 인터페이스를 제공하는 타입 클래스를 정의해 특정 효과를 구현하는 것이다. 덕분에 프로그램은 필요한 효과만 지정하고 호출자는 올바른 효과를 가진 어떤 모나드든 제공할 수 있다.

때로 보조 타입 정보(예: 상태를 제공하는 모나드의 상태 타입이나 예외를 제공하는 모나드의 예외 타입)는 출력 매개변수이고 때로는 그렇지 않다. 출력 매개변수는 각 효과를 한 번만 사용하는 단순한 프로그램에 유용하지만 같은 효과의 인스턴스를 여러 개 사용하면 타입 검사기가 너무 일찍 잘못된 타입으로 결정할 위험이 있다. 따라서 보통 두 버전을 모두 제공하며 일반 매개변수 버전 타입 클래스의 이름은 -Of로 끝난다.

6.6.3. Monad Transformers Don't Commute🔗

모나드에서 변환기의 순서를 바꾸면 그 모나드를 사용하는 프로그램의 의미가 바뀔 수 있다는 점이 중요하다. 예를 들어 StateTExceptT의 순서를 바꾸면 예외가 발생할 때 상태 변경을 잃는 프로그램이나 변경을 유지하는 프로그램이 될 수 있다. 대부분의 명령형 언어는 후자만 제공하지만 모나드 변환기의 유연성 때문에 작업에 맞는 종류를 고르려면 생각과 주의가 필요하다.

6.6.4. do-Notation for Monad Transformers🔗

Lean의 do 블록은 어떤 값으로 블록을 끝내는 조기 반환, 지역 가변 변수, breakcontinue가 있는 for 루프, 한 갈래 if 문을 지원한다. 이는 증명에 Lean을 사용하는 데 방해가 될 명령형 기능을 도입하는 것처럼 보일 수 있지만, 실제로는 모나드 변환기의 흔한 사용을 위한 더 편리한 문법일 뿐이다. 이면에서 do 블록이 작성된 모나드는 추가 효과를 지원하도록 ExceptTStateT를 적절히 사용해 변환한다.