OKR 3 - 타입 이론에 지치다

[<< | 이전 | 색인 | 다음 | >>]

2014년 3월 30일 일요일

OKR 3 - 타입 이론에 지치다

이 연재의 이전 글:

• 지식 표현에 관하여

• OKR 2 - 직관적 추론의 예

"타입"이란 무엇일까? 정수와 문자열의 차이는 무엇일까? 길이가 서로 다른 두 목록이 있다면, 이들은 같은 타입일까? 정수가 실수와 구별되는 타입이라면 소수도 구별되는 타입일까? 타입과 클래스는 어떻게 연결되는가? 소수는 정수의 하위 클래스인가(그리고 정수는 실수의 하위 클래스인가)? 타입 시스템, 타입 이론, 타입 추론은 모두 무엇에 관한 것인가?

기존의 타입 이론을 보면, 타입이라는 개념에는 아주 근본적인 무언가가 있으며 우리가 백 년이 넘도록 이토록 깊이 그것을 골몰해 온 데에는 타당한 이유가 있다고 결론내릴지도 모른다. 그 결과물은 이런 것이다:

알고 보니, 아니다.

이유는 있다. 하지만 딱히 좋은 이유는 아니다. 타입 이론은 원자적이고 플라톤적인 값 패러다임(및 그에 연관된 계산 모형)의 과도한 환원주의에서 회복하려는 시도다. 양손을 등 뒤로 묶고 저글링을 연구하는 것과 비슷하다.

자유로운 손으로 무엇을 할 수 있는지 보자.

OKR의 핵심 아이디어를 기억한다면, 변수에 담긴 (대개 플라톤적이고 원자적인) 값의 관점으로 생각하는 대신 변수 위와 변수 사이의 술어 관계라는 관점으로 생각할 수 있다. 다시 말해, 변수는 무언가를 담는 양동이가 아니라 우리가 무언가를 알고 있는 고유 식별자일 뿐이다. 단순한 값 할당의 경우 $X=7$은 $7(X)$이 되므로, 그 능력을 잃지는 않는다. 그러나 같은 방식으로 $Prime(X)$, $GreaterThan(X, Y)$ 등도 말할 수 있다.

실질적으로, 가능한 모든 것의 무한하고 연속적인 공간에서 $X$에 관한 새로운 관계가 하나 생길 때마다 $X$가 있을 수 있는 위치나 대상의 영역을 깎아 낸다. 그 영역이 (어떤 타입이 암묵적으로 정의한) 하나의 "값" 분할 안에 완전히 들어가면, 우리는 $X$의 값을 안다고 말한다(그 타입에 관하여). 예를 들어 $GreaterThan(X, 5)$, $LessThan(X, 11)$, $Prime(X)$를 안다면 $7(X)$, 즉 $X=7$을 추론할 수 있다. 이 값 분할은 특별한 구성물이 아니라 상호 관계들 사이의 논리(표)가 단지 함의하는 것이다. 예를 들어 $7(X)$, $3(Y)$, $Sum(X, Y, Z)$는 $10(Z)$를 함의한다. 즉, $X$와 $Y$를 각각 하나의 정수 분할까지 안다면, 그 합 역시 하나의 정수 분할까지 추론할 수 있다. 그러나 $GreaterThan(X, Y)$, $Positive(K)$, $Sum(X, K, Z)$가 $GreaterThan(Z, Y)$를 함의하는 것 또한 참이다. 이는 더 큰 분할에 대해 이루어지는, 정확히 같은 종류의 추론이다. 더 나아가 가장 작은 이 분할조차 원자적이지 않다. $7(X)$은 $X$가 플라톤적인 7과 같다는 뜻이 아니라, $X$가 7 분할 안에 속하는 무한히 많은 것 중 하나라는 뜻일 뿐이다. 현실의 예를 들면, IEEE 부동소수점 표준은 +0과 -0을 구별한다. 즉, 대부분의 목적에서 $0(X)$은 우리가 하나의 값이라고 부르는 것을 나타내지만, 어떤 목적에서는 두 개를 나타낸다. 그리고 우리의 지식 표현이 이 두 해석을 동시에, 자연스럽게 다룰 수 있는 것은 유용하고 중요하다.

여기까지 왔다면 $Real(X)$ 같은 타입 선언이 다른 모든 선언과 마찬가지로 $X$의 영역을 줄이는 또 하나의 방식임이 분명할 것이다. 그리고 위에서 했던 것처럼, 예컨대 $Real(X)$, $Real(Y)$, $Sum(X, Y, Z)$가 $Real(Z)$를 함의하는 경우 그로부터 추론을 이끌어 낼 수 있다. 짠, 타입 추론을 얻었다. 그런데 덧붙이자면 종속 타입도 얻었고, 사실상 세상의 모든 타입 시스템이 가진 다른 기능도 거의 전부 얻었다. 그 타입 시스템들이란 빈약한 모형 위에 일반적인 관계 추론의 가장 중요한 경우들을 다시 도입하려는 임시방편적 시도이기 때문이다.

요컨대 타입은 사물의 공간을 가장 일반적으로 분할한 것에 붙이는 이름일 뿐이고, 값은 가장 세밀하게 분할한 것에 붙이는 이름일 뿐이다(그리고 우리는 그 사이의 광대하고 유용한 영역을 대체로 피한다!). 이들이 질적으로 같다는 사실은 동적 타입 변수들이 보통 타입과 그 타입 영역 안의 값을 모두 부호화하는 복합 값으로 이루어진다는 점만으로도 분명하다. 즉, 타입은 값 자체의 일부다(정적 타입 언어처럼 암묵적으로 부호화되어 있더라도).

달리 말하면, 값은 그저 매우 구체적인 타입이다.

결론적으로 값 계산과 타입 추론은 둘 다 관계 추론의 사례이며, 전통적으로 독립적이고 상호 보완적인 영역으로 다뤄져 왔음에도 서로 다르기보다 훨씬 더 닮아 있다. 여러 프로그래밍 언어의 타입 시스템이 그 자체로 작은 프로그래밍 언어처럼 느껴지는 이유는 정확히 그것이기 때문이다. 그리고 값과 타입 사이에 끊기지 않은 연속체가 아니라 이 거대한 심연이 존재하는 것은 주로 역사적 우연과 관성 탓이다. 객체 지향 프로그래밍, 종속 타입, 일급 타입 등은 모두 이 심연을 잇기 위한 임시방편적 시도다. 하지만 남아 있는 것만 사용한다(즉, 컨테이너 속 값 패러다임과 빈약한 타입에서 출발한다).

애초에 그 심연을 파지 않는 편이 훨씬 쉽다.

[<< | 이전 | 색인 | 다음 | >>]