3.8.1. Type Classes and Overloading🔗

타입 클래스는 함수와 연산자를 오버로딩하는 Lean의 메커니즘이다. 다형 함수는 여러 타입에서 사용할 수 있지만 어떤 타입에서 사용하든 같은 방식으로 동작한다. 예를 들어 두 리스트를 이어 붙이는 다형 함수는 리스트 원소의 타입과 무관하게 사용할 수 있지만, 특정 타입인지에 따라 다르게 동작하게 만들 수는 없다. 반면 타입 클래스로 오버로딩한 연산도 여러 타입에서 사용할 수 있다. 그러나 각 타입에는 오버로딩된 연산의 고유한 구현이 필요하다. 따라서 제공된 타입에 따라 동작이 달라질 수 있다.

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

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

타입 클래스 매개변수는 입력 매개변수(기본값) 또는 출력 매개변수(outParam 수정자로 표시)다. Lean은 모든 입력 매개변수가 더 이상 메타변수가 아닐 때까지 인스턴스 검색을 시작하지 않지만, 출력 매개변수는 인스턴스를 검색하는 동안 해결될 수 있다. 타입 클래스 매개변수는 반드시 타입일 필요가 없으며 일반 값일 수도 있다. 자연수 리터럴을 오버로딩하는 OfNat 타입 클래스는 오버로딩된 Nat 자체를 매개변수로 받아 인스턴스가 허용할 수를 제한하게 한다.

인스턴스에는 @[default_instance] 속성을 표시할 수 있다. 기본 인스턴스는 타입에 메타변수가 있어 Lean이 인스턴스를 찾지 못할 때 대안으로 선택된다.

3.8.2. Type Classes for Common Syntax🔗

Lean의 대부분 중위 연산자는 타입 클래스로 오버로딩된다. 예를 들어 덧셈 연산자는 Add라는 타입 클래스에 대응한다. 이 연산자 대부분에는 두 인수가 같은 타입일 필요가 없는 이종 버전이 있다. 이 이종 연산자는 HAdd처럼 이름이 H로 시작하는 클래스 버전으로 오버로딩된다.

인덱싱 문법은 증명을 포함하는 GetElem 타입 클래스로 오버로딩된다. GetElem에는 두 출력 매개변수가 있다. 컬렉션에서 추출할 원소의 타입과 인덱스가 범위 안이라는 증거를 결정하는 함수다. 이 증거는 명제로 표현되며, 배열 인덱싱을 사용할 때 Lean이 이 명제를 증명하려고 한다. 컴파일 타임에 리스트나 배열 접근이 범위 안에 있는지 확인할 수 없으면 인덱싱 문법 뒤에 ?를 붙여 검사를 런타임으로 미룰 수 있다.

3.8.3. Functors🔗

Functor는 매핑 연산을 지원하는 다형 타입이다. 이 매핑 연산은 다른 구조를 바꾸지 않고 모든 원소를 “제자리에서” 변환한다. 예를 들어 리스트는 Functor이며 매핑 연산은 리스트의 원소를 삭제하거나 복제하거나 뒤섞어서는 안 된다.

Functor는 map으로 정의되지만, Lean의 Functor 타입 클래스에는 상수 함수를 값에 매핑하는 추가 기본 메서드가 있다. 이 메서드는 다형 타입 변수가 지정한 타입의 모든 값을 같은 새 값으로 바꾼다. 일부 Functor에서는 전체 구조를 순회하는 것보다 이를 더 효율적으로 할 수 있다.

3.8.4. Deriving Instances🔗

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

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

3.8.5. Coercions🔗

강제 변환은 한 타입의 데이터를 다른 타입으로 변환하는 함수 호출을 삽입하여 보통 컴파일 타임 오류가 될 상황을 Lean이 복구하게 한다. 예를 들어 임의의 타입 α에서 Option α으로의 강제 변환을 사용하면 some 생성자 없이 값을 직접 쓸 수 있어 Option이 객체 지향 언어의 nullable 타입처럼 동작한다.

강제 변환에는 여러 종류가 있다. 각각 다른 종류의 오류를 복구하며, 고유한 타입 클래스로 표현된다. Coe 클래스는 타입 오류를 복구하는 데 사용된다. Lean이 α 타입 표현식을 β 타입을 기대하는 문맥에서 만나면, 먼저 α를 β로 바꾸는 강제 변환 사슬을 이어 붙이려 한다. 불가능할 때만 오류를 표시한다. CoeDep 클래스는 강제 변환할 특정 값을 추가 매개변수로 받아 값에 대한 추가 타입 클래스 검색을 허용하거나, 인스턴스의 생성자로 변환 범위를 제한하게 한다. CoeFun 클래스는 함수 적용을 컴파일할 때 생길 “함수가 아님” 오류를 가로채고, 가능하면 함수 위치의 값을 실제 함수로 변환한다.