3.3. Controlling Instance Search
Add 클래스의 인스턴스만으로도 Pos 타입의 두 표현식을 편리하게 더해 또 다른 Pos를 만들 수 있다.
그러나 많은 경우 더 유연하게 인수 타입이 달라도 되는 이종 연산자 오버로딩을 허용하면 유용하다.
예를 들어 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. Heterogeneous Overloadings
오버로딩된 덧셈 절에서 설명했듯이 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은 타입 클래스 인스턴스 검색을 수행할 수 없었고, 인스턴스 검색만이 표현식의 타입을 결정할 방법이었다.
즉 HPlus Pos Nat Pos 인스턴스는 표현식의 타입이 Pos여야 적용되지만, 프로그램에는 인스턴스 자체 외에 그렇게 표시할 것이 없다.
한 가지 해결책은 전체 표현식에 타입 주석을 붙여 세 타입을 모두 알 수 있게 하는 것이다.
#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos)그러나 이 해결책은 양수 라이브러리 사용자에게 그리 편리하지 않다.
3.3.2. Output Parameters
이 문제는 γ를 출력 매개변수로 선언해 해결할 수도 있다.
대부분의 타입 클래스 매개변수는 검색 알고리즘의 입력이며 인스턴스를 선택하는 데 사용된다.
예를 들어 OfNat 인스턴스에서는 타입과 자연수를 모두 사용해 자연수 리터럴의 특정 해석을 선택한다.
그러나 어떤 경우에는 일부 타입 매개변수를 아직 몰라도 검색을 시작하고, 검색으로 발견한 인스턴스를 사용해 메타변수의 값을 정하는 것이 편리하다.
인스턴스 검색을 시작하는 데 필요하지 않은 매개변수는 과정의 출력이며 outParam 수정자로 선언한다.
class HPlus (α : Type) (β : Type) (γ : outParam Type) where
hPlus : α → β → γ
이 출력 매개변수가 있으면 타입 클래스 인스턴스 검색은 γ를 미리 몰라도 인스턴스를 선택할 수 있다.
예를 들어 다음과 같다.
#eval HPlus.hPlus (3 : Pos) (5 : Nat)출력 매개변수를 일종의 함수를 정의한다고 생각하면 도움이 된다. 출력 매개변수가 하나 이상인 타입 클래스의 각 인스턴스는 입력으로부터 출력을 결정하는 방법을 Lean에 제공한다. 인스턴스를 재귀적으로 검색하는 과정은 단순한 오버로딩보다 강력하다. 출력 매개변수는 프로그램의 다른 타입을 결정할 수 있고, 인스턴스 검색은 내부 인스턴스들을 모아 이 타입의 프로그램을 구성할 수 있다.
3.3.3. Default Instances
매개변수가 입력인지 출력인지 정하면 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)결과는 다음과 같다.
이종 및 동종 버전으로 오버로딩할 수 있는 각 연산자는 이종 버전이 필요한 문맥에서 동종 버전을 사용할 수 있게 하는 기본 인스턴스 패턴을 따른다. 중위 연산자는 이종 버전 호출로 바뀌고, 가능하면 동종 기본 인스턴스가 선택된다.
마찬가지로 5만 쓰면 OfNat 인스턴스를 고를 정보를 기다리는 메타변수 타입이 아니라 Nat이 된다.
이는 Nat에 대한 OfNat 인스턴스가 기본 인스턴스이기 때문이다.
기본 인스턴스에는 둘 이상 적용될 때 어떤 것을 고를지 정하는 우선순위도 지정할 수 있다. 기본 인스턴스 우선순위에 관한 자세한 내용은 Lean 매뉴얼을 참고하라.
3.3.4. Exercises
두 프로젝션에 스칼라를 곱하는 HMul (PPoint α) α (PPoint α) 인스턴스를 정의하라.
Mul α 인스턴스가 있는 모든 타입 α에서 동작해야 한다.
예를 들어 다음은
#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0다음을 출력해야 한다.