4.3.3.1. 효과 없음🔗

Empty 타입에는 생성자가 없으므로 값도 없습니다. 이는 Scala나 Kotlin의 Nothing 타입과 비슷합니다. Scala와 Kotlin에서 Nothing은 결과를 결코 반환하지 않는 계산을 나타낼 수 있습니다. 프로그램을 비정상 종료시키는 함수, 예외를 던지는 함수, 항상 무한 루프에 빠지는 함수 등이 여기에 해당합니다. 함수나 메서드가 Nothing 타입의 인자를 받는다면 그 코드는 죽은 코드입니다. 그 인자로 쓸 수 있는 값이 결코 존재하지 않기 때문입니다. Lean은 무한 루프와 예외를 지원하지 않지만, Empty는 어떤 함수가 호출될 수 없다는 것을 타입 시스템에 알리는 표시로서 여전히 유용합니다. E가 생성자가 없는 타입의 표현식일 때 nomatch E 문법을 사용하면, 현재 표현식은 결코 호출될 수 없었으므로 결과를 반환할 필요가 없다는 것을 Lean에 알려 줍니다.

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

이것을 항등 모나드인 Id와 함께 사용하면 효과가 전혀 없는 표현식을 평가할 수 있습니다.

-9

4.3.3.2. 비결정적 탐색🔗

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. 사용자 정의 환경🔗

문자열을 연산자로 쓸 수 있게 하고 각 문자열을 해당 연산자를 구현하는 함수에 대응시키는 매핑을 제공하면, 사용자가 평가기를 확장할 수 있게 됩니다. 예를 들어, 사용자는 나머지 연산자나 두 인자 중 최댓값을 반환하는 연산자를 추가하여 평가기를 확장할 수 있습니다. 함수 이름을 함수 구현에 대응시키는 매핑을 환경이라고 합니다.

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

함수를 모나드로 사용하는 것을 일반적으로 리더(reader) 모나드라고 합니다. 리더 모나드에서 표현식을 평가할 때는 다음 규칙이 사용됩니다.

• 상수 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의 매개변수 객체(parameter object)는 Reader에 정확히 대응하는 효과입니다. Kotlin의 컨텍스트 객체(context object) 관용구로도 비슷한 문제를 해결할 수 있지만, 컨텍스트 객체는 근본적으로 함수 인자를 자동으로 전달하는 수단입니다. 따라서 이 관용구는 언어에 내장된 효과라기보다는 리더 모나드로 인코딩한 방식에 더 가깝습니다.

4.3.3.4. 연습 문제🔗

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