5.4. Alternatives🔗

5.4.1. Recovery from Failure🔗

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 β

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.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. The `Alternative` Class🔗

많은 타입이 실패와 복구라는 개념을 지원한다. 여러 모나드에서 산술 표현식을 평가하는 절의 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. Exercises🔗

5.4.3.1. Improve Validation Friendliness🔗

<|>를 사용하는 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. Alternatives🔗

5.4.1. Recovery from Failure🔗

5.4.2. The Alternative Class🔗

5.4.3. Exercises🔗

5.4.3.1. Improve Validation Friendliness🔗

5.4.2. The `Alternative` Class🔗