3.2. 타입 클래스와 다형성
주어진 함수가 어떤 방식으로 오버로딩되어 있든 동작하는 함수를 작성하면 유용할 때가 있습니다. 예를 들어, IO.println은 ToString의 인스턴스가 있는 모든 타입에 대해 동작합니다. 이는 필요한 인스턴스를 대괄호로 감싸서 나타냅니다. IO.println의 타입은 {α : Type} → [ToString α] → α → IO Unit입니다. 이 타입은 IO.println이 α 타입의 인자를 받는데 이 타입은 Lean이 자동으로 결정해야 하며, α에 대해 사용할 수 있는 ToString 인스턴스가 있어야 한다는 것을 나타냅니다. 이 함수는 IO 액션을 반환합니다.
3.2.1. 다형 함수의 타입 확인하기
암시적 인자를 받거나 타입 클래스를 사용하는 함수의 타입을 확인하려면 추가적인 문법이 필요합니다. 단순히 다음과 같이 작성하면
#check (IO.println)메타변수가 포함된 타입이 나옵니다:
이는 Lean이 암시적 인자를 최대한 찾아내려고 하기 때문이며, 메타변수가 있다는 것은 아직 그렇게 하는 데 필요한 타입 정보를 충분히 찾아내지 못했다는 뜻입니다. 함수의 시그니처를 파악하려면 함수 이름 앞에 at 기호(@)를 붙여 이 기능을 끌 수 있습니다.
#check @IO.println
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]#eval fourNats.sumOfContents
하지만 Pos 숫자의 리스트에 대해서는 그렇지 않습니다:
def fourPos : List Pos := [1, 2, 3, 4]#eval fourPos.sumOfContents
Lean 표준 라이브러리에는 이 함수가 포함되어 있으며, 그곳에서는 List.sum이라고 불립니다.
대괄호 안에 필요한 인스턴스를 명시한 것을 인스턴스 암시적 인자라고 합니다. 내부적으로 모든 타입 클래스는 각 오버로드된 연산마다 하나의 필드를 갖는 구조체를 정의합니다. 인스턴스는 그 구조체 타입의 값이며, 각 필드에는 구현이 들어 있습니다. 호출 지점에서 Lean은 각 인스턴스 암시적 인자에 전달할 인스턴스 값을 찾아야 합니다. 일반 암시적 인자와 인스턴스 암시적 인자의 가장 중요한 차이점은 Lean이 인자 값을 찾을 때 사용하는 전략입니다. 일반 암시적 인자의 경우, Lean은 단일화라는 기법을 사용하여 프로그램이 타입 검사기를 통과할 수 있게 하는 유일한 인자 값을 찾습니다. 이 과정은 함수 정의와 호출 지점에 관련된 구체적인 타입에만 의존합니다. 반면 인스턴스 암시적 인자의 경우, 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 컴파일러가 재귀적 인스턴스 탐색을 시도하는 횟수에는 한계가 있습니다. 이 때문에 이전 연습 문제에서 정의한 짝수 리터럴의 크기에도 한계가 생깁니다. 그 한계가 얼마인지 실험을 통해 알아내십시오.