3.3. 인스턴스 탐색 제어하기
Add 클래스의 인스턴스만 있으면 Pos 타입을 가진 두 식을 편리하게 더해 또 다른 Pos를 만들어낼 수 있습니다. 하지만 많은 경우, 좀 더 유연하게 인자가 서로 다른 타입을 가질 수 있는 heterogeneous(이종) 연산자 오버로딩을 허용하는 것이 유용할 수 있습니다. 예를 들어, Nat를 Pos에 더하거나 Pos를 Nat에 더하면 항상 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) 버전으로 존재하는 각 연산자는, 이형 버전이 요구되는 컨텍스트에서 동형 버전을 사용할 수 있도록 하는 기본 인스턴스 패턴을 따릅니다. 중위 연산자는 이형(heterogeneous) 버전에 대한 호출로 대체되며, 가능한 경우 동형(homogeneous) 기본 인스턴스가 선택됩니다.
마찬가지로, 5를 그냥 쓰면 OfNat 인스턴스를 선택하기 위해 더 많은 정보를 기다리는 메타변수가 있는 타입이 아니라 Nat를 줍니다. 이는 Nat에 대한 OfNat 인스턴스가 기본 인스턴스이기 때문입니다.
기본 인스턴스에는 여러 인스턴스가 적용될 수 있는 상황에서 어떤 것이 선택될지에 영향을 미치는 priority를 지정할 수도 있습니다. 기본 인스턴스 우선순위에 대한 자세한 내용은 Lean 매뉴얼을 참고하십시오.
3.3.4. 연습문제
HMul (PPoint α) α (PPoint α)의 인스턴스를 정의하되, 두 투영값을 모두 스칼라로 곱하도록 하십시오. Mul α 인스턴스가 있는 임의의 타입 α에 대해 작동해야 합니다. 예를 들어,
#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0다음과 같은 결과를 산출해야 합니다