5.2. 애플리커티브 펑터🔗

애플리커티브 펑터는 pure와 seq라는 두 가지 연산을 추가로 사용할 수 있는 펑터입니다. Monad는 사실 Applicative를 상속하므로, pure는 Monad에서 사용하는 것과 같은 연산자입니다. seq는 map과 매우 비슷합니다. 즉, 함수를 사용하여 데이터 타입의 내용을 변환할 수 있게 해 줍니다. 그러나 seq에서는 함수 자체가 데이터 타입 안에 들어 있습니다: f (α → β) → (Unit → f α) → f β. Functor.map은 함수를 무조건 적용하지만, 함수가 타입 f 안에 들어 있으면 Applicative 인스턴스가 함수를 적용하는 방식을 제어할 수 있습니다. 두 번째 인자의 타입이 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# 같은 언어에서 함수의 인자는 왼쪽에서 오른쪽 순서로 평가됩니다. 앞선 인자가 일으키는 부수 효과는 뒤따르는 인자가 일으키는 부수 효과보다 먼저 발생합니다. 그러나 함수는 인자의 구체적인 값에 따라 달라지는 사용자 정의 단락 평가 연산자를 구현할 만큼 강력하지 않습니다.

일반적으로 seq를 직접 호출하지는 않습니다. 대신 <*> 연산자를 사용합니다. 이 연산자는 두 번째 인자를 fun () => ...로 감싸서 호출하는 쪽의 코드를 단순하게 만듭니다. 다시 말해, E1 <*> E2는 Seq.seq E1 (fun () => E2)의 문법 설탕입니다.

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:β⊢ α

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

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 구현자가 누릴 수 있는 유연성은 낮춥니다.