5.2. Applicative Functors🔗

애플리커티브 펑터는 pure와 seq라는 두 연산을 추가로 제공하는 펑터다. pure는 Monad에서 사용하는 것과 같은 연산자다. 실제로 Monad가 Applicative를 상속하기 때문이다. seq는 map과 매우 비슷하며, 함수를 사용해 데이터 타입의 내용을 변환한다. 하지만 seq에서는 함수 자체가 데이터 타입 안에 들어 있다: f (α → β) → (Unit → f α) → f β. 함수가 f 타입 안에 있으므로 Applicative 인스턴스가 함수 적용 방식을 제어할 수 있지만, Functor.map은 조건 없이 함수를 적용한다. 두 번째 인수의 타입이 Unit →으로 시작하는 것은 함수가 절대 적용되지 않을 경우 seq 정의가 단락할 수 있게 하기 위해서다.

이 단락 동작의 가치는 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 ()

이 단락 동작은 함수 자체가 아니라 함수를 둘러싼 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. A Non-Monadic Applicative🔗

양식의 사용자 입력을 검증할 때는 일반적으로 오류를 하나씩 제공하기보다 한 번에 여러 오류를 제공하는 것이 가장 좋다. 이렇게 하면 사용자는 필드별로 오류를 고치며 재촉받는 느낌을 받지 않고 컴퓨터를 만족시키려면 무엇이 필요한지 한눈에 볼 수 있다.

이상적으로는 사용자 입력을 검증하는 함수의 타입에 검증 과정이 드러나야 한다. 구체적인 데이터 타입을 반환해야 한다. 예를 들어 텍스트 상자에 숫자가 들어 있는지 확인한다면 실제 숫자 타입을 반환해야 한다. 검증 루틴은 입력이 검증을 통과하지 못할 때 예외를 던질 수 있다. 하지만 예외에는 큰 단점이 있다. 첫 번째 오류에서 프로그램을 종료하므로 오류 목록을 누적할 수 없다.

반면 오류 목록을 누적한 뒤 비어 있지 않으면 실패하는 일반적인 설계 패턴도 문제가 있다. 입력 데이터의 각 하위 부분을 검증하는 중첩된 if 문이 길게 이어지면 유지하기 어렵고 오류 메시지 한두 개를 놓치기 쉽다. 이상적으로는 새 값을 반환하면서도 오류 메시지를 자동으로 추적하고 누적하는 API로 검증을 수행할 수 있어야 한다.

Validate라는 애플리커티브 펑터는 이런 방식의 API를 구현하는 한 방법을 제공한다. Except 모나드처럼 Validate는 검증된 데이터를 정확히 나타내는 새 값을 구성할 수 있게 한다. Except와 달리 목록이 비어 있는지 확인하는 것을 잊을 위험 없이 여러 오류를 누적할 수 있다.

5.2.1.1. User Input🔗

사용자 입력의 예로 다음 구조체를 보자.

structure RawInput where
  name : String
  birthYear : String

구현할 업무 논리는 다음과 같다.

이름은 비어 있으면 안 된다.
출생 연도는 숫자이고 음수가 아니어야 한다.
출생 연도는 1900년보다 커야 하고, 양식을 검증하는 연도 이하여야 한다.

이를 데이터 타입으로 나타내려면 서브타입이라는 새 기능이 필요하다. 이 도구를 사용하면 애플리커티브 펑터로 오류를 추적하고 이 규칙을 프레임워크에 구현하는 검증 프레임워크를 작성할 수 있다.

5.2.1.2. Subtypes🔗

이 조건을 나타내는 가장 쉬운 방법은 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! 🐙⟩

여기서는 decide가 구체적인 값을 요구하지만 대상 명제가 n + 1 > 0이므로 simp가 필요하다.

서브타입은 양날의 검이다. 검증 규칙을 효율적으로 표현할 수 있지만, 중요한 불변식을 위반하지 않는다는 것을 증명해야 하는 부담을 라이브러리 사용자에게 넘긴다. 일반적으로 서브타입은 라이브러리 내부에서 사용하고, 필요한 증명을 라이브러리 안에 두면서 모든 불변식이 만족됨을 자동으로 보장하는 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. Validated Input🔗

검증된 사용자 입력은 여러 기법으로 업무 논리를 표현하는 구조체다.

구조체 타입 자체가 유효성을 검사한 연도를 인코딩하므로 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')

NonEmptyList 생성자와 .errors를 함께 사용하면 조금 장황하다. 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 구현자가 사용할 수 있는 유연성은 낮춘다.