Lean으로 하는 함수형 프로그래밍

5.4. 대안🔗

5.4.1. 실패로부터의 복구🔗

Validate는 입력을 허용할 수 있는 방법이 하나 이상 존재하는 상황에서도 사용할 수 있습니다. 입력 형식 RawInput에 대해, 레거시 시스템의 관례를 구현하는 대안적인 비즈니스 규칙 집합은 다음과 같을 수 있습니다:

  1. 모든 인간 사용자는 네 자리 숫자로 된 출생 연도를 제공해야 합니다.

  2. 1970년 이전에 태어난 사용자는 이전 기록이 불완전하기 때문에 이름을 제공할 필요가 없습니다.

  3. 1970년 이후 출생한 사용자는 이름을 제공해야 합니다.

  4. 회사는 출생 연도로 "FIRM"을 입력하고 회사명을 제공해야 합니다.

1970년에 태어난 사용자를 위한 특별한 규정은 마련되어 있지 않습니다. 그들은 포기하거나, 출생 연도를 거짓으로 말하거나, 전화를 걸 것으로 예상됩니다. 회사는 이를 사업 운영상 감수할 만한 비용으로 간주합니다.

다음 귀납적 타입은 이 명시된 규칙들로부터 생성될 수 있는 값들을 나타냅니다:

abbrev NonEmptyString := {s : String // s ≠ ""} inductive LegacyCheckedInput where | humanBefore1970 : (birthYear : {y : Nat // y > 999 ∧ y < 1970}) → String → LegacyCheckedInput | humanAfter1970 : (birthYear : {y : Nat // y > 1970}) → NonEmptyString → LegacyCheckedInput | company : NonEmptyString → LegacyCheckedInput deriving Repr

하지만 이 규칙들에 대한 검증기는 세 경우를 모두 다루어야 하므로 더 복잡합니다. 이는 중첩된 if 표현식의 연속으로 작성할 수도 있지만, 세 가지 경우를 독립적으로 설계한 다음 결합하는 것이 더 쉽습니다. 이를 위해서는 오류 메시지를 보존하면서 실패로부터 복구할 수 있는 수단이 필요합니다:

def Validate.orElse (a : Validate ε α) (b : Unit → Validate ε α) : Validate ε α := match a with | .ok x => .ok x | .errors errs1 => match b () with | .ok x => .ok x | .errors errs2 => .errors (errs1 ++ errs2)

이러한 실패 복구 패턴은 매우 흔하기 때문에 Lean에는 이를 위한 내장 문법이 있으며, 이는 OrElse라는 타입 클래스에 연결되어 있습니다:

class OrElse (α : Type) where orElse : α → (Unit → α) → α

E1 <|> E2 표현식은 OrElse.orElse E1 (fun () => E2)의 축약형입니다. Validate에 대한 OrElse의 인스턴스는 이 구문을 오류 복구에 사용할 수 있게 해 줍니다:

instance : OrElse (Validate ε α) where orElse := Validate.orElse

LegacyCheckedInput에 대한 검증기는 각 생성자에 대한 검증기로부터 만들어질 수 있습니다. 회사에 대한 규칙은 출생 연도가 문자열 "FIRM"이어야 하고 이름이 비어 있지 않아야 한다고 명시합니다. 하지만 생성자 LegacyCheckedInput.company는 출생 연도에 대한 표현이 전혀 없으므로, <*>를 사용해서 이를 수행할 간단한 방법이 없습니다. 핵심은 인자를 무시하는 <*> 함수를 사용하는 것입니다.

불리언 조건이 성립함을 확인하되 이 사실에 대한 증거를 타입에 기록하지 않는 것은 checkThat으로 수행할 수 있습니다:

def checkThat (condition : Bool) (field : Field) (msg : String) : Validate (Field × String) Unit := if condition then pure () else reportError field msg

checkCompany의 이 정의는 checkThat을 사용한 다음, 그 결과로 나온 Unit 값을 버립니다:

def checkCompany (input : RawInput) : Validate (Field × String) LegacyCheckedInput := pure (fun () name => .company name) <*> checkThat (input.birthYear == "FIRM") "birth year" "FIRM if a company" <*> checkName input.name

하지만 이 정의는 상당히 지저분합니다. 이는 두 가지 방법으로 간소화할 수 있습니다. 첫 번째 방법은 <*>의 첫 번째 사용을, 첫 번째 인자가 반환하는 값을 자동으로 무시하는 특수화된 버전인 *>로 대체하는 것입니다. 이 연산자 또한 SeqRight라는 타입 클래스에 의해 제어되며, E1 *> E2는 SeqRight.seqRight E1 (fun () => E2)의 구문 설탕입니다:

class SeqRight (f : Type → Type) where seqRight : f α → (Unit → f β) → f β

seq를 이용한 seqRight의 기본 구현이 존재합니다: seqRight (a : f α) (b : Unit → f β) : f β := pure (fun _ x => x) <*> a <*> b ().

seqRight를 사용하면, checkCompany는 더 간단해집니다:

def checkCompany (input : RawInput) : Validate (Field × String) LegacyCheckedInput := checkThat (input.birthYear == "FIRM") "birth year" "FIRM if a company" *> pure .company <*> checkName input.name

한 가지 더 단순화할 수 있습니다. 모든 Applicative에 대해, pure f <*> E는 f <$> E와 동치입니다. 다시 말해, pure를 사용하여 Applicative 타입에 넣은 함수를 적용하기 위해 seq를 사용하는 것은 과도한 조치이며, 이 함수는 그저 Functor.map을 사용하여 적용할 수도 있었을 것입니다. 이렇게 단순화하면 다음과 같은 결과를 얻습니다:

def checkCompany (input : RawInput) : Validate (Field × String) LegacyCheckedInput := checkThat (input.birthYear == "FIRM") "birth year" "FIRM if a company" *> .company <$> checkName input.name

LegacyCheckedInput의 나머지 두 생성자는 필드에 서브타입을 사용합니다. 서브타입을 검사하는 범용 도구를 사용하면 이를 더 쉽게 읽을 수 있습니다:

def checkSubtype {α : Type} (v : α) (p : α → Prop) [Decidable (p v)] (err : ε) : Validate ε {x : α // p x} := if h : p v then pure ⟨v, h⟩ else .errors { head := err, tail := [] }

함수의 인자 목록에서 타입 클래스 [Decidable (p v)]가 인자 v와 p의 명세 뒤에 와야 한다는 점이 중요합니다. 그렇지 않으면 이는 수동으로 제공된 값이 아니라 추가로 자동 생성된 암시적 인자 집합을 가리키게 됩니다. Decidable 인스턴스는 if를 사용하여 명제 p v를 검사할 수 있게 해 주는 것입니다.

인간 두 경우는 추가 도구가 필요하지 않습니다:

def checkHumanBefore1970 (input : RawInput) : Validate (Field × String) LegacyCheckedInput := (checkYearIsNat input.birthYear).andThen fun y => .humanBefore1970 <$> checkSubtype y (fun x => x > 999 ∧ x < 1970) ("birth year", "less than 1970") <*> pure input.namedef checkHumanAfter1970 (input : RawInput) : Validate (Field × String) LegacyCheckedInput := (checkYearIsNat input.birthYear).andThen fun y => .humanAfter1970 <$> checkSubtype y (· > 1970) ("birth year", "greater than 1970") <*> checkName input.name

세 경우에 대한 검증기들은 <|>를 사용하여 결합할 수 있습니다:

def checkLegacyInput (input : RawInput) : Validate (Field × String) LegacyCheckedInput := checkCompany input <|> checkHumanBefore1970 input <|> checkHumanAfter1970 input

성공한 경우들은 예상대로 LegacyCheckedInput의 생성자를 반환합니다:

Validate.ok (LegacyCheckedInput.company "Johnny's Troll Groomers")#eval checkLegacyInput ⟨"Johnny's Troll Groomers", "FIRM"⟩
Validate.ok (LegacyCheckedInput.company "Johnny's Troll Groomers")
Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "Johnny")#eval checkLegacyInput ⟨"Johnny", "1963"⟩
Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "Johnny")
Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "")#eval checkLegacyInput ⟨"", "1963"⟩
Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "")

최악의 입력은 가능한 모든 실패를 반환합니다.

Validate.errors { head := ("birth year", "FIRM if a company"), tail := [("name", "Required"), ("birth year", "less than 1970"), ("birth year", "greater than 1970"), ("name", "Required")] }#eval checkLegacyInput ⟨"", "1970"⟩
Validate.errors
  { head := ("birth year", "FIRM if a company"),
    tail := [("name", "Required"),
             ("birth year", "less than 1970"),
             ("birth year", "greater than 1970"),
             ("name", "Required")] }

5.4.2. Alternative 클래스🔗

많은 타입들이 실패와 복구라는 개념을 지원합니다. 다양한 모나드로 산술 표현식 평가하기 절에 나온 Many 모나드가 그러한 타입 중 하나이며, Option 역시 마찬가지입니다. 둘 다 이유를 제공하지 않고 실패하는 것을 지원합니다(반면 Except와 Validate는 무엇이 잘못되었는지에 대한 표시를 요구합니다).

Alternative 클래스는 실패와 복구를 위한 추가 연산자를 가진 애플리커티브 펑터를 설명합니다:

class Alternative (f : Type → Type) extends Applicative f where failure : f α orElse : f α → (Unit → f α) → f α

Add α의 구현자가 HAdd α α α 인스턴스를 무료로 얻는 것과 마찬가지로, Alternative의 구현자는 OrElse 인스턴스를 무료로 얻습니다:

instance [Alternative f] : OrElse (f α) where orElse := Alternative.orElse

Option에 대한 Alternative의 구현은 첫 번째 none이 아닌 인자를 유지합니다:

instance : Alternative Option where failure := none orElse | some x, _ => some x | none, y => y ()

마찬가지로, Many에 대한 구현은 Many.union의 일반적인 구조를 따르며, 지연 평가를 유도하는 Unit 매개변수가 다르게 배치되어 있다는 점에서 사소한 차이가 있습니다:

def Many.orElse : Many α → (Unit → Many α) → Many α | .none, ys => ys () | .more x xs, ys => .more x (fun () => orElse (xs ()) ys) instance : Alternative Many where failure := .none orElse := Many.orElse

다른 타입 클래스와 마찬가지로, Alternative는 Alternative를 구현하는 어떤 애플리커티브 펑터에도 동작하는 다양한 연산의 정의를 가능하게 합니다. 가장 중요한 것 중 하나는 결정 가능한 명제가 거짓일 때 failure를 발생시키는 guard입니다:

def guard [Alternative f] (p : Prop) [Decidable p] : f Unit := if p then pure () else failure

모나드 프로그램에서 실행을 조기에 종료하는 것은 매우 유용합니다. Many에서 이는 다음과 같이 자연수의 모든 짝수 약수를 계산하는 프로그램에서처럼 탐색의 한 가지 전체를 걸러내는 데 사용될 수 있습니다:

def Many.countdown : Nat → Many Nat | 0 => .none | n + 1 => .more n (fun () => countdown n) def evenDivisors (n : Nat) : Many Nat := do let k ← Many.countdown (n + 1) guard (k % 2 = 0) guard (n % k = 0) pure k

20에 대해 실행하면 예상한 결과를 얻을 수 있습니다:

[20, 10, 4, 2]#eval (evenDivisors 20).takeAll
[20, 10, 4, 2]

5.4.3. 연습 문제🔗

5.4.3.1. 유효성 검증 친화성 개선🔗

<|>를 사용하는 Validate 프로그램에서 반환되는 오류는 읽기 어려울 수 있는데, 오류 목록에 포함된다는 것은 그저 어떤 코드 경로를 통해 해당 오류에 도달할 수 있다는 의미일 뿐이기 때문입니다. 더 구조화된 오류 보고서를 사용하면 사용자가 그 과정을 더 정확하게 따라가도록 안내할 수 있습니다:

  • Validate.errors의 NonEmptyList를 순수한 타입 변수로 교체한 다음, Applicative (Validate ε)와 OrElse (Validate ε α) 인스턴스의 정의를 Append ε 인스턴스만 있으면 되도록 갱신하십시오.

  • 검증 실행 중 발생한 모든 오류를 변환하는 함수 Validate.mapErrors : Validate ε α → (ε → ε') → Validate ε' α를 정의하십시오.

  • 오류를 나타내기 위해 데이터 타입 TreeError를 사용하여, 레거시 검증 시스템이 세 가지 대안을 거치는 경로를 추적하도록 다시 작성하십시오.

  • TreeError에 누적된 경고와 오류를 사용자 친화적으로 보여 주는 함수 report : TreeError → String을 작성하십시오.

inductive TreeError where | field : Field → String → TreeError | path : String → TreeError → TreeError | both : TreeError → TreeError → TreeError instance : Append TreeError where append := .both