5.2. 애플리커티브 펑터🔗

애플리커티브 펑터는 두 가지 추가 연산인 pure와 seq를 사용할 수 있는 펑터입니다. pure는 Monad에서 사용되는 것과 동일한 연산자인데, 이는 Monad가 실제로 Applicative를 상속하기 때문입니다. seq는 map과 매우 유사하게, 함수를 사용하여 데이터 타입의 내용을 변환할 수 있게 해줍니다. 하지만 seq의 경우, 함수 자체가 데이터 타입 안에 포함되어 있습니다: f (α → β) → (Unit → f α) → f β. 함수를 타입 f 아래에 둠으로써 Applicative 인스턴스가 함수가 적용되는 방식을 제어할 수 있게 되는 반면, Functor.map은 무조건적으로 함수를 적용합니다. 두 번째 인수는 Unit →으로 시작하는 타입을 가지는데, 이는 함수가 결코 적용되지 않는 경우에 seq의 정의가 단락 평가(short-circuit)될 수 있도록 하기 위함입니다.

이 단락 감소(short-circuiting) 동작의 가치는 Applicative Option의 인스턴스에서 확인할 수 있습니다:

instance : Applicative Option where
  pure x := .some x
  seq f x :=
    match f with
    | none => none
    | some g => g <$> x ()

이 경우, seq가 적용할 함수가 없다면 그 인자를 계산할 필요가 없으므로, x는 결코 호출되지 않습니다. 동일한 고려 사항이 Except에 대한 Applicative 인스턴스에도 반영되어 있습니다:

instance : Applicative (Except ε) where
  pure x := .ok x
  seq f x :=
    match f with
    | .error e => .error e
    | .ok g => g <$> x ()

이러한 단락 평가(short-circuiting) 동작은 함수 자체가 아니라 함수를 둘러싼 Option 또는 Except 구조에만 의존합니다.

모나드는 순차적으로 문장을 실행한다는 개념을 순수 함수형 언어에 담아내는 방법으로 볼 수 있습니다. 한 문장의 결과가 이후 어떤 문장들이 실행될지에 영향을 미칠 수 있습니다. 이는 bind의 타입 m α → (α → m β) → m β에서 확인할 수 있습니다. 첫 번째 문장의 결과 값은 다음에 실행할 문장을 계산하는 함수의 입력이 됩니다. bind를 연속으로 사용하는 것은 명령형 프로그래밍 언어에서 문장들을 나열하는 것과 비슷하며, bind는 조건문이나 반복문 같은 제어 구조를 구현할 수 있을 만큼 강력합니다.

이 비유를 따르면, Applicative는 부수 효과가 있는 언어에서의 함수 적용을 포착합니다. Kotlin이나 C# 같은 언어에서 함수의 인자는 왼쪽에서 오른쪽 순서로 평가됩니다. 앞선 인자에서 수행된 부수 효과는 나중 인자에서 수행된 부수 효과보다 먼저 발생합니다. 그러나 함수는 인자의 특정 값에 의존하는 사용자 정의 단락 평가(short-circuiting) 연산자를 구현할 만큼 강력하지는 않습니다.

일반적으로 seq는 직접 호출되지 않습니다. 대신 연산자 <*>가 사용됩니다. 이 연산자는 두 번째 인수를 fun () => ...로 감싸서 호출 지점을 단순화합니다. 다시 말해, E1 <*> E2는 Seq.seq E1 (fun () => E2)의 문법적 설탕(syntactic sugar)입니다.

seq를 여러 인자와 함께 사용할 수 있게 해주는 핵심적인 특징은, 여러 인자를 받는 Lean 함수가 사실은 나머지 인자를 기다리는 또 다른 함수를 반환하는 단일 인자 함수라는 점입니다. 다시 말해, seq의 첫 번째 인자가 여러 인자를 기다리고 있는 상태라면, seq의 결과는 나머지 인자들을 기다리는 상태가 됩니다. 예를 들어, some Plus.plus는 Option (Nat → Nat → Nat) 타입을 가질 수 있습니다. 인자를 하나 제공하면 some Plus.plus <*> some 4는 Option (Nat → Nat) 타입이 됩니다. 이것 자체도 seq와 함께 사용할 수 있으므로, some Plus.plus <*> some 4 <*> some 7은 Option Nat 타입을 가집니다.

모든 펑터가 애플리커티브인 것은 아닙니다. Pair는 내장 곱 타입 Prod와 비슷합니다:

structure Pair (α β : Type) : Type where
  first : α
  second : β

Except와 마찬가지로, Pair는 Type → Type → Type 타입을 가집니다. 이는 Pair α가 Type → Type 타입을 가진다는 것을 의미하며, 다음과 같이 Functor 인스턴스를 만드는 것이 가능합니다:

instance : Functor (Pair α) where
  map f x := ⟨x.first, f x.second⟩

이 인스턴스는 Functor 계약을 준수합니다.

확인해야 할 두 가지 속성은 id <$> Pair.mk x y = Pair.mk x y라는 것과 f <$> g <$> Pair.mk x y = (f ∘ g) <$> Pair.mk x y라는 것입니다. 첫 번째 속성은 좌변의 평가를 단계별로 따라가면서, 그것이 우변으로 평가된다는 것을 확인하는 것만으로 검사할 수 있습니다:

              id <$> Pair.mk x yPair.mk x (id y)Pair.mk x y

두 번째 등식은 양변을 단계별로 계산해 보면서 동일한 결과를 산출하는지 확인함으로써 검증할 수 있습니다:

              f <$> g <$> Pair.mk x yf <$> Pair.mk x (g y)Pair.mk x (f (g y))

              (f ∘ g) <$> Pair.mk x yPair.mk x ((f ∘ g) y)Pair.mk x (f (g y))

하지만 Applicative 인스턴스를 정의하려는 시도는 그다지 잘 작동하지 않습니다. pure의 정의가 필요합니다:

def Pair.pure (x : β) : Pair α β := don't know how to synthesize placeholder
context:
β α:Typex:β⊢ Pair α β_

don't know how to synthesize placeholder
context:
β α:Typex:β⊢ Pair α β

스코프 안에 타입이 β인 값(즉 x)이 있으며, 밑줄에서 나온 오류 메시지는 다음 단계로 생성자 Pair.mk를 사용하라고 제안합니다:

def Pair.pure (x : β) : Pair α β := Pair.mk don't know how to synthesize placeholder for argument `first`
context:
β α:Typex:β⊢ α_ x

don't know how to synthesize placeholder for argument `first`
context:
β α:Typex:β⊢ α

안타깝게도 사용 가능한 α가 없습니다. pure가 Applicative (Pair α)의 인스턴스를 정의하려면 가능한 모든 타입 α에 대해 작동해야 하므로, 이는 불가능합니다. 결국, 호출자는 α를 값이 전혀 없는 Empty로 선택할 수 있습니다.

5.2.1. 모나드가 아닌 애플리커티브🔗

폼에 대한 사용자 입력을 검증할 때는, 한 번에 하나의 오류만 제공하기보다는 여러 오류를 한꺼번에 제공하는 것이 일반적으로 가장 좋다고 여겨집니다. 이를 통해 사용자는 필드별로 오류를 수정하며 성가심을 느끼는 대신, 컴퓨터를 만족시키기 위해 무엇이 필요한지 전체적으로 파악할 수 있습니다.

이상적으로는, 사용자 입력을 검증한다는 사실이 검증을 수행하는 함수의 타입에서 드러나야 합니다. 이 함수는 구체적인 데이터 타입을 반환해야 합니다—예를 들어 텍스트 상자에 숫자가 들어 있는지 확인하는 경우 실제 숫자 타입을 반환해야 합니다. 검증 루틴은 입력이 검증을 통과하지 못할 때 예외를 던질 수 있습니다. 그러나 예외에는 중대한 단점이 있습니다: 첫 번째 오류에서 프로그램을 종료시키므로, 오류 목록을 누적하는 것이 불가능합니다.

반면, 오류 목록을 누적한 다음 이 목록이 비어 있지 않으면 실패하는 일반적인 설계 패턴 역시 문제가 있습니다. 입력 데이터의 각 하위 절을 검증하는 길게 중첩된 if 문 시퀀스는 유지 관리하기 어려우며, 오류 메시지 한두 개를 놓치기 쉽습니다. 이상적으로는, 새로운 값을 반환할 수 있으면서도 오류 메시지를 자동으로 추적하고 누적하는 API를 사용하여 검증을 수행할 수 있습니다.

Validate라는 애플리커티브 펑터는 이러한 스타일의 API를 구현하는 한 가지 방법을 제공합니다. Except 모나드와 마찬가지로, Validate는 검증된 데이터를 정확하게 특징짓는 새로운 값을 구성할 수 있게 해 줍니다. Except와 달리, 목록이 비어 있는지 확인하는 것을 잊어버릴 위험 없이 여러 오류를 누적할 수 있습니다.

5.2.1.1. 사용자 입력🔗

사용자 입력의 예시로, 다음 구조를 살펴보겠습니다.

structure RawInput where
  name : String
  birthYear : String

구현해야 할 비즈니스 로직은 다음과 같습니다:

이름은 비어 있을 수 없습니다
태어난 해는 숫자여야 하며 음수가 아니어야 합니다
출생 연도는 1900년보다 크고, 양식이 검증되는 연도보다 작거나 같아야 합니다

이들을 데이터 타입으로 표현하려면 서브타입이라 불리는 새로운 기능이 필요합니다. 이 도구를 손에 넣으면 애플리커티브 펑터를 사용하여 오류를 추적하는 검증 프레임워크를 작성할 수 있으며, 이러한 규칙들을 이 프레임워크에서 구현할 수 있습니다.

5.2.1.2. 서브타입🔗

이러한 조건을 표현하는 가장 쉬운 방법은 Subtype라는 추가적인 Lean 타입, 즉 서브타입을 사용하는 것입니다:

structure Subtype {α : Type} (p : α → Prop) where
  val : α
  property : p val

이 서브타입 구조체는 두 개의 타입 매개변수를 가집니다: α라는 데이터 타입인 암시적 매개변수와, α에 대한 술어인 명시적 매개변수 p입니다. 술어는 값으로 치환하면 실제 서술이 되는 변수를 포함한 논리적 서술로서, 조회에서 인덱스가 범위 내에 있다는 것이 무엇을 의미하는지 설명하는 GetElem의 매개변수와 같습니다. Subtype(서브타입)의 경우, 술어는 α의 값들 중 술어가 성립하는 부분 집합을 잘라냅니다. 이 서브타입 구조체의 두 필드는 각각 α에서 얻은 값과, 그 값이 술어 p를 만족한다는 증거입니다. Lean은 Subtype(서브타입)에 대한 특수 문법을 가지고 있습니다. p가 α → Prop 타입을 가진다면, Subtype p라는 서브타입은 {x : α // p x}로 쓸 수도 있으며, 타입 α를 자동으로 추론할 수 있는 경우에는 {x // p x}로도 쓸 수 있습니다.

귀납적 타입으로 양수를 표현하는 것은 명확하며 프로그래밍하기 쉽습니다. 하지만 여기에는 중요한 단점이 있습니다. Nat와 Int는 Lean 프로그램의 관점에서는 일반적인 귀납적 타입의 구조를 가지고 있지만, 컴파일러는 이들을 특별하게 취급하며 빠른 임의 정밀도 숫자 라이브러리를 사용하여 이들을 구현합니다. 추가로 사용자가 정의한 타입에는 이것이 해당되지 않습니다. 하지만 Nat을 0이 아닌 수로 제한하는 서브타입은 새 타입이 효율적인 표현을 그대로 사용하면서도 컴파일 시점에 0을 배제할 수 있게 해 줍니다:

def FastPos : Type := {x : Nat // x > 0}

가장 작은 빠른 양수는 여전히 1입니다. 이제 귀납적 타입의 생성자가 아니라, 꺾쇠괄호로 구성되는 구조체의 인스턴스입니다. 첫 번째 인자는 기저의 Nat이고, 두 번째 인자는 해당 Nat이 0보다 크다는 증거입니다:

def one : FastPos := ⟨1, by⊢ 1 > 0 decideAll goals completed! 🐙⟩

명제 1 > 0는 결정 가능하므로, decide 택틱이 필요한 증거를 생성합니다. OfNat 인스턴스는 Pos의 인스턴스와 매우 유사하지만, n + 1 > 0이라는 증거를 제공하기 위해 짧은 택틱 증명을 사용한다는 점이 다릅니다:

instance : OfNat FastPos (n + 1) where
  ofNat := ⟨n + 1, byn:Nat⊢ n + 1 > 0 simpAll goals completed! 🐙⟩

여기서 simp가 필요한 이유는 decide가 구체적인 값을 요구하지만, 문제가 되는 명제는 n + 1 > 0이기 때문입니다.

서브타입은 양날의 검입니다. 이러한 방식은 검증 규칙을 효율적으로 표현할 수 있게 해 주지만, 이 규칙을 유지해야 하는 부담을 라이브러리 사용자에게 전가하며, 사용자는 중요한 불변 조건을 위반하지 않는다는 것을 증명해야 합니다. 일반적으로 이들을 라이브러리 내부에서 사용하여, 모든 불변식이 자동으로 충족되도록 보장하는 API를 사용자에게 제공하고, 필요한 증명은 모두 라이브러리 내부에 두는 것이 좋습니다.

α 타입의 값이 서브타입 {x : α // p x}에 속하는지 확인하려면 보통 명제 p x가 결정 가능해야 합니다. 동등성과 순서 클래스에 대한 절에서는 결정 가능한 명제를 if와 함께 사용하는 방법을 설명합니다. if가 결정 가능한 명제와 함께 사용될 때는, 이름을 제공할 수 있습니다. then 분기에서는 그 이름이 명제가 참이라는 증거에 묶이고, else 분기에서는 명제가 거짓이라는 증거에 묶입니다. 이는 주어진 Nat이 양수인지 확인할 때 유용합니다:

def Nat.asFastPos? (n : Nat) : Option FastPos :=
  if h : n > 0 then
    some ⟨n, h⟩
  else none

then 분기에서 h는 n > 0이라는 증거에 바인딩되며, 이 증거는 Subtype(서브타입)의 생성자에 대한 두 번째 인자로 사용될 수 있습니다.

5.2.1.3. 검증된 입력🔗

유효성이 검증된 사용자 입력은 여러 기법을 사용하여 비즈니스 로직을 표현하는 구조체입니다:

구조체 타입 자체가 유효성을 검사한 연도를 인코딩하므로, CheckedInput 2019는 CheckedInput 2020과 같은 타입이 아닙니다
출생 연도는 String이 아니라 Nat으로 표현됩니다
서브타입은 이름과 출생 연도 필드에 허용되는 값을 제한하는 데 사용됩니다

structure CheckedInput (thisYear : Nat) : Type where
  name : {n : String // n ≠ ""}
  birthYear : {y : Nat // y > 1900 ∧ y ≤ thisYear}

입력 검증기는 현재 연도와 RawInput을 인자로 받아, 검사된 입력 또는 하나 이상의 검증 실패를 반환해야 합니다. 이는 Validate 타입으로 표현됩니다:

inductive Validate (ε α : Type) : Type where
  | ok : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

이것은 Except와(과) 매우 유사해 보입니다. 유일한 차이점은 errors 생성자가 두 개 이상의 실패를 포함할 수 있다는 것입니다.

Validate는 펑터입니다. 함수를 매핑하면 존재할 수 있는 성공 값을 변환하며, 이는 Except에 대한 Functor 인스턴스에서와 마찬가지입니다.

instance : Functor (Validate ε) where
  map f
   | .ok x => .ok (f x)
   | .errors errs => .errors errs

Validate에 대한 Applicative 인스턴스는 Except에 대한 인스턴스와 중요한 차이점이 있습니다: Except에 대한 인스턴스는 처음 만난 오류에서 종료되는 반면, Validate에 대한 인스턴스는 함수 분기와 인자 분기 둘 다에서 발생하는 모든 오류를 누적하도록 신경 써서 작성되었습니다:

instance : Applicative (Validate ε) where
  pure := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors errs =>
      match x () with
      | .ok _ => .errors errs
      | .errors errs' => .errors (errs ++ errs')

.errors를 NonEmptyList의 생성자와 함께 사용하는 것은 다소 장황합니다. reportError와 같은 헬퍼는 코드를 더 읽기 쉽게 만들어 줍니다. 이 애플리케이션에서 오류 보고서는 필드 이름과 메시지가 짝지어진 형태로 구성됩니다:

def Field := String

def reportError (f : Field) (msg : String) : Validate (Field × String) α :=
  .errors { head := (f, msg), tail := [] }

Validate에 대한 Applicative 인스턴스를 사용하면 각 필드에 대한 검사 절차를 독립적으로 작성한 다음 조합할 수 있습니다. 이름을 확인하는 것은 문자열이 비어 있지 않은지 확인한 다음, 이 사실에 대한 증거를 서브타입(Subtype) 형태로 반환하는 것으로 이루어집니다. 이는 if의 증거 결속(evidence-binding) 버전을 사용합니다:

def checkName (name : String) :
    Validate (Field × String) {n : String // n ≠ ""} :=
  if h : name = "" then
    reportError "name" "Required"
  else pure ⟨name, h⟩

then 분기에서 h는 name = ""라는 증거에 묶이고, else 분기에서는 ¬name = ""라는 증거에 묶입니다.

일부 유효성 검사 오류가 다른 검사를 불가능하게 만드는 경우가 분명히 있습니다. 예를 들어, 혼란에 빠진 사용자가 숫자 대신 "syzygy"라는 단어를 입력했다면 출생 연도 필드가 1900보다 큰지 확인하는 것은 아무런 의미가 없습니다. 숫자의 허용 범위를 확인하는 것은 해당 필드가 실제로 숫자를 포함하고 있음을 먼저 확인한 후에야 의미가 있습니다. 이는 함수 andThen을 사용하여 표현할 수 있습니다:

def Validate.andThen (val : Validate ε α)
    (next : α → Validate ε β) : Validate ε β :=
  match val with
  | .errors errs => .errors errs
  | .ok x => next x

이 함수의 타입 시그니처는 Monad 인스턴스에서 bind로 사용하기에 적합하지만, 그렇게 하지 않아야 할 타당한 이유가 있습니다. 이는 Applicative 계약을 설명하는 절에 기술되어 있습니다.

출생 연도가 숫자인지 확인하려면 String.Slice.toNat? : String.Slice → Option Nat라는 내장 함수가 유용합니다. String.trimAscii를 사용하여 선행 및 후행 공백을 먼저 제거하는 것이 사용자에게 가장 친화적입니다:

def checkYearIsNat (year : String) : Validate (Field × String) Nat :=
  match year.trimAscii.toNat? with
  | none => reportError "birth year" "Must be digits"
  | some n => pure n

제공된 연도가 예상 범위 내에 있는지 확인하려면, 증거를 제공하는 형태의 if를 중첩하여 사용하는 것이 적절합니다:

def checkBirthYear (thisYear year : Nat) :
    Validate (Field × String) {y : Nat // y > 1900 ∧ y ≤ thisYear} :=
  if h : year > 1900 then
    if h' : year ≤ thisYear then
      pure ⟨year, bythisYear:Natyear:Nath:year > 1900h':year ≤ thisYear⊢ year > 1900 ∧ year ≤ thisYear simp [*]All goals completed! 🐙⟩
    else reportError "birth year" s!"Must be no later than {thisYear}"
  else reportError "birth year" "Must be after 1900"

마지막으로, 이 세 가지 구성 요소는 <*>를 사용하여 결합할 수 있습니다:

def checkInput (year : Nat) (input : RawInput) :
    Validate (Field × String) (CheckedInput year) :=
  pure CheckedInput.mk <*>
    checkName input.name <*>
    (checkYearIsNat input.birthYear).andThen fun birthYearAsNat =>
      checkBirthYear year birthYearAsNat

checkInput을 테스트해 보면 실제로 여러 개의 피드백을 반환할 수 있음을 알 수 있습니다:

Validate.ok { name := "David", birthYear := 1984 }#eval checkInput 2023 {name := "David", birthYear := "1984"}

Validate.ok { name := "David", birthYear := 1984 }

Validate.errors { head := ("name", "Required"), tail := [("birth year", "Must be no later than 2023")] }#eval checkInput 2023 {name := "", birthYear := "2045"}

Validate.errors { head := ("name", "Required"), tail := [("birth year", "Must be no later than 2023")] }

Validate.errors { head := ("birth year", "Must be digits"), tail := [] }#eval checkInput 2023 {name := "David", birthYear := "syzygy"}

Validate.errors { head := ("birth year", "Must be digits"), tail := [] }

checkInput을 이용한 폼 검증은 Monad에 비해 Applicative가 갖는 핵심적인 장점을 보여줍니다. >>=는 첫 번째 단계의 값을 기반으로 프로그램의 나머지 실행을 수정할 수 있는 충분한 힘을 제공하기 때문에, 전달할 값을 첫 번째 단계로부터 반드시 받아야 합니다. 값을 받지 못하면(예: 오류가 발생한 경우), >>=는 프로그램의 나머지 부분을 실행할 수 없습니다. Validate는 그럼에도 불구하고 프로그램의 나머지 부분을 실행하는 것이 왜 유용할 수 있는지를 보여줍니다: 이전 데이터가 필요하지 않은 경우, 프로그램의 나머지 부분을 실행하면 유용한 정보(이 경우 더 많은 검증 오류)를 얻을 수 있습니다. Applicative의 <*>는 결과를 재결합하기 전에 두 인자를 모두 실행할 수 있습니다. 마찬가지로, >>=는 순차적 실행을 강제합니다. 각 단계는 다음 단계가 실행되기 전에 완료되어야 합니다. 이는 일반적으로 유용하지만, 프로그램의 실제 데이터 의존성으로부터 자연스럽게 발생하는 서로 다른 스레드들의 병렬 실행을 불가능하게 만듭니다. Monad와 같이 더 강력한 추상화는 API 소비자가 사용할 수 있는 유연성을 높이지만, API 구현자가 사용할 수 있는 유연성은 감소시킵니다.