3.3. 인스턴스 검색 제어하기
Add 클래스의 인스턴스가 있으면 Pos 타입의 두 표현식을 편리하게 더해 또 다른 Pos를 얻을 수 있습니다. 하지만 많은 경우에는 더 유연하게 인자의 타입이 서로 다를 수 있는 이종(heterogeneous) 연산자 오버로딩을 허용하는 것이 유용합니다. 예를 들어 Pos에 Nat을 더하거나 Nat에 Pos를 더하면 항상 Pos가 나옵니다.
def addNatPos : Nat → Pos → Pos
| 0, p => p
| n + 1, p => Pos.succ (addNatPos n p)
def addPosNat : Pos → Nat → Pos
| p, 0 => p
| p, n + 1 => Pos.succ (addPosNat p n)
이 함수들을 사용하면 자연수를 양수에 더할 수 있지만, add의 두 인자가 같은 타입이기를 기대하는 Add 타입 클래스와 함께 사용할 수는 없습니다.
3.3.1. 이종 오버로딩
덧셈 오버로딩 절에서 언급했듯이, Lean은 서로 다른 타입 간의 덧셈을 오버로딩할 수 있도록 HAdd라는 타입 클래스를 제공합니다. HAdd 클래스는 두 인자의 타입과 반환 타입, 이렇게 세 개의 타입 매개변수를 받습니다. HAdd Nat Pos Pos와 HAdd Pos Nat Pos의 인스턴스가 있으면 일반적인 덧셈 표기법으로 두 타입을 섞어 쓸 수 있습니다:
instance : HAdd Nat Pos Pos where
hAdd := addNatPos
instance : HAdd Pos Nat Pos where
hAdd := addPosNat위의 두 인스턴스가 주어지면 다음 예제들이 동작합니다:
#eval (3 : Pos) + (5 : Nat)#eval (3 : Nat) + (5 : Pos)
HAdd 타입 클래스의 정의는 다음에 나오는 HPlus의 정의 및 해당 인스턴스들과 매우 비슷합니다.
class HPlus (α : Type) (β : Type) (γ : Type) where
hPlus : α → β → γinstance : HPlus Nat Pos Pos where
hPlus := addNatPos
instance : HPlus Pos Nat Pos where
hPlus := addPosNat
하지만 HPlus의 인스턴스는 HAdd의 인스턴스보다 훨씬 덜 유용합니다. #eval과 함께 이 인스턴스를 사용하려고 하면 오류가 발생합니다:
#eval toString (HPlus.hPlus (3 : Pos) (5 : Nat))이 메시지는 타입에 메타변수가 있고 Lean이 이를 풀 방법이 없기 때문에 이런 일이 발생한다는 것을 알려 줍니다.
다형성에 대한 첫 설명에서 다루었듯이, 메타변수는 프로그램에서 추론할 수 없었던 알 수 없는 부분을 나타냅니다. 표현식을 #eval 뒤에 작성하면 Lean은 그 타입을 자동으로 결정하려고 시도합니다. 이 경우에는 그렇게 할 수 없었습니다. HPlus의 세 번째 타입 매개변수를 알 수 없었기 때문에 Lean은 타입 클래스 인스턴스 검색을 수행할 수 없었습니다. 그런데 Lean이 표현식의 타입을 결정할 수 있는 방법은 인스턴스 검색뿐입니다. 즉, HPlus Pos Nat Pos 인스턴스는 표현식의 타입이 Pos여야 하는 경우에만 적용될 수 있습니다. 하지만 프로그램에는 인스턴스 자체 외에 표현식이 이 타입을 가져야 한다는 것을 알려 주는 것이 아무것도 없습니다.
이 문제를 해결하는 한 가지 방법은 전체 표현식에 타입 표기를 추가하여 세 타입을 모두 사용할 수 있도록 하는 것입니다:
#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos)하지만 이 해결책은 양수 라이브러리 사용자에게 그다지 편리하지 않습니다.
3.3.2. 출력 매개변수
이 문제는 γ를 출력 매개변수로 선언하여 해결할 수도 있습니다. 대부분의 타입 클래스 매개변수는 검색 알고리즘의 입력이며, 인스턴스를 선택하는 데 사용됩니다. 예를 들어, OfNat 인스턴스에서는 타입과 자연수가 모두 자연수 리터럴의 특정 해석을 선택하는 데 사용됩니다. 그러나 경우에 따라서는 일부 타입 매개변수를 아직 모르는 상태에서도 검색 과정을 시작하고, 검색 중에 발견된 인스턴스를 사용하여 메타변수의 값을 결정하는 것이 편리할 수 있습니다. 인스턴스 검색을 시작하는 데 필요하지 않은 매개변수는 이 과정의 출력이며, 이는 outParam 수식어로 선언합니다:
class HPlus (α : Type) (β : Type) (γ : outParam Type) where
hPlus : α → β → γ
이 출력 매개변수 덕분에 타입 클래스 인스턴스 검색은 γ를 미리 알지 못해도 인스턴스를 선택할 수 있습니다. 예를 들면 다음과 같습니다.
#eval HPlus.hPlus (3 : Pos) (5 : Nat)출력 매개변수가 일종의 함수를 정의한다고 생각하면 도움이 될 수 있습니다. 하나 이상의 출력 매개변수를 가진 타입 클래스의 인스턴스는 입력으로부터 출력을 결정하는 방법을 Lean에 알려 줍니다. 인스턴스를 검색하는 과정은 재귀적으로 이루어질 수도 있으므로, 단순한 오버로딩보다 더 강력합니다. 출력 매개변수는 프로그램의 다른 타입을 결정할 수 있으며, 인스턴스 검색은 여러 기반 인스턴스를 조합하여 그 타입을 가진 프로그램을 만들어 낼 수 있습니다.
3.3.3. 기본 인스턴스
매개변수를 입력으로 둘지 출력으로 둘지에 따라 Lean이 타입 클래스 탐색을 시작하는 상황이 결정됩니다. 특히 타입 클래스 탐색은 모든 입력이 알려지기 전에는 일어나지 않습니다. 하지만 경우에 따라서는 출력 매개변수만으로는 충분하지 않으며, 일부 입력을 알지 못할 때에도 인스턴스 검색이 이루어져야 합니다. 이는 Python이나 Kotlin에서 선택적 함수 인자의 기본값과 비슷하지만, 여기서는 기본 타입이 선택된다는 점이 다릅니다.
기본 인스턴스는 모든 입력이 알려지지 않은 경우에도 인스턴스 검색에 사용할 수 있는 인스턴스입니다. 이러한 인스턴스 중 하나를 사용할 수 있으면 그 인스턴스가 사용됩니다. 이 덕분에 알 수 없는 타입이나 메타변수와 관련된 오류로 실패하지 않고 프로그램이 타입 검사를 통과할 수 있습니다. 반면에 기본 인스턴스는 인스턴스 선택을 예측하기 어렵게 만들 수 있습니다. 특히 원하지 않는 기본 인스턴스가 선택되면 표현식이 예상과 다른 타입을 가질 수 있으며, 이로 인해 프로그램의 다른 곳에서 혼란스러운 타입 오류가 발생할 수 있습니다. 기본 인스턴스를 사용할 곳은 신중하게 고르십시오!
기본 인스턴스가 유용할 수 있는 한 가지 예로, Add 인스턴스로부터 유도할 수 있는 HPlus 인스턴스가 있습니다. 다시 말해, 일반적인 덧셈은 세 타입이 모두 우연히 같은 경우에 해당하는 이종 덧셈의 특수한 경우입니다. 이는 다음 인스턴스를 사용하여 구현할 수 있습니다:
instance [Add α] : HPlus α α α where
hPlus := Add.add
이 인스턴스가 있으면 hPlus를 Nat처럼 덧셈이 가능한 모든 타입에 사용할 수 있습니다:
#eval HPlus.hPlus (3 : Nat) (5 : Nat)그러나 이 인스턴스는 두 인자의 타입이 모두 알려진 상황에서만 사용됩니다. 예를 들어,
#check HPlus.hPlus (5 : Nat) (3 : Nat)다음 타입을 산출합니다.
예상대로 동작하지만
#check HPlus.hPlus (5 : Nat)남은 인자에 대한 메타변수 하나와 반환 타입에 대한 메타변수 하나, 이렇게 두 개의 메타변수를 포함하는 타입이 만들어집니다.
대부분의 경우, 덧셈에 인자 하나를 제공하면 다른 인자도 같은 타입을 갖습니다. 이 인스턴스를 기본 인스턴스로 만들려면 default_instance 속성을 적용하십시오:
@[default_instance]
instance [Add α] : HPlus α α α where
hPlus := Add.add이 기본 인스턴스를 사용하면 예제의 타입이 더 유용해집니다:
#check HPlus.hPlus (5 : Nat)결과는 다음과 같습니다
오버로드 가능한 이종(heterogeneous) 버전과 동종(homogeneous) 버전이 모두 존재하는 각 연산자는, 이종 버전이 필요한 맥락에서 동종 버전을 사용할 수 있게 해 주는 기본 인스턴스 패턴을 따릅니다. 중위 연산자는 이종 버전 호출로 바뀌며, 가능하면 동종 기본 인스턴스가 선택됩니다.
마찬가지로, 단순히 5라고 쓰면 OfNat 인스턴스를 선택하기 위해 더 많은 정보를 기다리는 메타변수를 가진 타입이 아니라 Nat이 됩니다. 이는 Nat에 대한 OfNat 인스턴스가 기본 인스턴스이기 때문입니다.
기본 인스턴스에는 우선순위를 지정할 수도 있으며, 이는 둘 이상의 인스턴스가 적용될 수 있는 상황에서 어느 것이 선택될지에 영향을 줍니다. 기본 인스턴스 우선순위에 대한 자세한 내용은 Lean 매뉴얼을 참고하십시오.
3.3.4. 연습 문제
두 프로젝션에 모두 스칼라를 곱하는 HMul (PPoint α) α (PPoint α)의 인스턴스를 정의하십시오. 이 인스턴스는 Mul α 인스턴스가 존재하는 모든 타입 α에 대해 동작해야 합니다. 예를 들어,
#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0다음과 같은 결과를 내야 합니다