5.7.1. 타입 클래스와 구조체🔗

내부적으로 타입 클래스는 구조체로 표현됩니다. 클래스를 정의하면 구조체가 정의되며, 추가로 빈 인스턴스 테이블이 생성됩니다. 인스턴스를 정의하면 해당 구조체를 타입으로 가지거나 그 구조체를 반환할 수 있는 함수인 값이 생성되며, 추가로 테이블에 항목이 추가됩니다. 인스턴스 검색은 인스턴스 테이블을 참조하여 인스턴스를 구성하는 것으로 이루어집니다. 구조체와 클래스는 모두 필드(즉, 메서드의 기본 구현)에 대한 기본값을 제공할 수 있습니다.

5.7.2. 구조체와 상속🔗

구조체는 다른 구조체를 상속할 수 있습니다. 내부적으로, 다른 구조체를 상속받은 구조체는 원래 구조체의 인스턴스를 필드로 포함합니다. 다시 말해, 상속은 합성으로 구현됩니다. 다중 상속을 사용하는 경우, 다이아몬드 문제를 피하기 위해 추가 부모 구조체들에서 고유한 필드만 사용되며, 일반적으로 부모 값을 추출하는 함수들은 대신 그 값을 구성하도록 조직됩니다. 레코드 점 표기법은 구조체 상속을 고려합니다.

타입 클래스는 추가적인 자동화가 적용된 구조체일 뿐이므로, 이러한 모든 기능을 타입 클래스에서도 사용할 수 있습니다. 기본 메서드와 함께 사용하면, 이를 통해 세밀하게 나뉜 인터페이스 계층을 만들 수 있으며, 그럼에도 클라이언트에게 큰 부담을 지우지 않는데, 이는 큰 클래스가 상속하는 작은 클래스들을 자동으로 구현할 수 있기 때문입니다.

5.7.3. 애플리커티브 펑터🔗

애플리커티브 펑터는 두 가지 추가 연산을 갖는 펑터입니다:

• pure는 Monad(모나드)와 동일한 연산자입니다

• seq는 펑터의 맥락에서 함수를 적용할 수 있게 해 줍니다.

모나드는 제어 흐름을 갖는 임의의 프로그램을 표현할 수 있지만, 애플리커티브 펑터는 함수 인자를 왼쪽에서 오른쪽으로만 실행할 수 있습니다. 이들은 능력이 덜 강력하기 때문에 해당 인터페이스에 맞추어 작성된 프로그램에게 제공하는 제어권이 더 적으며, 그만큼 메서드 구현자에게는 더 큰 자유도가 주어집니다. 몇몇 유용한 타입은 Applicative는 구현할 수 있지만 Monad(모나드)는 구현할 수 없습니다.

실제로 타입 클래스 Functor, Applicative, Monad는 능력의 위계를 이룹니다. 위계를 따라 Functor에서 Monad로 올라가면 더 강력한 프로그램을 작성할 수 있지만, 더 강력한 클래스를 구현하는 타입은 더 적습니다. 다형적 프로그램은 가능한 한 약한 추상을 사용하도록 작성해야 하는 반면, 데이터 타입에는 가능한 한 강력한 인스턴스가 주어져야 합니다. 이는 코드 재사용을 극대화합니다. 더 강력한 타입 클래스는 덜 강력한 타입 클래스를 확장하는데, 이는 Monad(모나드)의 구현이 Functor(펑터)와 Applicative(애플리커티브 펑터)의 구현을 공짜로 제공한다는 것을 의미합니다.

각 클래스에는 구현해야 할 메서드 집합과 해당 메서드에 대한 추가 규칙을 명시하는 계약이 있습니다. 이러한 인터페이스를 대상으로 작성된 프로그램은 추가 규칙이 준수될 것을 기대하며, 그렇지 않을 경우 버그가 발생할 수 있습니다. Applicative의 메서드로 Functor의 메서드를 구현한 기본 구현과, Monad의 메서드로 Applicative의 메서드를 구현한 기본 구현은 이 규칙들을 따릅니다.

5.7.4. 유니버스🔗

Lean을 프로그래밍 언어이자 정리 증명기로 사용할 수 있도록 하려면, 언어에 몇 가지 제약이 필요합니다. 여기에는 재귀 함수에 대한 제약이 포함되는데, 이는 모든 재귀 함수가 종료되거나 partial로 표시되고 공허하지 않은 반환 타입을 갖도록 작성되었음을 보장합니다. 또한, 특정 종류의 논리적 역설을 타입으로 표현하는 것이 불가능해야 합니다.

특정 역설을 배제하는 제약 조건 중 하나는 모든 타입이 유니버스에 배정된다는 것입니다. 유니버스는 Prop, Type, Type 1, Type 2 등과 같은 타입입니다. 이러한 타입들은 다른 타입을 기술합니다—마치 0과 17이 Nat으로 기술되듯이, Nat 자체는 Type으로 기술되고, Type은 Type 1로 기술됩니다. 타입을 인자로 받는 함수의 타입은 인자의 유니버스보다 더 큰 유니버스여야 합니다.

각 선언된 데이터 타입은 고유한 유니버스를 가지므로, data와 같은 타입을 사용하는 코드를 작성하는 일은 곧 성가셔질 것입니다. 각 다형적 타입이 Type 1로부터 인자를 받도록 하려면 매번 복사-붙여넣기를 해야 하기 때문입니다. 유니버스 다형성이라는 기능은 일반적인 다형성이 프로그램으로 하여금 타입을 인자로 받을 수 있게 하는 것과 마찬가지로, Lean 프로그램과 데이터타입이 유니버스 수준을 인자로 받을 수 있게 합니다. 일반적으로 Lean 라이브러리는 다형적 연산의 라이브러리를 구현할 때 유니버스 다형성을 사용해야 합니다.