4.3.3.1. 효과 없음🔗

타입 Empty는 생성자가 없으며, 따라서 값도 없습니다. 이는 Scala나 Kotlin의 Nothing 타입과 같습니다. Scala와 Kotlin에서 Nothing은 프로그램을 크래시시키거나, 예외를 던지거나, 항상 무한 루프에 빠지는 함수처럼 결코 결과를 반환하지 않는 계산을 나타낼 수 있습니다. 타입이 Nothing인 함수나 메서드의 인자는 죽은 코드를 나타내는데, 이는 적합한 인자 값이 결코 존재할 수 없기 때문입니다. Lean은 무한 루프와 예외를 지원하지 않지만, Empty는 함수가 호출될 수 없음을 타입 시스템에 나타내는 지표로서 여전히 유용합니다. nomatch E 구문을 E가 생성자가 없는 타입의 표현식일 때 사용하면, 현재 표현식이 결코 호출될 수 없으므로 결과를 반환할 필요가 없다는 것을 Lean에게 알려줍니다.

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

이는 항등 모나드인 Id와 함께 사용하여 아무런 효과가 없는 표현식을 평가하는 데 쓸 수 있습니다:

-9

4.3.3.2. 비결정적 탐색🔗

0으로 나누기를 만났을 때 단순히 실패하는 대신, 역추적하여 다른 입력을 시도하는 것도 합리적일 수 있습니다. 적절한 모나드가 주어지면, 바로 그 동일한 evaluateM은 실패로 귀결되지 않는 답의 집합을 찾는 비결정적 탐색을 수행할 수 있습니다. 이를 위해서는 나눗셈 외에도 결과를 선택할 수 있는 수단이 필요합니다. 이를 수행하는 한 가지 방법은 표현식 언어에 함수 choose를 추가하여, 평가기가 실패하지 않는 결과를 탐색하는 동안 두 인자 중 하나를 선택하도록 지시하는 것입니다.

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

• 상수 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 연산자를 필요로 합니다. 비결정적 탐색(nondeterministic search)에서 두 연산을 순차 실행한다는 것은 첫 번째 단계에서 나온 모든 가능성을 취하여 각각에 대해 나머지 프로그램을 실행한 뒤, 그 결과들의 합집합을 취하는 것으로 이루어집니다. 다시 말해, 첫 번째 단계가 세 가지 가능한 답을 반환한다면, 두 번째 단계는 그 세 가지 모두에 대해 시도되어야 합니다. 두 번째 단계는 각 입력에 대해 임의의 개수의 답을 반환할 수 있으므로, 그 합집합을 취하면 전체 탐색 공간을 나타내게 됩니다.

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일 때 빈 리스트는 성공적인 탐색이며, 그렇지 않으면 실패합니다. 리스트가 비어 있지 않은 경우 두 가지 가능성이 있습니다: 리스트의 머리가 목표보다 크다면 성공적인 탐색에 참여할 수 없고, 그렇지 않다면 참여할 수 있습니다. 리스트의 머리(head)가 후보가 아니라면, 탐색은 리스트의 꼬리(tail)로 진행됩니다. head가 후보라면, Many.union으로 결합할 두 가지 가능성이 있습니다: 찾은 해가 head를 포함하거나, 포함하지 않는 경우입니다. head를 포함하지 않는 해는 tail에 대한 재귀 호출로 찾을 수 있으며, head를 포함하는 해는 목표에서 head를 뺀 다음, 재귀 호출의 결과로 나온 해에 head를 붙임으로써 얻을 수 있습니다.

헬퍼 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의 언폴딩(unfolding)을 되돌리고 명시적인 세부 사항을 정리함으로써 얻을 수 있습니다:

단순히 "타입을 따라가는" 방식만으로 항상 올바른 함수를 작성할 수 있는 것은 아니며, 이는 결과로 나온 프로그램을 이해하지 못하게 될 위험을 안고 있습니다. 하지만 이미 작성된 프로그램을 이해하는 것이 아직 작성되지 않은 프로그램을 이해하는 것보다 더 쉬울 수 있으며, 밑줄을 채워 나가는 과정에서 통찰을 얻을 수도 있습니다. 이 경우, 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 }