4.3.3.1. No Effects🔗

Empty 타입에는 생성자가 없으므로 값도 없다. Scala나 Kotlin의 Nothing 타입과 같다. Scala와 Kotlin에서 Nothing은 프로그램을 중단하거나 예외를 던지거나 항상 무한 루프에 빠지는 함수처럼 결과를 반환하지 않는 계산을 나타낼 수 있다. Nothing 타입의 함수나 메서드에 전달하는 인수는 적합한 인수 값이 절대 존재하지 않으므로 도달 불가능한 코드임을 나타낸다. Lean은 무한 루프와 예외를 지원하지 않지만 Empty는 함수를 호출할 수 없음을 타입 시스템에 알리는 데 여전히 유용하다. E가 타입에 생성자가 없는 식일 때 nomatch E 문법을 사용하면, 해당 식은 호출될 수 없으므로 현재 식이 결과를 반환할 필요가 없다고 Lean에 알린다.

Empty를 Prim의 매개변수로 사용하면 Prim.plus, Prim.minus, Prim.times 외에 추가 경우가 없음을 나타낸다. Prim.other 생성자에 넣을 Empty 타입의 값을 만들 수 없기 때문이다. Empty 타입의 연산자를 두 정수에 적용하는 함수는 호출될 수 없으므로 결과를 반환할 필요가 없다. 따라서 어떤 모나드에서도 사용할 수 있다.

이를 항등 모나드인 Id와 함께 사용하면 아무 효과도 없는 표현식을 평가할 수 있다.

-9

4.3.3.2. Nondeterministic Search🔗

0으로 나눌 때 단순히 실패하는 대신 되돌아가 다른 입력을 시도하는 것도 합리적이다. 적절한 모나드가 주어지면 동일한 evaluateM으로 실패하지 않는 답의 집합을 비결정적으로 검색할 수 있다. 이를 위해서는 나눗셈에 더해 결과를 선택하는 방법을 지정할 수 있어야 한다. 한 가지 방법은 표현식 언어에 choose 함수를 추가해, 평가기가 실패하지 않는 결과를 검색하는 동안 두 인수 중 하나를 선택하도록 지시하는 것이다.

이제 평가기의 결과는 단일 값이 아니라 값의 멀티셋이다. 멀티셋으로 평가하는 규칙은 다음과 같다.

• 상수 n은 싱글턴 집합 \{n\}으로 평가된다.

• 나눗셈 이외의 산술 연산자는 연산자들의 데카르트 곱에서 각 쌍에 적용되므로, X + Y는 \{ x + y \mid x ∈ X, y ∈ Y \}로 평가된다.

• 나눗셈 X / Y는 \{ x / y \mid x ∈ X, y ∈ Y, y ≠ 0\}로 평가된다. 즉 Y의 모든 0 값은 버린다.

• 선택 \mathrm{choose}(x, y)는 \{ x, y \}로 평가된다.

예를 들어 1 + \mathrm{choose}(2, 5)는 \{ 3, 6 \}으로, 1 + 2 / 0은 \{\}으로, 90 / (\mathrm{choose}(-5, 5) + 5)는 \{ 9 \}로 평가된다. 진정한 집합 대신 멀티셋을 사용하면 원소의 고유성을 검사할 필요가 없어 코드가 단순해진다.

Monad Many 인스턴스에는 bind 연산자가 필요하다. 비결정적 검색에서 두 연산을 순서대로 연결하는 일은 첫 단계의 모든 가능성을 얻고 각각에 대해 프로그램의 나머지를 실행한 뒤 결과의 합집합을 취하는 것이다. 즉 첫 단계가 가능한 답 세 개를 반환하면 두 번째 단계는 세 답 모두에 대해 시도해야 한다. 두 번째 단계는 각 입력에 대해 임의 개수의 답을 반환할 수 있으므로, 이들을 합집합으로 묶으면 전체 검색 공간이 된다.

Many.one과 Many.bind는 모나드 계약을 따른다. Many.bind (Many.one v) f가 f v와 같은지 확인하려면 식을 가능한 만큼 먼저 평가한다.

빈 멀티셋은 union의 오른쪽 항등원이므로 결과는 f v와 같다. Many.bind v Many.one이 v와 같은지 확인하려면 Many.bind가 v의 각 원소에 Many.one을 적용한 결과의 합집합을 취한다는 점을 생각하라. 즉 v가 {v₁, v₂, v₃, …, vₙ} 형태라면 Many.bind v Many.one은 {v₁} ∪ {v₂} ∪ {v₃} ∪ … ∪ {vₙ}이고, 이는 {v₁, v₂, v₃, …, vₙ}이다.

마지막으로 Many.bind가 결합적인지 확인하려면 Many.bind (Many.bind v f) g가 Many.bind v (fun x => Many.bind (f x) g)와 같은지 확인한다. v가 {v₁, v₂, v₃, …, vₙ} 형태라면 다음과 같다.

이는 다음을 뜻한다.

마찬가지로

따라서 양변이 같으므로 Many.bind는 결합적이다.

따라서 모나드 인스턴스는 다음과 같다.

이 모나드를 사용하는 예제 검색은 목록에서 합이 15가 되는 모든 수 조합을 찾는다.

검색 과정은 목록에 대해 재귀적이다. 목표가 0이면 빈 목록은 성공적인 검색이고, 그렇지 않으면 실패한다. 목록이 비어 있지 않을 때는 두 가지 가능성이 있다. 목록의 머리가 목표보다 커서 성공적인 검색에 참여할 수 없거나, 그렇지 않아 참여할 수 있다. 머리가 후보가 아니면 목록의 꼬리로 검색을 진행한다. 머리가 후보라면 Many.union으로 결합할 두 가능성이 있다. 찾은 해가 머리를 포함하거나 포함하지 않는다. 머리를 포함하지 않는 해는 꼬리에 재귀 호출을 해 찾고, 머리를 포함하는 해는 목표에서 머리를 뺀 뒤 재귀 호출의 결과에 머리를 붙여 얻는다.

printList 보조 함수는 결과가 한 줄에 하나씩 표시되도록 한다.

[7, 8]
[6, 9]
[5, 10]
[4, 5, 6]
[3, 5, 7]
[3, 4, 8]
[2, 6, 7]
[2, 5, 8]
[2, 4, 9]
[2, 3, 10]
[2, 3, 4, 6]
[1, 6, 8]
[1, 5, 9]
[1, 4, 10]
[1, 3, 5, 6]
[1, 3, 4, 7]
[1, 2, 5, 7]
[1, 2, 4, 8]
[1, 2, 3, 9]
[1, 2, 3, 4, 5]

[3, 6]

[]

[9]

4.3.3.3. Custom Environments🔗

문자열을 연산자로 사용할 수 있게 하고 문자열에서 이를 구현하는 함수로 가는 매핑을 제공하면 평가기를 사용자가 확장할 수 있다. 예를 들어 사용자는 나머지 연산자나 두 인수 중 최댓값을 반환하는 연산자로 평가기를 확장할 수 있다. 함수 이름에서 함수 구현으로 가는 매핑을 환경이라고 한다.

환경은 재귀 호출마다 전달해야 한다. 처음에는 evaluateM에 환경을 담을 추가 인수가 필요하고 이 인수를 각 재귀 호출에 전달해야 할 것처럼 보인다. 하지만 이런 인수를 전달하는 것은 모나드의 또 다른 형태이므로, 적절한 Monad 인스턴스를 사용하면 평가기를 변경하지 않고 사용할 수 있다.

함수를 모나드로 사용하는 것을 보통 리더 모나드라고 한다. 리더 모나드에서 표현식을 평가할 때는 다음 규칙을 사용한다.

• 상수 n은 상수 함수 λ e . n으로 평가된다.

• 산술 연산자는 인수를 전달하는 함수로 평가되므로 f + g는 λ e . f(e) + g(e)로 평가된다.

• 사용자 정의 연산자는 인수에 사용자 정의 연산자를 적용한 결과로 평가되므로 f \ \mathrm{OP}\ g는 다음으로 평가된다. λ e . \begin{cases} h(f(e), g(e)) & \mathrm{if}\ e\ \mathrm{contains}\ (\mathrm{OP}, h) \\ 0 & \mathrm{otherwise} \end{cases} 여기서 0은 알 수 없는 연산자를 적용했을 때의 대체값이다.

반면 bind는 조금 더 까다롭다. 그 타입은 Reader ρ α → (α → Reader ρ β) → Reader ρ β다. Reader의 정의를 펼치면 (ρ → α) → (α → ρ → β) → (ρ → β)가 되므로 이 타입을 더 쉽게 이해할 수 있다. 첫 번째 인수로 환경을 받는 함수를 받고, 두 번째 인수는 환경을 받는 함수의 결과를 또 다른 환경 수신 함수로 변환해야 한다. 이 둘을 결합한 결과 자체가 환경을 기다리는 함수다.

Lean을 대화식으로 사용해 이 함수 작성을 도움받을 수 있다. 첫 단계는 가능한 한 많은 도움을 얻도록 인수와 반환 타입을 매우 명시적으로 적고, 정의 본문에는 밑줄을 넣는 것이다.

Lean은 현재 범위에서 사용할 수 있는 변수와 결과에 기대하는 타입을 설명하는 메시지를 제공한다. 지하철 입구와 닮아서 턴스타일이라고 부르는 ⊢ 기호는 지역 변수와 원하는 타입을 구분한다. 이 메시지에서 원하는 타입은 ρ → β다.

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → β⊢ ρ → β

반환 타입이 함수이므로 밑줄을 fun으로 감싸는 것이 좋은 첫 단계다.

이제 결과 메시지에서 함수의 인수가 지역 변수로 표시된다.

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ β

현재 문맥에서 β를 만들 수 있는 것은 next뿐이며, 그러려면 인수 두 개가 필요하다. 각 인수 자체를 밑줄로 둘 수 있다.

두 밑줄에는 각각 다음 메시지가 표시된다.

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ α

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ ρ

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ ρ

Reader를 펼치기 전으로 되돌리고 명시적인 세부 사항을 정리하면 최종 버전을 얻을 수 있다.

단순히 “타입을 따라가기”만으로 항상 올바른 함수를 작성할 수 있는 것은 아니며, 결과 프로그램을 이해하지 못할 위험도 있다. 하지만 작성되지 않은 프로그램보다 작성된 프로그램을 이해하기 쉬울 수도 있고, 밑줄을 채우는 과정에서 통찰을 얻을 수 있다. 이 경우 Reader.bind는 Id의 bind와 똑같이 작동한다. 단, 추가 인수를 받아 자신의 인수에 전달한다. 이 직관은 작동 방식을 이해하는 데 도움이 된다.

상수 함수를 만드는 Reader.pure와 Reader.bind는 모나드 계약을 따른다. Reader.bind (Reader.pure v) f가 f v와 같은지 확인하려면 마지막 단계까지 정의를 치환하면 충분하다.

모든 함수 f에 대해 fun x => f x는 f와 같으므로 계약의 첫 부분을 만족한다. Reader.bind r Reader.pure가 r와 같은지 확인할 때도 비슷한 기법이 작동한다.

리더 동작 r 자체가 함수이므로 이는 r와 같다. 결합성을 확인하려면 Reader.bind (Reader.bind r f) g와 Reader.bind r (fun x => Reader.bind (f x) g) 모두에 같은 방법을 적용할 수 있다.

Reader.bind r (fun x => Reader.bind (f x) g)도 같은 식으로 줄어든다.

따라서 Monad (Reader ρ) 인스턴스가 정당화된다.

표현식 평가기에 전달할 사용자 정의 환경은 쌍의 목록으로 나타낼 수 있다.

예를 들어 exampleEnv에는 최댓값 함수와 나머지 함수가 들어 있다.

Lean에는 쌍의 목록에서 키에 연결된 값을 찾는 List.lookup 함수가 이미 있으므로, applyPrimReader는 사용자 정의 함수가 환경에 있는지만 확인하면 된다. 함수를 알 수 없으면 0을 반환한다.

evaluateM을 applyPrimReader 및 표현식과 함께 사용하면 환경을 받는 함수가 나온다. 다행히 exampleEnv를 사용할 수 있다.

9

Many와 마찬가지로 Reader는 대부분의 언어에서 인코딩하기 어려운 효과의 예지만, 타입 클래스와 모나드를 사용하면 다른 효과만큼 편리하게 만들 수 있다. Common Lisp, Clojure, Emacs Lisp의 동적 변수나 특수 변수는 Reader처럼 사용할 수 있다. 마찬가지로 Scheme과 Racket의 매개변수 객체는 Reader에 정확히 대응하는 효과다. Kotlin의 컨텍스트 객체 관용구도 비슷한 문제를 해결할 수 있지만, 근본적으로 함수 인수를 자동으로 전달하는 수단이다. 따라서 이 관용구는 언어의 효과라기보다 리더 모나드로 인코딩하는 방식에 가깝다.

4.3.3.4. Exercises🔗

{ log := [(Prim.plus, 1, 2), (Prim.minus, 3, 4), (Prim.times, 3, -1)], val := -3 }