3.2. 타입 클래스와 다형성🔗

주어진 함수의 어떤 오버로딩에 대해서도 동작하는 함수를 작성하는 것이 유용할 수 있습니다. 예를 들어, IO.println은 ToString의 인스턴스가 있는 모든 타입에 대해 작동합니다. 이는 필요한 인스턴스를 대괄호로 감싸서 표시합니다. 즉 IO.println의 타입은 {α : Type} → [ToString α] → α → IO Unit입니다. 이 타입은 IO.println이 α 타입의 인자를 받으며, 이 타입은 Lean이 자동으로 결정해야 하고, α에 대해 사용 가능한 ToString 인스턴스가 있어야 함을 나타냅니다. 이는 IO 액션을 반환합니다.

3.2.1. 다형 함수의 타입 검사하기🔗

암시적 인자를 받거나 타입 클래스를 사용하는 함수의 타입을 확인하려면 몇 가지 추가 구문을 사용해야 합니다. 단순히 다음과 같이 작성하면

IO.println : ?m.1 → IO Unit#check (IO.println)

메타변수가 포함된 타입을 산출합니다:

IO.println : ?m.1 → IO Unit

이는 Lean이 암시적 인자를 발견하기 위해 최선을 다하기 때문이며, 메타변수의 존재는 그렇게 하기에 충분한 타입 정보를 아직 발견하지 못했음을 나타냅니다. 함수의 시그니처를 이해하기 위해, 함수 이름 앞에 골뱅이 기호(@)를 붙여 이 기능을 억제할 수 있습니다:

@IO.println : {α : Type u_1} → [ToString α] → α → IO Unit#check @IO.println

@IO.println : {α : Type u_1} → [ToString α] → α → IO Unit

Type 뒤에 u_1이 있는데, 이는 아직 소개되지 않은 Lean의 기능을 사용합니다. 지금은 Type의 이 매개변수들을 무시하십시오.

3.2.2. 인스턴스 암묵 인자를 사용한 다형 함수 정의🔗

리스트의 모든 항목을 합산하는 함수에는 두 가지 인스턴스가 필요합니다: Add는 항목들을 더할 수 있게 해주며, 0에 대한 OfNat 인스턴스는 빈 리스트에 대해 반환할 적절한 값을 제공합니다.

def List.sumOfContents [Add α] [OfNat α 0] : List α → α
  | [] => 0
  | x :: xs => x + xs.sumOfContents

이 함수는 OfNat α 0 대신 Zero α 요구 사항으로도 정의할 수 있습니다. 두 방식은 동등하지만, Zero α가 더 읽기 쉬울 수 있습니다:

def List.sumOfContents [Add α] [Zero α] : List α → α
  | [] => 0
  | x :: xs => x + xs.sumOfContents

이 함수는 Nat의 리스트에 사용할 수 있습니다:

def fourNats : List Nat := [1, 2, 3, 4]10#eval fourNats.sumOfContents

하지만 Pos 숫자 목록에는 해당하지 않습니다:

def fourPos : List Pos := [1, 2, 3, 4]

#eval failed to synthesize instance of type class
  Zero Pos

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.fourPos.sumOfContents

failed to synthesize instance of type class
  Zero Pos

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Lean 표준 라이브러리에는 이 함수가 포함되어 있으며, List.sum이라고 불립니다.

대괄호 안에 필요한 인스턴스를 명시하는 것을 instance implicits라고 합니다. 내부적으로 모든 타입 클래스는 오버로드된 연산마다 필드를 하나씩 갖는 구조체를 정의합니다. 인스턴스는 해당 구조체 타입의 값이며, 각 필드는 구현을 담고 있습니다. 호출 지점에서, Lean은 각 인스턴스 암시적 인자에 대해 전달할 인스턴스 값을 찾는 역할을 담당합니다. 일반 암묵 인자와 인스턴스 암묵 인자 사이의 가장 중요한 차이점은 Lean이 인자 값을 찾을 때 사용하는 전략에 있습니다. 일반적인 암시적 인자의 경우, Lean은 프로그램이 타입 검사기를 통과할 수 있도록 하는 단일한 고유 인자 값을 찾기 위해 통합(unification)이라는 기법을 사용합니다. 이 과정은 함수의 정의와 호출 지점에 관련된 구체적인 타입에만 의존합니다. 인스턴스 암묵 인자의 경우, Lean은 대신 내장된 인스턴스 값 테이블을 참조합니다.

Pos에 대한 OfNat 인스턴스가 자연수 n을 자동 암시적 인자로 취했던 것처럼, 인스턴스도 그 자체로 인스턴스 암시적 인자를 취할 수 있습니다. 다형성에 관한 절에서는 다형적인 점 타입을 제시했습니다:

structure PPoint (α : Type) where
  x : α
  y : α

점의 덧셈은 기저에 있는 x 및 y 필드를 더해야 합니다. 따라서 PPoint에 대한 Add 인스턴스는 이 필드들이 갖는 타입이 무엇이든 그 타입에 대한 Add 인스턴스를 필요로 합니다. 다시 말해, PPoint에 대한 Add 인스턴스는 α에 대한 추가적인 Add 인스턴스를 필요로 합니다:

instance [Add α] : Add (PPoint α) where
  add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }

Lean은 두 점의 덧셈을 만나면 이 인스턴스를 검색하여 찾아냅니다. 그런 다음 Add α 인스턴스에 대한 추가 검색을 수행합니다.

이런 방식으로 구성된 인스턴스 값은 타입 클래스의 구조체 타입에 속하는 값입니다. 성공적인 재귀적 인스턴스 검색은 다른 구조체 값에 대한 참조를 가진 구조체 값을 결과로 산출합니다. Add (PPoint Nat)의 인스턴스는 찾아낸 Add Nat의 인스턴스에 대한 참조를 포함합니다.

이러한 재귀적 탐색 과정은 타입 클래스가 단순한 오버로드 함수보다 훨씬 더 강력한 기능을 제공한다는 것을 의미합니다. 다형적 인스턴스로 이루어진 라이브러리란, 원하는 타입만 주어지면 컴파일러가 스스로 조립할 수 있는 코드 구성 요소들의 집합입니다. 인스턴스 인자를 받는 다형 함수는 타입 클래스 메커니즘이 배후에서 보조 함수를 조립하도록 하는 잠재적인 요청입니다. API의 클라이언트는 필요한 모든 부품을 직접 손으로 연결해야 하는 부담에서 벗어납니다.

3.2.3. 메서드와 암시적 인자🔗

OfNat.ofNat의 타입은 의외일 수 있습니다. 이는 : {α : Type} → (n : Nat) → [OfNat α n] → α이며, 여기서 Nat 인자 n은 명시적 함수 매개변수로 나타납니다. 그러나 메서드의 선언에서, ofNat는 단순히 α 타입을 갖습니다. 이러한 겉보기 불일치는 타입 클래스를 선언하면 실제로는 다음과 같은 결과가 발생하기 때문입니다:

오버로드된 각 연산의 구현을 담을 구조체 타입
클래스와 같은 이름을 가진 네임스페이스입니다
각 메서드에 대해, 인스턴스로부터 그 구현을 가져오는 클래스 네임스페이스 내의 함수

이는 새로운 구조체를 선언하면 접근자 함수도 함께 선언되는 방식과 유사합니다. 주된 차이점은 구조체의 접근자는 구조체 값을 명시적 매개변수로 받는 반면, 타입 클래스의 메서드는 인스턴스 값을 Lean이 자동으로 찾아야 하는 인스턴스 암묵적 매개변수로 받는다는 것입니다.

Lean이 인스턴스를 찾으려면 해당 매개변수가 사용 가능해야 합니다. 즉, 타입 클래스의 각 매개변수는 인스턴스보다 앞에 나오는 메서드의 매개변수여야 합니다. 이러한 매개변수는 암시적일 때 가장 편리한데, Lean이 그 값을 알아내는 작업을 대신 수행하기 때문입니다. 예를 들어, Add.add는 {α : Type} → [Add α] → α → α → α라는 타입을 가집니다. 이 경우 타입 매개변수 α는 암묵적일 수 있는데, Add.add의 인자들이 사용자가 어떤 타입을 의도했는지에 대한 정보를 제공하기 때문입니다. 이 타입은 Add 인스턴스를 검색하는 데 사용될 수 있습니다.

그러나 OfNat.ofNat의 경우, 디코딩할 특정 Nat 리터럴은 다른 어떤 매개변수의 타입 일부로도 나타나지 않습니다. 이는 Lean이 암시적 매개변수 n을 알아내려 할 때 사용할 수 있는 정보가 전혀 없다는 것을 의미합니다. 그 결과는 매우 불편한 API가 될 것입니다. 따라서 이러한 경우 Lean은 해당 타입 클래스 메서드에 명시적 매개변수를 사용합니다.

3.2.4. 연습문제🔗

3.2.4.1. 짝수 숫자 리터럴🔗

이전 절의 연습문제에 나온 짝수 데이터 타입에 대해, 재귀적 인스턴스 탐색을 사용하는 OfNat 인스턴스를 작성하십시오.

3.2.4.2. 재귀적 인스턴스 탐색 깊이🔗

Lean 컴파일러가 재귀적 인스턴스 탐색을 시도하는 횟수에는 한계가 있습니다. 이는 이전 연습문제에서 정의한 짝수 리터럴의 크기에도 제한을 둡니다. 실험을 통해 그 한계가 무엇인지 확인하십시오.