5.7.1. Type Classes and Structures🔗

내부적으로 타입 클래스는 구조체로 표현된다. 클래스를 정의하면 구조체가 정의되고 빈 인스턴스 테이블도 만들어진다. 인스턴스를 정의하면 구조체를 타입으로 갖는 값 또는 구조체를 반환하는 함수가 만들어지고, 테이블에 항목도 추가된다. 인스턴스 검색은 인스턴스 테이블을 참조해 인스턴스를 구성하는 과정이다. 구조체와 클래스 모두 필드의 기본값(메서드의 기본 구현)을 제공할 수 있다.

5.7.2. Structures and Inheritance🔗

구조체는 다른 구조체를 상속할 수 있다. 내부적으로 다른 구조체를 상속하는 구조체는 원래 구조체의 인스턴스를 필드로 포함한다. 즉 상속은 합성으로 구현된다. 다중 상속을 사용할 때는 다이아몬드 문제를 피하기 위해 추가 부모 구조체에서 고유한 필드만 사용하며, 보통 부모 값을 추출하는 함수는 대신 부모 값을 구성하도록 조직된다. 레코드 점 표기법은 구조체 상속을 고려한다.

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

5.7.3. Applicative Functors🔗

Applicative functor는 두 연산이 추가된 Functor다.

• pure, Monad의 것과 같은 연산자

• 펑터의 문맥에서 함수를 적용할 수 있게 하는 seq

Monad는 제어 흐름이 있는 임의의 프로그램을 표현할 수 있지만, Applicative functor는 함수 인수를 왼쪽에서 오른쪽으로만 실행할 수 있다. 더 약하므로 이 인터페이스를 대상으로 작성한 프로그램에는 제어력이 덜 제공되지만, 메서드 구현자에게는 더 큰 자유가 주어진다. 유용한 일부 타입은 Applicative를 구현할 수 있지만 Monad는 구현하지 못한다.

실제로 Functor, Applicative, Monad 타입 클래스는 강력함의 계층 구조를 이룬다. 계층 구조에서 Functor에서 Monad 쪽으로 올라갈수록 더 강력한 프로그램을 작성할 수 있지만, 더 강력한 클래스를 구현하는 타입은 줄어든다. 다형적 프로그램은 가능한 한 약한 추상화를 사용하도록 작성하고, 데이터 타입에는 가능한 한 강력한 인스턴스를 제공해야 한다. 이렇게 하면 코드 재사용이 최대화된다. 더 강력한 타입 클래스는 더 약한 타입 클래스를 확장하므로 Monad 구현은 Functor와 Applicative 구현도 자동으로 제공한다.

각 클래스에는 구현할 메서드 집합과 메서드에 대한 추가 규칙을 지정하는 대응 계약이 있다. 이 인터페이스를 대상으로 작성한 프로그램은 추가 규칙이 지켜진다고 가정하며, 지켜지지 않으면 버그가 생길 수 있다. Functor의 메서드를 Applicative의 메서드로, Applicative의 메서드를 Monad의 메서드로 정의한 기본 구현은 이 규칙을 따른다.

5.7.4. Universes🔗

Lean을 프로그래밍 언어이자 정리 증명기로 사용하려면 언어에 일부 제한이 필요하다. 여기에는 재귀 함수가 모두 종료하거나 partial로 표시되고 비공허 타입을 반환하도록 작성되어야 한다는 제한이 포함된다. 또한 특정 종류의 논리적 역설을 타입으로 표현할 수 없어야 한다.

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

선언된 각 데이터 타입에는 유니버스가 있으므로 데이터처럼 타입을 사용하는 코드를 작성하면 곧 성가셔진다. 각 다형 타입이 Type 1에서 인수를 받도록 복사해 붙여 넣어야 하기 때문이다. 유니버스 다형성이라는 기능을 사용하면 일반 다형성이 프로그램이 타입을 인수로 받게 하듯이 Lean 프로그램과 데이터 타입이 유니버스 레벨을 인수로 받게 할 수 있다. 일반적으로 Lean 라이브러리는 다형 연산 라이브러리를 구현할 때 유니버스 다형성을 사용해야 한다.