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

타입 클래스는 함수와 연산자를 오버로딩하기 위한 Lean의 메커니즘입니다. 다형 함수는 여러 타입에 사용할 수 있지만, 어떤 타입에 사용하든 동일한 방식으로 동작합니다. 예를 들어, 두 리스트를 이어붙이는 다형 함수는 리스트에 담긴 항목의 타입이 무엇이든 상관없이 사용할 수 있지만, 어떤 특정 타입이 발견되었는지에 따라 다른 동작을 하도록 할 수는 없습니다. 반면, 타입 클래스로 오버로드된 연산은 여러 타입에 사용할 수도 있습니다. 그러나 각 타입은 오버로드된 연산에 대해 자신만의 구현을 필요로 합니다. 즉, 어떤 타입이 제공되는지에 따라 동작이 달라질 수 있습니다.

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

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

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

인스턴스는 @[default_instance] 속성으로 표시될 수 있습니다. 인스턴스가 기본 인스턴스인 경우, 타입에 메타변수가 존재하여 Lean이 인스턴스를 찾는 데 실패할 상황에서 대체 수단으로 선택됩니다.

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

Lean의 대부분의 중위 연산자는 타입 클래스로 오버라이드됩니다. 예를 들어, 덧셈 연산자는 Add라는 타입 클래스에 대응됩니다. 이러한 연산자 대부분에는 두 인자가 같은 타입일 필요가 없는 이종(heterogeneous) 버전이 대응됩니다. 이러한 이종(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은 객체 지향 언어의 널러블 타입처럼 동작하게 됩니다.

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