5.1. 구조체와 상속
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. 다중 상속
헬퍼는 알맞은 대가를 받으면 도움을 줄 수 있는 신화 속 존재입니다:
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. 기본 선언
한 구조체가 다른 구조체를 상속할 때, 기본 필드 정의를 사용하면 자식 구조체의 필드를 바탕으로 부모 구조체의 필드를 인스턴스화할 수 있습니다. 생물이 큰지 아닌지보다 크기를 더 세밀하게 구분해야 한다면, 크기를 나타내는 전용 데이터 타입을 상속과 함께 사용할 수 있으며, 그러면 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. 타입 클래스 상속
내부적으로 타입 클래스는 구조체입니다. 새 타입 클래스를 정의하면 새 구조체가 정의되고, 인스턴스를 정의하면 그 구조체 타입의 값이 만들어집니다. 그런 다음 이 값들은 Lean 내부 테이블에 추가되며, Lean은 이 테이블을 이용해 요청이 있을 때 인스턴스를 찾을 수 있습니다. 그 결과 타입 클래스는 다른 타입 클래스를 상속할 수 있습니다.
타입 클래스 상속은 구조체 상속과 정확히 동일한 언어 기능을 사용하기 때문에 다중 상속, 부모 타입 메서드의 기본 구현, 다이아몬드의 자동 병합을 포함한 구조체 상속의 모든 기능을 지원합니다. 이는 Java, C#, Kotlin 같은 언어에서 다중 인터페이스 상속이 유용한 상황과 상당 부분 같은 상황에서 유용합니다. 타입 클래스 상속 계층을 신중하게 설계하면 프로그래머는 두 가지 장점을 모두 얻을 수 있습니다. 하나는 각각 독립적으로 구현할 수 있는 세분화된 추상화의 모음이고, 다른 하나는 더 크고 일반적인 추상화로부터 이러한 구체적인 추상화를 자동으로 구성하는 것입니다.