5.1. Structures and Inheritance
Functor, Applicative, Monad의 전체 정의를 이해하려면 또 다른 Lean 기능인 구조체 상속이 필요하다.
구조체 상속을 사용하면 한 구조체 타입이 다른 구조체의 인터페이스를 제공하면서 필드를 추가할 수 있다.
이는 분류학적 관계가 분명한 개념을 모델링할 때 유용하다.
예를 들어 신화 속 생물을 모델링해 보자.
어떤 생물은 크고 어떤 생물은 작다:
structure MythicalCreature where
large : Bool
deriving Repr
내부적으로 MythicalCreature 구조체를 정의하면 mk라는 생성자 하나를 가진 귀납 타입이 만들어진다:
#check MythicalCreature.mk
마찬가지로 생성자에서 필드를 실제로 추출하는 함수 MythicalCreature.large도 만들어진다:
#check MythicalCreature.large대부분의 옛이야기에서는 모든 괴물을 어떤 방법으로든 물리칠 수 있다. 괴물의 설명에는 크기와 함께 이를 나타내는 정보가 포함되어야 한다:
structure Monster extends MythicalCreature where
vulnerability : String
deriving Repr
헤더의 extends MythicalCreature는 모든 괴물이 신화 속 생물이기도 하다는 뜻이다.
Monster를 정의하려면 MythicalCreature의 필드와 Monster가 추가하는 필드를 모두 제공해야 한다.
트롤은 햇빛에 약한 큰 괴물이다:
def troll : Monster where
large := true
vulnerability := "sunlight"
내부적으로 상속은 합성으로 구현된다.
생성자 Monster.mk는 인수로 MythicalCreature를 받는다:
#check Monster.mk
새 필드 각각의 값을 추출하는 함수를 정의하는 것 외에도, Monster → MythicalCreature 타입의 함수 Monster.toMythicalCreature가 정의된다.
이 함수를 사용하면 바탕이 되는 생물을 추출할 수 있다.
Lean에서 상속 계층을 위로 이동하는 것은 객체 지향 언어의 업캐스팅과 같지 않다.
업캐스트 연산자는 파생 클래스의 값을 부모 클래스의 인스턴스로 취급하게 하지만, 값은 자신의 정체성과 구조를 유지한다.
그러나 Lean에서 상속 계층을 위로 이동하면 실제로 바탕 정보가 지워진다.
이를 확인하려면 troll.toMythicalCreature를 평가한 결과를 살펴보자:
#eval troll.toMythicalCreature
MythicalCreature의 필드만 남는다.
where 구문과 마찬가지로 필드 이름을 사용하는 중괄호 표기도 구조체 상속에서 작동한다:
def troll : Monster := {large := true, vulnerability := "sunlight"}그러나 바탕 생성자에 위임하는 이름 없는 꺾쇠괄호 표기는 내부 세부 사항을 드러낸다:
def troll : Monster := ⟨true, "sunlight"⟩
꺾쇠괄호를 한 겹 더 써서 true에 MythicalCreature.mk를 호출해야 한다:
def troll : Monster := ⟨⟨true⟩, "sunlight"⟩
Lean의 점 표기는 상속을 고려할 수 있다.
즉 기존의 MythicalCreature.large를 Monster와 함께 사용할 수 있으며, Lean은 MythicalCreature.large를 호출하기 전에 Monster.toMythicalCreature 호출을 자동으로 삽입한다.
그러나 이는 점 표기를 사용할 때만 일어나며, 일반 함수 호출 구문으로 필드 조회 함수를 적용하면 타입 오류가 발생한다:
#eval MythicalCreature.large troll점 표기는 사용자가 정의한 함수에서도 상속을 고려할 수 있다. 작은 생물은 크지 않은 생물이다:
def MythicalCreature.small (c : MythicalCreature) : Bool := !c.large
troll.small을 평가하면 false가 나오지만, MythicalCreature.small troll을 평가하려 하면 다음 결과가 나온다:
5.1.1. Multiple Inheritance
도우미는 적절한 대가를 받으면 도움을 제공할 수 있는 신화 속 생물이다:
structure Helper extends MythicalCreature where
assistance : String
payment : String
deriving Repr예를 들어 니세(nisse)는 맛있는 죽을 받으면 집안일을 돕는 것으로 알려진 작은 요정이다:
def nisse : Helper where
large := false
assistance := "household tasks"
payment := "porridge"길들인 트롤은 훌륭한 도우미가 된다. 트롤은 하룻밤에 밭 전체를 갈 수 있을 만큼 강하지만, 삶에 만족하도록 모형 염소가 필요하다. 괴물 도우미는 괴물이면서 도우미이기도 한 생물이다:
structure MonstrousAssistant extends Monster, Helper where
deriving Repr이 구조체 타입의 값은 두 부모 구조체의 모든 필드를 채워야 한다:
def domesticatedTroll : MonstrousAssistant where
large := true
assistance := "heavy labor"
payment := "toy goats"
vulnerability := "sunlight"
두 부모 구조체 타입 모두 MythicalCreature를 상속한다.
다중 상속을 순진하게 구현하면 “다이아몬드 문제”가 생길 수 있다. 주어진 MonstrousAssistant에서 large로 가는 경로가 어느 것인지 분명하지 않기 때문이다.
포함된 Monster에서 large를 가져와야 할까, 아니면 포함된 Helper에서 가져와야 할까?
Lean에서는 조부모 구조체로 가는 경로 중 먼저 지정된 경로를 사용하며, 추가 부모 구조체의 필드는 새 구조체가 두 부모를 직접 포함하는 대신 복사한다.
이는 MonstrousAssistant 생성자의 시그니처를 살펴보면 확인할 수 있다:
#check MonstrousAssistant.mk
이 생성자는 인수로 Monster를 받고, Helper가 MythicalCreature 위에 추가하는 두 필드도 받는다.
마찬가지로 MonstrousAssistant.toMonster는 생성자에서 Monster를 추출할 뿐이지만, MonstrousAssistant.toHelper가 추출할 Helper는 없다.
#print 명령으로 그 구현을 확인할 수 있다:
#print MonstrousAssistant.toHelper
이 함수는 MonstrousAssistant의 필드로 Helper를 구성한다.
@[reducible] 속성은 abbrev라고 쓰는 것과 같은 효과를 낸다.
5.1.1.1. Default Declarations
한 구조체가 다른 구조체를 상속할 때 기본 필드 정의를 사용하면 자식 구조체의 필드에 따라 부모 구조체의 필드를 인스턴스화할 수 있다.
생물이 큰지 아닌지보다 더 구체적인 크기 정보가 필요하다면, 크기를 설명하는 전용 데이터 타입을 상속과 함께 사용할 수 있다. 그러면 large 필드가 size 필드의 내용으로부터 계산되는 구조체가 만들어진다:
inductive Size where
| small
| medium
| large
deriving BEq
structure SizedCreature extends MythicalCreature where
size : Size
large := size == Size.large
그러나 이 정의는 어디까지나 기본 정의일 뿐이다.
C#이나 Scala 같은 언어의 속성 상속과 달리 자식 구조체의 정의는 large에 특정 값이 제공되지 않을 때만 사용되므로, 말이 되지 않는 결과가 생길 수 있다:
def nonsenseCreature : SizedCreature where
large := false
size := .large자식 구조체가 부모 구조체에서 벗어나지 않아야 한다면 몇 가지 선택지가 있다:
-
필드가 적절한 관계를 가진다는 명제를 정의하고, 필요한 곳에서 그 명제가 참이라는 증거를 요구하도록 API를 설계하라.
-
상속을 전혀 사용하지 말라.
두 번째 선택지는 다음과 같을 수 있다:
abbrev SizesMatch (sc : SizedCreature) : Prop :=
sc.large = (sc.size == Size.large)
등호 하나는 동등성 명제를 나타내고, 등호 두 개는 동등성을 검사해 Bool을 반환하는 함수를 나타낸다는 점에 유의하라.
SizesMatch는 abbrev로 정의된다. 증명에서 자동으로 전개되어 decide가 증명해야 할 동등성을 볼 수 있어야 하기 때문이다.
훌드레(huldre)는 중간 크기의 신화 속 생물이며, 실제로 인간과 크기가 같다.
huldre의 두 크기 관련 필드는 서로 일치한다:
def huldre : SizedCreature where
size := .medium
example : SizesMatch huldre := ⊢ SizesMatch huldre
All goals completed! 🐙5.1.1.2. Type Class Inheritance
내부적으로 타입 클래스는 구조체다. 새 타입 클래스를 정의하면 새 구조체가 정의되고, 인스턴스를 정의하면 그 구조체 타입의 값이 만들어진다. 그런 다음 이 값들은 Lean의 내부 테이블에 추가되어, 요청이 들어올 때 Lean이 인스턴스를 찾을 수 있게 된다. 따라서 타입 클래스는 다른 타입 클래스를 상속할 수 있다.
정확히 같은 언어 기능을 사용하므로 타입 클래스 상속은 다중 상속, 부모 타입 메서드의 기본 구현, 다이아몬드의 자동 병합을 비롯한 구조체 상속의 모든 기능을 지원한다. 이는 Java, C#, Kotlin 같은 언어에서 다중 인터페이스 상속이 유용한 여러 상황에서 마찬가지로 유용하다. 타입 클래스 상속 계층을 신중하게 설계하면 프로그래머는 두 장점을 모두 얻을 수 있다. 즉 독립적으로 구현할 수 있는 세분화된 추상화 모음과, 더 크고 일반적인 추상화에서 이러한 구체적 추상화를 자동으로 구성하는 기능이다.