타입을 특별한 구성 요소가 아니라 관계적 소속과 컴파일 시점의 의미 구분으로 바라보는 글.
[프로그래밍 언어 이론, 타입 이론, 인식론]
이 글은 대체로 타입 이론에 지침의 보충편이므로, 거기서 시작하는 편이 좋을지도 모른다. 다만 이 글 자체로도 이해할 수 있게 해 보겠다.
나는 정확히 말해 “타입”이 무엇이고, 무엇을 의미하며, 무엇을 더하는지를 거의 영원히 고심해 왔다. 결국 나는 그것이 아무것도 더하지 않는다는 사실을 깨달았다(충분한 토대에 대해서는). 그래서 여러 해 동안 혼란스러웠던 것이다. 하지만 사라지지 않는 한 가지 남은 문제가 있었고, 그것은 최근에야 떠올랐다. 아래에서 개괄하겠다.
그것이 (거의) 아무것도 더하지 않는다는 점과 관련해, 그 역사는 이렇다. 컴퓨터 과학과 수학의 학자들은 지나치게 제한적이거나 지나치게 독단적인 여러 체계를 만들었고, 그로 인해 생긴 문제를 고치기 위해 더 많은 기계를 도입해야 했다.
예를 들어 러셀의 역설은 궁극적으로는 당신이 적어 낼 수 있는 모든 공식이 잘 정의된 값을 가진다는 가정에서 비롯된다. 이는 가 해결될 수 없다는 점을 간과하는 것만큼이나 어리석으며, 단지 한 단계 더 우회되어 있을 뿐이다. 가 규칙으로 제출되는 것을 금지하는 바로 그 장치는, 굳이 적용하기만 한다면, 러셀의 공식도 금지한다. 주목할 점은 이 사실이 개념적으로는 문제에 대한 영리한 비전문가의 전형적인 첫 반응과 정확히 같다는 것이다. 학자들은 그들이 옳은데도 보통 온갖 난해화와 우회 논리로 이를 일축한다. (전형적인 학자는 이 문제에 대해 복잡하고 난해하며 형식적인 답을 여럿 알고 있지만, 자기 자신의 난해화 때문에 그것들이 비전문가의 첫 반응과 정확히 같다는 사실을 알아보지 못한다.) 여기에는 볼 것이 없다. 계속 가라.
한편 커리-하워드 대응은 이전에 무관했던 두 것 사이의 신비로운 유사성과는 거리가 멀다. 그것은 프로그래밍 언어에 덧붙인 타입 체계가 그 언어들에서 제거했던 관계 논리의 일부를 그저 다시 도입하고 있었음을 인정하는 일일 뿐이다.
이런 호의적이지 않은 요약에서 얻을 교훈은 다음과 같다. 먼저 문제의 원인을 찾는 편이 낫다. 이전의 실수를 되돌리는 일은 언제나 그것을 보상하는 일보다 낫다.
이는 “타입”이라는 개념과 관련이 있다. 타입에는 많은 짐이 붙어 있기 때문이다(부분적으로는 위의 비문제를 해결하기 위해서다). 타입은 매우 중요하고, 많은 부담을 지며, “정확성”과 인수분해(클래스) 등의 중심에 있는 듯 보인다. 따라서 그것이 필요하지도 유용하지도 않다는 함의는 표면상 다소 터무니없어 보인다.
하지만 우리는 약간의 역사를 풀어내고 사물을 더 단순하게 다시 세우기만 하면, 훨씬 단순하고 일반적인 것에 도달한다. 무언가를 배우는 데 걸리는 시간보다 그것을 잊는 데 걸리는 시간이 훨씬 더 길다는 사실은 불쾌하다. 나는 당연하게 받아들였어야 했던 온갖 쓰레기를 뇌에서 문질러 지우며 경력 전체를 보낸 듯하다.
첫째, 타입 이론에 지침에서 언급했듯이, “타입”의 기능 거의 전부는 괜찮은 관계적 표현에 사소할 정도로 포섭된다. 즉 타입이 쓸모없는 개념이라기보다, 이미 존재하는 개념이라는 뜻이다. 가장 일반적인 형태에서 타입은 관계적 소속과 동의어다. 나는 여기서 요지를 지나치게 제한하지 않기 위해 두 패러다임(관계 논리, 집합 소속)을 섞고 있다. 집합 소속이라 부르든, 술어 함수의 참값이라 부르든, 상관없다. 이는 흔하고 직관적인 생각이다. “과일”은 “타입”이다. “Y보다 큰 값”도 그렇다. 전자를 후자보다 훨씬 더 자주 타입으로 생각하는 이유는 대체로 실용적인 이유 때문이지만(뒤에서 다룬다), 이들은 동일한 인식론적 구성물이다.
역사적으로 “값”과 “타입” 사이의 결정적 분기는 다음으로 귀결되었다. 값은 프로그램이 실행될 때 신뢰성 있게 계산할 수 있는 것이다. 타입은 프로그램이 컴파일될 때 신뢰성 있게 계산할 수 있는 것이다. 여기서 핵심은 계산의 표현과 규칙이 완전히 통합될 수 있다는 점이다(예를 들어 관계 논리로). 하지만 이 두 집단이 실용적으로 서로 다른 역할을 맡았기 때문에, 역사적으로는 그렇지 않았다.
나아가, 컴파일과 실행 사이의 선을 흐리기 시작하면 이 실용적 경계 또한 무너지고, 우리는 그 선을 완전히 버린 뒤 타입과 값 사이를 구별하지 않는 단일한 통합 표현을 고수하는 편이 즉시 더 나아진다.
따라서 이것이 여러 방식으로 타입을 특별한 구성물로 필요로 하지 않는다는 나의 논증이다. 우리가 보통 타입으로 하는 모든 일은 그대로 남지만, 이제 다른 모든 것과 동등한 지위의 평범한 관계적 사실과 규칙이 된다.
하지만 한 가지 중요한 예외가 있다. 그리고 이것이야말로 타입이라는 개념을 특별한 구성물로서 오래전에 사라져 버리지 않도록 붙들어 둔 것이라고 나는 생각한다.
위의 정의, 즉 _타입은 프로그램이 컴파일될 때 신뢰성 있게 계산할 수 있는 것_을 다시 보면, 이것은 다른 무언가를 함의한다. 그것은 프로그램이 작성될 때 알려진 것이다. 즉 프로그래머 자신이 아는 것이다. 물론 그것은 그 지식의 부분집합일 뿐이며, 이는 다시금 더 일반적인 표현으로 옮기는 편이 낫다는 점을 강하게 시사한다. 하지만 특히 그것은 매우 쉽게 얻을 수 있는 부분집합이다. 일반적으로 타입 논리는 꽤 사소하다. 타입 정보를 제외한 모든 코드 세부 사항을 제거하면, 타입이 이미 모든 곳에 명시되어 있지 않은 한, 매우 기본적인 데이터 흐름 문제만 남는다. 그리고 우리 관계적 진실 가운데 이처럼 쉽게 추론되는(코드 작성 또는 컴파일 시점에) 부분집합은 우리가 작성하는 코드에 _암묵적 문맥_을 만든다. 그리고 이 문맥은 다시 타입의 마지막이자 실제이며 다소 사소하지만 진정으로 특별한 구성물 기능을 제공한다. 그것은 우리가 구문 수준에서 _언어_를 모호하지 않게 해석하도록 해 준다.
예를 들어, 이것은 우리가 “length”라는 단어를 쓰고 컴파일러가, 프로그래머 자신이나 코드를 읽는 사람이 그러하듯, 그것이 개수를 뜻하는지 기하학적 크기를 뜻하는지 알 수 있게 한다. 그리고 여기서 실행 시점에 이를 맡기는 코드는 컴파일될 수 없어야 한다는 점을 강조하고 싶다. 코드를 작성할 때 자신이 의도한 length의 의미를 모른다면, 자신이 무엇을 쓰고 있는지 모르는 것이며 컴파일러도 모른다. 이것을 객체의 세부 사항에 따라 여러 다른 방식으로 계산할 수 있는 _디스패치_와 혼동하지 말라. 여기서 우리가 해결하는 것은 계산하는 방식이 아니라, 무엇을, 즉 어떤 의미를 계산하는가다.
우리는 이를 C++ 또는 Java 스타일의 정적 타이핑에서 실제로 보며, 그 가치는 단지 언어의 압축이다. 즉 서로 다른, 비록 흔히 어느 정도 비슷한, 의미에 같은 단어를 재사용할 수 있게 하는 것이다.
여기서 중요하고 유용하게 볼 점은 이 뚜렷한 기능적 구분이다.
정적 타입 기반 의미 구분은 전적으로 의사소통을 위한 편의 기능이며, 사실상 구문 설탕이다. 서로 다른 문맥에서 서로 다른 것을 위해 토큰을 재사용함으로써 조금 덜 쓰게 해 준다. 이는 작은 코드 압축일 뿐이며, 전부다. 그리고 이것이 타입이 수행하는 유일한 진정한 특별 기능이다.
하지만 이제 이를 보았으므로, 하나의 속성 외에는 타입으로 인정되는 것을 더 이상 제한할 필요가 없다. 즉 컴파일 시점에 알아낼 수 있어야 한다는 속성이다(매개변수나 데이터를 알기 전에 코드 자체에서 분명해야 한다). 다시 말해, 원칙적으로 우리는 무엇이든 문맥적 모호성 제거 장치로 사용할 수 있으며, 깔끔한 타입 계층이나 그와 비슷한 것에 자신을 제한할 필요가 없다. 일반적으로 그렇게 하는 것은 규칙이나 절차를 구상할 때 무엇을 쉽게 알아낼 수 있는지, 그리고 우리의 언어(자연어와 수학적 언어 모두)가 그에 맞추어 어떻게 발전했는지에 관한 실용적 현실일 뿐이다.
그 밖의 모든 것, 그리고 우리가 보통 타입에 돌리는 모든 무거운 작업은 이제 평소와 같은 관계 논리일 뿐이다. 사라진 것도, 쓸모없어진 것도 아니다. 단지 더 이상 특별 사례가 아닐 뿐이다. 모든 동일한 패턴이 적용되며, 이제 가운데를 가르는 제한적인 선만 없을 뿐이다.
