하위 타입과 공변·반변(Subtyping and variance)

고양이는 동물입니다. 그래서 동물을 받는 함수 '이름 부르기'에 고양이를 넘겨도 됩니다. 타입으로 적으면 $\text{고양이} \le \text{동물}$이고, 규칙은 한 줄입니다. $a : A$이고 $A \le B$이면 $a : B$. 이 규칙을 포섭⁠(subsumption)⁠이라 합니다. A가 B의 하위 타입이라는 말은 B가 필요한 모든 자리에 A를 넣어도 프로그램이 잘못되지 않는다는 약속입니다. 미국 컴퓨터 과학자 바버라 리스코프는 1987년 강연에서 이 원칙을 내세웠고, 1994년 저넷 윙과 함께 '상위 타입⁠(supertype)⁠의 객체에 대해 증명할 수 있는 성질은 하위 타입의 객체에서도 성립해야 한다'로 정식화했습니다. 리스코프 치환 원칙⁠(Liskov substitution principle)⁠이라 부릅니다.

그렇다면 고양이의 목록은 동물의 목록일까요? 목록을 읽기만 한다면 그렇습니다. 동물을 기대하고 꺼낸 것이 고양이여도 아무 문제가 없습니다. 목록에 무엇을 넣을 수 있다면 사정이 다릅니다. 자바에서 Cat[] cats를 만들고 Animal[] animals = cats;로 같은 배열을 동물의 배열이라고 부른 뒤 animals[0] = new Dog();를 쓰면, 컴파일러⁠(compiler)⁠는 세 줄을 모두 통과시킵니다. 자바는 고양이 ≤ 동물이면 Cat[] ≤ Animal[]이라는 규칙을 두기 때문입니다. 그대로 두면 고양이 배열에 개가 들어가고, 나중에 cats[0]을 고양이로 꺼내 쓰는 순간 무너집니다. 그래서 자바는 셋째 줄을 실행할 때 검사해 ArrayStoreException을 던집니다. 타입 검사를 통과한 프로그램이 실행 중에 타입 오류로 멈추니, 정적 타입 검사만 놓고 보면 이 규칙은 건전하지 않습니다. 자바는 그 구멍을 실행 중 검사로 메우는 것입니다. 타입스크립트의 배열도 같은 규칙을 쓰는데, 실행 중 검사가 없습니다. 그래서 개를 고양이로 꺼내 고양이에게만 있는 기능을 쓰는 곳에 가서야 오류가 나거나, 오류 없이 틀린 결과가 나옵니다. 편의를 위해 설계자들이 알고 받아들인 구멍입니다.

함수 타입의 규칙이 이 모든 것의 열쇠입니다. 어떤 동물이든 진찰하는 수의사 $v : \text{동물} \to \text{기록}$는 고양이만 진찰할 수의사가 필요한 자리에 써도 됩니다. 고양이도 진찰할 수 있으니까요. 반대로 고양이 전문 수의사를 동물 수의사 자리에 두면, 개가 왔을 때 '야옹 소리를 들어 본다'는 진찰 절차가 실패합니다. 그러니 $\text{동물} \to \text{기록} \;\le\; \text{고양이} \to \text{기록}$이고, 인자 쪽에서는 방향이 뒤집힙니다. 돌려주는 값은 방향을 따릅니다. 고양이를 돌려주는 함수는 동물을 돌려주는 함수 자리에 써도 됩니다. 둘을 합친 것이 다음 규칙입니다.

$$\dfrac{A' \le A \qquad B \le B'}{A \to B \;\le\; A' \to B'}$$

'누가 무엇을 공급하는가'로 기억하면 틀리지 않습니다. 인자는 함수를 쓰는 쪽이 공급하므로, 함수는 약속보다 더 넓은 것을 받아들일 수 있어야 합니다. 결과는 함수가 공급하므로, 약속보다 더 좁은(더 구체적인) 것을 돌려줘도 됩니다. 흔한 실수는 인자도 공변이라고 생각하는 것입니다. 에펠(Eiffel) 언어는 메서드를 물려받아 고칠 때 인자 타입을 더 구체적으로 바꾸는 것을 허락했는데, 1989년 윌리엄 쿡이 이것이 실행 중 타입 오류를 낳는 구멍임을 지적했습니다.

타입 생성자 F(목록, 배열, 함수 등)가 하위 타입 관계를 어떻게 옮기는지를 그 생성자의 변성⁠(variance)⁠이라 합니다. $A \le B$일 때 늘 $F(A) \le F(B)$이면 공변, 늘 $F(B) \le F(A)$이면 반변, 같을 때 말고는 어느 쪽도 성립하지 않으면 무변입니다. 생성자 F = 에서, X = , Y = 로 두고 F(X)를 F(Y)가 필요한 자리에 써도 되는지 연산마다 따져 보세요.

표를 보면 변성이 연산에서 나온다는 것이 드러납니다. 값을 꺼내 주는 연산(get, 함수의 결과)은 $X \le Y$를 요구하고, 값을 받아들이는 연산(set, 함수의 인자)은 $Y \le X$를 요구합니다. 가변 배열에는 둘 다 있으니 X = Y일 때만 통과하고, 그래서 Array<Cat>과 Array<Animal>은 어느 방향으로도 하위 타입이 아닙니다. 연속 $(T \to \text{기록}) \to \text{기록}$처럼 화살표 왼쪽의 왼쪽에 있는 자리는 두 번 뒤집혀 다시 공변이 됩니다. 일반 규칙은 부호 셈입니다. 화살표의 왼쪽으로 들어갈 때마다 부호가 바뀌고, T가 양의 자리에만 나오면 공변, 음의 자리에만 나오면 반변, 두 자리에 다 나오면 무변입니다. 어디에도 나오지 않으면 두 방향이 다 되는 쌍변입니다. 곱 $A \times B$와 합 $A + B$는 두 자리 모두에서 공변이니, 대수적 자료형⁠(algebraic data type)⁠으로 지은 읽기 전용 자료는 대개 공변입니다.

언어들은 이것을 표시로 받아들였습니다. C#은 2010년 4.0판부터 제네릭 인터페이스의 타입 매개변수⁠(parameter)⁠에 out(꺼내기만 함, 공변)과 in(받기만 함, 반변)을 붙이게 하고, 표시와 맞지 않게 쓰면 컴파일을 거절합니다. 스칼라의 +T와 -T, 코틀린의 out과 in도 같습니다. 자바의 제네릭은 쓰는 곳에서 List<? extends Animal>(꺼내기용: null 말고는 넣을 수 없음)과 List<? super Cat>(넣기용: 꺼낸 값은 Object로만 보임)으로 적게 합니다. 타입스크립트는 2017년 2.6판부터 strictFunctionTypes 설정에서 함수 타입의 인자를 반변으로 검사하지만, 메서드의 인자는 여전히 두 방향을 모두 허락합니다.

범주론⁠(category theory)⁠으로 보면 이 모든 것이 한 문장으로 줄어듭니다. 하위 타입 관계는 순서이고, 순서는 두 대상 사이에 화살표가 많아야 하나인 범주입니다. 공변 생성자는 이 범주⁠(category)⁠에서 자기 자신으로 가는 함자⁠(functor)⁠, 곧 순서를 지키는 사상이고, 반변 생성자는 화살표를 뒤집는 반변 함자입니다. $T \mapsto (T \to R)$가 반변인 것은 집합⁠(set)⁠과 함수의 범주에서 $\mathrm{Hom}(-, R)$이 반변 함자⁠(contravariant functor)⁠라는 사실, 곧 $f : A \to B$가 앞에 합성하는 사상 $(B \to R) \to (A \to R)$을 준다는 사실의 그림자입니다. 두 자리를 함께 보면 →는 첫 자리에서 반변, 둘째 자리에서 공변인 두 변수 함자 $\mathrm{Hom}(-, -)$이고, 요네다 보조정리⁠(Yoneda lemma)⁠가 다루는 것이 바로 이 Hom 함자입니다. 하위 타입 $A \le B$를 A를 B로 바꾸는 보이지 않는 변환 $c : A \to B$로 읽으면(정수⁠(integer)⁠를 실수⁠(real number)⁠로 바꾸는 변환처럼), 목록의 공변성은 $\mathrm{map}\;c : \mathrm{List}\,A \to \mathrm{List}\,B$이고 함수의 반변성은 인자 쪽에 c를 먼저 합성하는 것입니다.

하위 타입을 이름으로 정하는 언어와 모양으로 정하는 언어가 있습니다. 자바와 C#에서는 선언할 때 '고양이는 동물을 물려받는다'고 적어야 하위 타입이 됩니다(이름 기반). 타입스크립트에서는 필드를 더 많이 가진 레코드가 그대로 하위 타입입니다. {이름, 나이}를 가진 값은 {이름}만 요구하는 자리에 쓸 수 있습니다(구조적, 너비 하위 타입). 필드의 타입을 더 구체적으로 바꾸는 깊이 하위 타입은 필드를 읽기만 할 때만 안전합니다. 이유는 배열과 같습니다. 또 코드를 물려받는 상속과 대신 써도 된다는 하위 타입은 다른 개념입니다. 물려받은 메서드의 인자를 좁히면 상속은 되어도 하위 타입은 깨집니다.

하위 타입은 다형성⁠(polymorphism)⁠과 만나면 어려워집니다. '동물의 하위 타입인 모든 X에 대해'라는 뜻의 $\forall X \le \text{동물}.\; X \to X$처럼 타입 변수에 상한⁠(upper bound)⁠을 두는 한정 양화(루카 카델리·피터 웨그너, 1985)는 자연스러운 확장이지만, 이것을 시스템 F⁠(System F)⁠에 넣은 F_<:에서는, 두 한정 양화⁠(bounded quantification)⁠ 타입을 비교하는 규칙을 가장 너그럽게 둔 판의 경우 한 타입이 다른 타입의 하위 타입인지 판정하는 문제조차 결정할 수 없습니다(벤저민 피어스, 1992). 비교 규칙을 좁힌 '커널' 판은 결정 가능⁠(decidable)⁠합니다. 힌들리–밀너 타입 추론⁠(type inference)⁠과도 잘 섞이지 않습니다. 같음의 방정식을 푸는 대신 부등식 $X \le Y$를 풀어야 하고, 가장 일반적인 타입이 깔끔한 모양으로 나오지 않기 때문입니다. 2017년 스티븐 돌런과 앨런 마이크로프트의 MLsub처럼 둘을 함께 다루는 방법도 나왔지만, 많은 함수형 언어⁠(functional programming language)⁠가 하위 타입을 최소한으로만 두는 까닭이 여기에 있습니다.

흔한 오해 하나. 타입을 지금 담긴 값들의 집합으로만 읽으면, 고양이만 든 배열도 동물이 든 배열이니 배열⟨고양이⟩ ≤ 배열⟨동물⟩처럼 보입니다. 그러나 배열⟨동물⟩이라는 타입은 '동물을 꺼낼 수 있다'뿐 아니라 '아무 동물이나 넣을 수 있다'도 약속합니다. 하위 타입은 담긴 값이 아니라 모든 연산에서 '대신 써도 되는가'라는 행동의 약속이고, 리스코프가 행동을 앞세워 정식화한 까닭이 이것입니다. 리스코프와 윙의 조건을 메서드의 명세로 적으면, 하위 타입의 메서드는 전조건⁠(precondition)⁠을 약하게(더 많은 입력을 받게) 하고 후조건⁠(postcondition)⁠을 강하게(더 좁은 결과를 약속하게) 해도 됩니다. 함수 규칙의 반변·공변과 똑같은 모양이며, 호어 논리⁠(Hoare logic)⁠의 결과 규칙이 바로 이 모양입니다.

이어지는 곳. 공변과 반변은 함자 페이지의 공변 함자와 반변 함자를 순서라는 가장 작은 범주에서 본 것이고, 함수 타입의 두 자리는 요네다 보조정리의 Hom 함자로 이어집니다. 하위 타입 규칙이 건전한지는 타입 이론⁠(type theory)⁠의 안전성 정리(진행과 보존)로 따지며, 자바 배열은 실행 중 검사 없이는 그 정리가 깨지는 곳입니다. 곱과 합이 왜 공변인지는 대수적 자료형에서, 타입 변수에 상한을 두는 일은 다형성과 시스템 F에서, 부등식을 푸는 추론의 어려움은 타입 추론에서 이어집니다. 전조건은 반변, 후조건은 공변이라는 명세의 규칙은 호어 논리에서 증명의 규칙으로 다시 나오고, 명제들 사이의 '약하다·강하다'라는 순서는 불 대수⁠(Boolean algebra)⁠의 함의 순서입니다.