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

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

5.7.2. 구조체와 상속🔗

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

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

5.7.3. 애플리커티브 펑터🔗

애플리커티브 펑터는 두 가지 연산이 추가로 있는 펑터입니다:

• Monad와 같은 연산자인 pure

• 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로 기술됩니다. 타입을 인자로 받는 함수의 타입은 그 인자의 유니버스보다 더 큰 유니버스여야 합니다.

선언된 각 데이터 타입에는 유니버스가 있기 때문에, 타입을 데이터처럼 사용하는 코드를 작성하다 보면 금세 번거로워집니다. 각 다형 타입을 복사해 붙여 넣어 Type 1에서도 인자를 받도록 만들어야 하기 때문입니다. 일반적인 다형성이 프로그램에서 타입을 인자로 받을 수 있게 하는 것처럼, 유니버스 다형성이라는 기능은 Lean 프로그램과 데이터 타입에서 유니버스 레벨을 인자로 받을 수 있게 합니다. 일반적으로 Lean 라이브러리는 다형적 연산 라이브러리를 구현할 때 유니버스 다형성을 사용해야 합니다.