3.2. Type Classes and Polymorphism
주어진 함수의 어떤 오버로딩에서도 동작하는 함수를 작성하면 유용할 수 있다.
예를 들어 IO.println은 ToString 인스턴스가 있는 모든 타입에서 동작한다.
필요한 인스턴스를 대괄호로 감싸 이를 나타낸다. IO.println의 타입은 {α : Type} → [ToString α] → α → IO Unit이다.
이 타입은 IO.println이 α 타입의 인수를 받고 Lean이 이를 자동으로 결정해야 하며, α에 사용할 ToString 인스턴스가 있어야 함을 뜻한다.
반환값은 IO 동작이다.
3.2.1. Checking Polymorphic Functions' Types
암시 인수를 받거나 타입 클래스를 사용하는 함수의 타입을 확인하려면 추가 문법이 필요하다. 그냥 다음을 작성하면
#check (IO.println)메타변수가 포함된 타입을 얻는다.
이는 Lean이 암시 인수를 최대한 알아내려 하기 때문이다. 메타변수가 있다는 것은 아직 충분한 타입 정보를 찾지 못했다는 뜻이다.
함수 시그니처를 이해하려면 함수 이름 앞에 at 기호(@)를 붙여 이 기능을 억제할 수 있다.
#check @IO.println
Type 뒤의 u_1은 아직 소개하지 않은 Lean 기능을 사용한다.
지금은 Type의 이 매개변수들을 무시하라.
3.2.2. Defining Polymorphic Functions with Instance Implicits
리스트의 모든 원소를 더하는 함수에는 두 인스턴스가 필요하다. 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은 프로그램이 타입 검사기를 통과하게 하는 유일한 인수 값을 찾기 위해 단일화(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. Methods and Implicit Arguments
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. Exercises
3.2.4.1. Even Number Literals
앞 절의 연습문제에 나온 짝수 데이터 타입에 재귀적 인스턴스 검색을 사용하는 OfNat 인스턴스를 작성하라.
3.2.4.2. Recursive Instance Search Depth
Lean 컴파일러가 재귀적 인스턴스 검색을 시도하는 횟수에는 한계가 있다. 따라서 앞 연습문제에서 정의한 짝수 리터럴의 크기에도 한계가 생긴다. 실험으로 그 한계를 알아내라.