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.toMythicalCreature 함수가 Monster → MythicalCreature 타입으로 정의됩니다. 이를 사용하여 내부의 creature를 추출할 수 있습니다.
Lean에서 상속 계층 구조를 위로 이동하는 것은 객체 지향 언어에서의 업캐스팅과 같은 것이 아닙니다. 업캐스트 연산자는 파생 클래스의 값을 부모 클래스의 인스턴스로 취급되게 하지만, 그 값은 자신의 정체성과 구조를 그대로 유지합니다. 하지만 Lean에서는 상속 계층을 위로 이동하면 실제로 기저 정보가 지워집니다. 이것이 실제로 작동하는 모습을 보려면, troll.toMythicalCreature를 평가한 결과를 살펴보십시오:
#eval troll.toMythicalCreature
MythicalCreature의 필드만 남습니다.
where 구문과 마찬가지로, 필드 이름을 사용한 중괄호 표기법도 구조체 상속과 함께 작동합니다:
def troll : Monster := {large := true, vulnerability := "sunlight"}하지만 내부의 생성자에 위임하는 익명 꺾쇠괄호(anonymous angle-bracket) 표기법은 내부 세부 사항을 드러냅니다:
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 내부 테이블에 추가됩니다. 이로 인해 타입 클래스는 다른 타입 클래스로부터 상속받을 수 있습니다.
정확히 동일한 언어 기능을 사용하기 때문에, 타입 클래스 상속은 다중 상속, 부모 타입 메서드의 기본 구현, 다이아몬드의 자동 병합을 포함하여 구조체 상속의 모든 기능을 지원합니다. 이는 Java, C#, Kotlin과 같은 언어에서 다중 인터페이스 상속이 유용한 것과 많은 부분에서 동일한 상황에 유용합니다. 타입 클래스 상속 계층을 신중하게 설계함으로써, 프로그래머는 두 가지 장점을 모두 얻을 수 있습니다: 독립적으로 구현 가능한 세밀한 추상화의 모음과, 이러한 특정 추상화를 더 크고 일반적인 추상화로부터 자동으로 구성하는 것입니다.