3.8.1. 타입 클래스와 오버로딩🔗

타입 클래스는 함수와 연산자를 오버로딩하기 위한 Lean의 메커니즘입니다. 다형 함수는 여러 타입에 사용할 수 있지만, 어떤 타입에 사용하든 동일한 방식으로 동작합니다. 예를 들어, 두 리스트를 이어 붙이는 다형 함수는 리스트 원소의 타입이 무엇이든 사용할 수 있지만, 구체적으로 어떤 타입이 주어졌는지에 따라 다르게 동작할 수는 없습니다. 반면에 타입 클래스로 오버로딩된 연산 역시 여러 타입에 사용할 수 있습니다. 하지만 각 타입은 오버로드된 연산에 대한 자체 구현을 필요로 합니다. 이는 어떤 타입이 주어지느냐에 따라 동작이 달라질 수 있음을 의미합니다.

타입 클래스는 이름, 매개변수, 그리고 타입이 지정된 여러 이름으로 이루어진 본문을 가집니다. 이름은 오버로드된 연산을 가리키는 수단이고, 매개변수는 정의의 어떤 측면을 오버로드할 수 있는지를 결정하며, 본문은 오버로드 가능한 연산의 이름과 타입 시그니처를 제공합니다. 각 오버로드 가능한 연산을 타입 클래스의 메서드라고 합니다. 타입 클래스는 일부 메서드의 기본 구현을 다른 메서드를 이용해 제공할 수 있으므로, 구현자는 필요하지 않은 경우 각 오버로드를 일일이 직접 정의하지 않아도 됩니다.

타입 클래스의 인스턴스는 주어진 매개변수에 대한 메서드 구현을 제공합니다. 인스턴스는 다형적일 수 있으며, 이 경우 다양한 매개변수에 대해 동작할 수 있습니다. 또한 특정 타입에 대해 더 효율적인 버전이 있는 경우에는 기본 메서드의 더 구체적인 구현을 선택적으로 제공할 수도 있습니다.

타입 클래스 매개변수는 입력 매개변수(기본값)이거나 출력 매개변수(outParam 수식어로 표시)입니다. Lean은 모든 입력 매개변수가 더 이상 메타변수가 아니게 될 때까지 인스턴스 탐색을 시작하지 않지만, 출력 매개변수는 인스턴스를 탐색하는 도중에 결정될 수 있습니다. 타입 클래스의 매개변수가 반드시 타입일 필요는 없으며, 일반적인 값일 수도 있습니다. 자연수 리터럴을 오버로드하는 데 사용되는 OfNat 타입 클래스는 오버로드되는 Nat 자체를 매개변수로 받으므로, 인스턴스가 허용되는 수를 제한할 수 있습니다.

인스턴스에는 @[default_instance] 속성을 붙일 수 있습니다. 기본 인스턴스로 지정된 인스턴스는 타입에 메타변수가 있어서 Lean이 인스턴스를 찾지 못하게 되는 경우에 대체 수단으로 선택됩니다.

3.8.2. 공통 문법을 위한 타입 클래스🔗

Lean의 중위 연산자 대부분은 타입 클래스를 통해 오버라이드됩니다. 예를 들어 덧셈 연산자는 Add라는 타입 클래스에 대응합니다. 이러한 연산자 대부분에는 두 인자의 타입이 같지 않아도 되는 이종(heterogeneous) 버전이 있습니다. 이러한 이종 연산자는 HAdd처럼 이름이 H로 시작하는 버전의 클래스를 사용하여 오버로드됩니다.

인덱싱 문법은 GetElem이라는 타입 클래스를 통해 오버로드되며, 이 타입 클래스에는 증명이 관여합니다. GetElem에는 출력 매개변수가 두 개 있습니다. 하나는 컬렉션에서 꺼낼 원소의 타입이고, 다른 하나는 인덱스 값이 컬렉션의 범위 안에 있다는 증거로 무엇을 인정할지 결정하는 데 쓸 수 있는 함수입니다. 이 증거는 명제로 기술되며, 배열 인덱싱이 사용되면 Lean은 이 명제를 증명하려고 시도합니다. Lean이 컴파일 시점에 리스트나 배열 접근 연산이 범위 안에 있는지 확인할 수 없는 경우, 인덱싱 문법에 ?를 덧붙여 그 확인을 런타임으로 미룰 수 있습니다.

3.8.3. 펑터🔗

펑터는 매핑 연산을 지원하는 다형 타입입니다. 이 매핑 연산은 다른 구조는 전혀 바꾸지 않고 모든 원소를 “제자리에서” 변환합니다. 예를 들어, 리스트는 펑터이며, 매핑 연산은 리스트의 항목을 빠뜨리거나 중복시키거나 뒤섞어서는 안 됩니다.

펑터는 map을 가진다는 점으로 정의되지만, Lean의 Functor 타입 클래스에는 기본 메서드가 하나 더 있습니다. 이 메서드는 값에 상수 함수를 매핑하는 역할을 하며, 다형 타입 변수로 주어진 타입을 가진 모든 값을 같은 새 값으로 바꿉니다. 일부 펑터에서는 전체 구조를 순회하는 것보다 더 효율적으로 이 작업을 수행할 수 있습니다.

3.8.4. 인스턴스 파생하기🔗

많은 타입 클래스에는 매우 표준적인 구현이 있습니다. 예를 들어 불리언 동등성 클래스 BEq는 보통 먼저 두 인자가 같은 생성자로 만들어졌는지 확인한 다음, 그 생성자의 인자들이 모두 같은지 확인하는 방식으로 구현됩니다. 이러한 클래스의 인스턴스는 자동으로 만들 수 있습니다.

귀납적 타입이나 구조체를 정의할 때 선언 끝에 deriving 절을 붙이면 인스턴스가 자동으로 생성됩니다. 또한 deriving instance ... for ... 명령을 사용하면 데이터 타입 정의 바깥에서도 인스턴스를 생성할 수 있습니다. 인스턴스를 파생할 수 있는 클래스는 각각 별도의 처리가 필요하므로 모든 클래스를 파생할 수 있는 것은 아닙니다.

3.8.5. 강제 변환🔗

강제 변환을 사용하면 Lean은 데이터를 한 타입에서 다른 타입으로 바꾸는 함수 호출을 삽입하여, 원래라면 컴파일 타임 오류가 되었을 상황을 복구할 수 있습니다. 예를 들어, 임의의 타입 α에서 Option α 타입으로의 강제 변환 덕분에 some 생성자를 쓰지 않고 값을 직접 쓸 수 있습니다. 이로써 Option은 객체 지향 언어의 nullable 타입과 더 비슷하게 동작합니다.

강제 변환에는 여러 종류가 있습니다. 각 강제 변환은 서로 다른 종류의 오류로부터 복구할 수 있으며, 각각 고유한 타입 클래스로 표현됩니다. Coe 클래스는 타입 오류로부터 복구하는 데 사용됩니다. Lean은 β 타입을 기대하는 문맥에서 α 타입의 표현식을 만나면, 먼저 α를 β로 변환할 수 있는 강제 변환들을 하나의 사슬로 엮으려고 시도하며, 이것이 불가능할 때에만 오류를 표시합니다. CoeDep 클래스는 강제 변환되는 특정 값을 추가 매개변수로 받으므로, 그 값에 대해 추가적인 타입 클래스 탐색을 수행하거나 인스턴스에서 생성자를 사용하여 변환의 범위를 제한할 수 있습니다. CoeFun 클래스는 함수 적용을 컴파일할 때 원래라면 "함수가 아님" 오류가 발생했을 상황을 가로채어, 가능한 경우 함수 위치에 있는 값을 실제 함수로 변환할 수 있게 합니다.