5.4. 대안🔗

5.4.1. 실패로부터의 복구🔗

Validate는 입력이 허용될 수 있는 방식이 둘 이상인 상황에서도 사용할 수 있습니다. 입력 양식 RawInput의 경우, 레거시 시스템의 관례를 구현하는 또 다른 비즈니스 규칙 집합은 다음과 같을 수 있습니다:

모든 인간 사용자는 네 자리 숫자로 된 출생 연도를 제공해야 합니다.
1970년 이전에 태어난 사용자는 과거 기록이 불완전하므로 이름을 제공하지 않아도 됩니다.
1970년 이후에 태어난 사용자는 이름을 입력해야 합니다.
회사는 출생 연도 대신 "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 β

seqRight에는 seq를 사용해 정의한 기본 구현이 있습니다: 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.name

def 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를 구현하는 모든 애플리커티브 펑터에서 동작하는 다양한 연산을 정의할 수 있습니다. 그중 가장 중요한 연산 하나는 guard로, 결정 가능한 명제가 거짓이면 failure를 일으킵니다:

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

5.4. 대안🔗

5.4.1. 실패로부터의 복구🔗

5.4.2. Alternative 클래스🔗

5.4.3. 연습 문제🔗

5.4.3.1. 검증 친화성 개선하기🔗

5.4.2. `Alternative` 클래스🔗