타입과 타입 시스템 : 연재를 시작하며 ⇠ 사색송어

들어가며

타입type.

TypeError: unsupported operand type(s) for +: 'int' and 'str'

TypeError: "x" is not a function

타입!

프로그래머라면 이 단어를 하루에도 몇 번은 마주할 것이다. 타입은 프로그램을 작성할 때에도, 문서를 읽을 때도, 또 디버깅을 할 때도 중요한 요소로 작용한다. 훌륭한 타입 시스템을 가진 언어를 쓸땐 타입 체커type checker가 프로그래머의 실수를 잡아줘 마치 컴파일러와 페어 프로그래밍을 하는 듯한 신기한 경험을 하게 된다. 한편 사려 깊지 않게 구현된 타입 시스템은 별로 도움은 주지 않으며 ”대체 왜 이걸 일일이 적어줘야 하는 거야” 따위의 불평만 불러일으키는 주범 취급을 받기도 한다.

어느 쪽이든, 타입과 타입 시스템type system은 프로그래밍에서 굉장히 큰 비중을 차지한다. 그런데도 이 주제를 다루는 자료 대부분이 특정 언어의 타입 시스템에 대해 다루는 수준에서 그친다. 그 때문에 타입 시스템 전반에 대한 지식을 폭넓게 다루는 자료가 너무 없다는 아쉬움을 갖게 되었다. 그런 아쉬움을 해소하고자 하는 조그만 시도의 하나로 타입과 타입 시스템에 대한 연재를 해보려 한다.

부디 즐기시길!

독자분들께

평어체로 써놓으니 왜인지 어색하여 이 부분만 경어체로 작성합니다.

저는 이 주제로 학위를 받은 적도 없거니와 가진 경력도 그다지 길지 않습니다. 글을 써나가며 공부를 게을리하지 않겠으나 부족한 부분이 많을 것입니다. 글에서 잘못된 정보를 발견하신다면 부디 메일 등의 수단으로 알려주시길 부탁드립니다. 이어질 글들이 첫 선보임 이후에도 독자분들께서 지적/보충해 주신 내용을 바탕으로 꾸준히 나아지는 것이 저의 바람입니다. 꼭 지적이 아니더라도 연재에 관한 어떤 의견이든 환영합니다. ❤️

또한 저는 이 연재가 타입 시스템에 이미 큰 관심을 두고 있는 일부만이 즐길 수 있는 내용에서 벗어나, 가능한 많은 프로그래머에게 흥미롭게 읽히고 도움이 되길 바랍니다. 그 때문에 이론적 엄밀성을 다소 희생하는 한이 있더라도 저와 같은 보통의 프로그래머에게 더욱 쉽게 다가갈 수 있다면 그 길을 택할 예정입니다. 너그러운 양해 바랍니다. 연재의 기조에 대한 의견도 환영합니다. ❤️

타입과 타입 시스템, 현 위치

흔히 타입 시스템은 (특히 새로운 언어에 막 발을 들이는 프로그래머에게) 별문제 없어 보이는 프로그램을 실행하기 위해 불필요한 노력을 더 들이게 만드는 까다로운 잔소리꾼으로 인식되곤 한다.

하지만 이는 부정적인 편견에 불과하다. 견고한 타입 시스템을 통해, 프로그래머는:

(주석과 다르게) 항상 프로그램의 최신 상태와 합치되는 방식으로 프로그램의 올바른 동작을 기술할 수 있다.
런타임에 발생하는 오류를 예방할 수 있다.
IDE를 비롯한 다양한 도구에게 도움을 줌으로써 자동 완성 등의 기능의 사용을 수월하게 만들 수 있다.

실제로 프로그램을 실행하기 전에 프로그램의 타입이 올바른지 검사하는 정적 타이핑의 가치는 프로그래머 커뮤니티 사이에서 날이 갈수록 점점 인정받는 추세다. Python의 mypy와 3.5 버전에서 정식 문법에 들어온 옵셔널 타입 힌팅 문법, 그리고 Javascript의 Flow와 TypeScript 등 기존에는 런타임에만 타입의 유효성을 검사하던 언어에 정적 타이핑을 도입하려는 시도가 활발히 이루어지고있다는 사실이 이러한 기류를 증명한다.

‘타입스크립트’ 주제 Google Trends ‘타입스크립트‘ 주제 Google Trends

‘mypy’ 검색어 Google Trends

인기와 별개로 실질적인 효과에 대한 의문에는 지난 5월 ICSE 2017에 발표된, 자바스크립트에 정적 타입 시스템을 도입한 결과를 분석한 논문 To type or not to: quantifying detectable bugs in JavaScript. 이 하나의 답을 제시할 것이다. 이 논문은 정적 타입 시스템을 도입했더라면 Github에 공개적으로 올라온 코드의 버그중 최소 15%는 커밋조차 되지 못하고 잡혔을 것이라고 주장하고 있다. 이 결과의 의의에 대한 논의는 논문 내에 인용된 Microsoft 사의 엔지니어링 매니저의 발언을 재인용 하는 것으로 갈음한다.

충격적이다. 만약 개발하는 방식에 어떤 변화를 주어서 저장소에 들어오는 버그중 10% 이상을 줄일 수 있다면, 고민할 이유가 전혀 없다. 개발에 쓰이는 드는 시간이 두 배 이상 늘어나거나 하지 않는 한, 우리는 그 변화를 택할 것이다. That’s shocking. If you could make a change to the way we do development that would reduce the number of bugs being checked in by 10% or more overnight, that’s a no-brainer. Unless it doubles development time or something, we’d do it.

타입과 타입 시스템

그렇다면 과연 프로그래밍에서 타입이란 무엇인지, 그리고 타입 시스템의 역할은 무엇인지에 대해 이야기해보자.

타입의 의의

타입은 프로그램의 ‘올바른 동작’이 무엇인지에 대한 프로그래머의 의도를 인코딩하는 역할을 한다. 두 정수를 더하는 작업과 기계의 특정 메모리 주소로부터 어떤 값만큼 떨어진 주소를 찾는 작업을 생각해보자. 프로그래머는 두 연산을 전혀 다른 의도로 작성하고 사용하겠지만, 이 두 연산 모두 어셈블리 수준에서는 “한 값에 다른 값을 더한다”라는 같은 연산으로 환원된다.

따라서 코드를 읽는 다른 프로그래머 혹은 미래의 작성자 자신에게 이런 프로그래머의 의도를 효과적으로 전달하기 위해서는 이러한 정보를 어딘가에 추가로 기록할 필요가 있다. 때로는 별도의 주석이나 문서 또는 변수명이 그런 기록의 수단이 되곤 한다. 마찬가지로 타입 또한 그러한 의도를 인코딩하는 장소가 될 수 있다.

주석이나 변수명과 다르게 타입은 프로그램의 실제 동작과 일정 수준 이상으로 동떨어질 수 없다는 것이 보장된다. 아래의 자바스크립트 파일을 보자.

// 자기 자신을 리턴한다
function sum(a, b) {
  return a + b;
}

function concat_string(a, b) {
  return a - b;
}
concat_string("a", "b") // NaN

위의 concat_string, sum 함수는 각각 주석 또는 함수명을 읽고 추론할 수 있는 것과는 전혀 동떨어진 동작을 하고 있다. 하지만 이 두 함수는 분명 유효한 자바스크립트 함수이며, 자바스크립트 실행기는 조금의 거리낌도 없이 이 함수를 실행할 것이다. 이런 상황이 발생할 수 있는 이유는 주석과 변수명은 프로그램의 실제 동작과 직접 결합하지 않는, 상대적으로 추상적인 정보이기 때문이다. 이런 불일치에 불만을 가지는 건 프로그래머뿐일 것이다.

반면 타입은 어떨까? 아래 타입스크립트 코드를 보자.

type IdentityFunction = (a: number) => number
const sum: IdentityFunction = (a: number, b: number) => {
	return a + b;
}
// error TS2322: Type '(a: number, b: number) => number' is not assignable to type 'IdentityFunction'.

function concat_string(a: string, b: string): string {
    return a - b;
}
// error TS2322: Type 'number' is not assignable to type 'string'.
// error TS2362: The left-hand side of an arithmetic operation must be of type 'any', 'number' or an enum type.
// error TS2363: The right-hand side of an arithmetic operation must be of type 'any', 'number' or an enum type.

두 함수는 각각 함수 아래에 주석으로 적혀진 오류를 발생시킨다. 올바르지 않은 타입 정보를 가진 프로그램을 실행할 수단이 원천적으로 차단되는 것이다. 주석이나 변수명과는 다르게, 타입 정의와 다르게 동작하는 프로그램은 실행 자체가 불가능하다는 점은 타입을 앞서 언급된 다른 수단보다 훌륭한 명세 수단으로 동작할 수 있게 해 준다.

프로그램의 동작과 강하게 결합한, “올바른 동작”에 대한 기술 수단이라는 타입의 의의에 대해 간단히 다루어 보았다. 다음으로 ‘값이 타입을 갖는다’는 개념을 어떻게 이해할 수 있을지 살펴보자.

집합으로 타입 이해하기

프로그래밍에서의 타입은 수학에서의 집합과 매우 많은 특징을 공유한다.

어떤 프로그래밍 언어 L로 쓰인 프로그램이 가질 수 있는 모든 값의 집합 V를 생각해보자. 이때, V의 원소 중 특정한 조건을 만족하는 값들을 모은 집합을 L에서의 타입 T라고 정의할 수 있다. 예를 들어, MIN_INT, MIN_INT + 1, …, 0, 1, 2, …, MAX_INT 라는 값을 모두 모은 집합을 Integer 라는 타입으로 부를 수 있겠다.

이렇게 타입을 집합으로서 바라볼 때, 아래와 같은 대응 관계가 성립한다.

원소 x가 집합 S에 속한다 (x ∈ S) 👉 값 x는 S 타입에 속한다. (혹은 S 타입을 값 x에 할당assign할 수 있다.)
한 원소가 여러 집합에 속할 수 있다 👉 한 값이 여러 타입에 속할 수 있다.
집합 T가 집합 S의 부분집합이다 (T ⊂ S) 👉 타입 T가 타입 S의 서브타입subtype이다.
조건 제시법을 이용해 기존에 존재하는 집합으로부터 새로운 집합을 만들어낼 수 있다 ( S’ = { (x, y) | x ∈ S, y ∈ S }) 👉 기존 타입의 정의로부터 새로운 타입을 만들어낼 수 있다.
모든 집합의 부분집합인 공집합 Ø이 존재한다 👉 모든 타입의 서브타입인 바닥 타입bottom type이 존재한다 (혹은 존재할 수 있다).

구체적인 예를 들어서 위의 비유를 다시 살펴보자.

L 코드에서의 값 0은 위에서 정의한 Integer 집합의 원소이다. 다시 말해, 값 0에 Integer 라는 타입을 할당할 수 있다.
V의 값 중 0과 1만을 원소로 갖는 집합을 생각할 수 있다. 이 집합을 Binary 라는 타입이라고 부르자. 이때, 값 0은 Integer 타입과 Binary 타입에 동시에 속한다.
Binary 타입에 대응하는 집합의 모든 원소는 Integer 타입에 대응하는 집합의 원소이다. 따라서 Binary 타입은 Integer 타입의 서브타입이다. 다르게 표현하면, Integer 타입 값을 필요로 하는 임의의 자리에 Binary 타입의 값을 넣어도 프로그램은 정상적으로 동작할 것이 보장된다.
이미 존재하는 타입을 이용해 더욱 복잡한 자료형을 만들어낼 수 있다. 예를 들어, 문자열 타입으로부터 두 개의 문자열 필드를 갖는 풀 네임이라는 새로운 타입을 정의할 수 있다. (interface FullName = { first: string; last: string; } )
바닥 타입의 존재 여부는 언어의 구현마다 다른데, 그중 한 예로 타입스크립트의 never 타입을 들 수 있다. 문서에 쓰여 있듯, never 타입을 갖는 실제 값은 존재할 수 없고, never 타입은 모든 타입의 서브타입이며, 다른 어떤 타입도 never 타입의 서브타입이 될 수 없다.

이러한 맥락에서, 프로그래밍 언어가 제공하는 내장 자료형은 언어가 허용하는 모든 값 중 특정한 유용한 특성을 공유하는 일부 값들을 미리 묶어 둔 집합의 모음이다. 또한 프로그래머는 이러한 미리 정의된 집합의 모음을 이용해 무수히 많은 새로운 집합(조합 자료형composite data type)을 정의할 수 있다. 이때, 가능한 조합 자료형의 경우의 수는 다음 (언어에 따라 달라지는) 두 요소에 크게 영향을 받는다.

내장 자료형의 종류. 예를 들어, 언어가 (가상) 기계의 메모리 주소를 직접 드러내는 자료형을 제공하는가? 수(number)를 나타내는 내장 자료형을 얼마나 많이 제공하는가? 등.
가능한 조합의 수단. 예를 들어, “두 번째 값이 첫 번째 값보다 큰 짝pair”과 같은 타입을 표현할 수단을 제공하는가? “원소가 모두 같은 타입인, 크기가 정해져 있지 않은 리스트”와 같은 타입은?

타입 시스템

지금까지 타입의 의의, 그리고 타입을 이해할 수 있는 하나의 관점에 대해 다루었다. 타입을 통해 프로그래머의 의도를 표기할 수 있지만, 프로그램의 모퉁이 모퉁이마다 그러한 의도를 기술 해두었다 한들 그 의도가 실제로 강요되지 않는다면 무의미할 것이다. 타입 시스템은 프로그램 내에 타입을 이용해 기술된 프로그래머의 여러 의도가 말이 되는지, 서로 모순을 일으키지 않는지 검사(타입 검사type check)하는 검사원이다.

현실에서, 같은 일을 수행하는 검사원도 어떤 이는 사소한 오류는 설렁설렁 넘어가지만 어떤 이는 조금의 미심쩍은 부분이라도 보이면 깐깐하게 파고드는 것처럼 개인차가 존재한다. 마찬가지로, 타입 시스템도 큰 목적은 같되 언어마다 그 엄밀함과 능력에 있어 큰 차이가 있다. 오류의 가능성을 절대 허용하지 않고 매우 다양한 종류의 오류를 잡아내는 타입 시스템이 있는 한편, 극히 제한적인 종류의 오류만 검출수 있으며 그런 오류마저도 매우 너그러이 넘어가는 타입 시스템도 존재한다.

더 엄밀하고 더 풍부한 표현력을 가진 타입 시스템이 항상 더 훌륭한 타입 시스템인 것은 아니다. 거의 모든 것이 그렇듯, 여기에서도 트레이드오프가 일어난다. 일반적으로, 타입 시스템이 더욱 엄밀하고 강력해질수록 언어가 복잡해지는 경향이 있으며, 어지간해선 프로그램을 실행조차 못 시키게 하는 컴파일러가 프로그래머에겐 진입 장벽으로 작용하는 경우도 많다.

하지만 이는 어디까지나 경향일 뿐 절대적인 진리는 아니다. 관련된 분야에서 깊은 조예를 가진 이들에게서 탄생한 타입 시스템은 다른 언어들보다 더 적은 노력을 요구하면서도 더 많은 것을 가능케 한다. 다른 언어보다 보다 정확하고 많은 정보를 담을 수 있는 언어가 정작 프로그래머에게는 더 적은 노력만을 요구하는 일은 얼마든지 가능하다.

그런 강력한 타입 시스템을 가진 언어의 예로 Haskell을 살펴보자. 대부분의 언어와는 달리, 하스켈에서는 어떤 함수가 입출력를 수행하는지가 함수의 타입에 인코딩된다. 더욱 쉬운 이해를 위해 예를 들어 살펴볼 수 있겠다. 먼저 타입스크립트로 쓰인 다음의 함수를 보자.

function sum(a: number, b: number): number {
	launchNuclearMissile(); // 핵미사일을 발사한다
	return (a + b);
}

sum 함수는 두 수를 받아 그 합을 리턴하는 함수다. 타입 상으로는 전혀 문제가 없다. 하지만 실제로는 가져다 쓰는 사람도 모르게 핵미사일의 발사 버튼을 누르는 대참사가 발생할 수 있다. 타입스크립트의 타입 시스템은 함수의 인자의 값, 그리고 함수가 리턴하는 값만을 검사하기 때문이다. 비슷한 일을 하는 함수를 하스켈로 짜면 어떻게 될까?

sum a b = do
	launchNuclearMissle
	return (a + b)

하스켈의 타입 시스템은 위 함수의 타입을 Num a => a -> a -> IO a으로 추론한다. 정수인지, 부동 소수인지, 또는 아예 다른 어떤 포맷인지는 모르겠으나 수(number)를 나타내는 a 타입의 두 개 인자를 받아 IO와 연관된 작업을 실행하고 a 타입 값을 리턴한다는 의미다. 이 정의로부터 프로그래머는 컴파일러의 도움을 받아 아래와 같은 사고의 과정을 손쉽게 밟을 수 있다.

두 수의 합을 구하는 작업에는 IO가 끼어들 여지가 없다.
그런데도 이 sum이라는 함수의 타입에는 IO와 연관된 작업을 수행한다고 쓰여 있다.
함수의 내부에서 내가 sum 함수에 기대하지 않는, 어쩌면 위험한, 일을 하고 있음이 틀림없다.

이렇듯, 하스켈의 타입 시스템은 타입스크립트의 그것이 쉽사리 (혹은 절대) 담아낼 수 없는 다양한 정보를 타입 내에 담는 것을 가능케 한다. 더구나, 위 코드에서 볼 수 있듯 프로그래머가 타입에 대한 정보를 전혀 주지 않았음에도 타입 시스템이 스스로 프로그램의 내부를 살펴 함수의 타입을 도출해 내고 있다(타입 추론). 이 단순한 예제를 통해 살펴보았듯이, 서로 다른 언어의 타입 시스템은 종종 같은 개념이라고는 생각하기 힘들 정도로 전혀 다른 수준의 정보를 담아내곤 한다.

연재 계획 및 목표

여기까지 연재를 시작하게 된 동기와 타입과 타입 시스템, 그리고 연관된 기본 개념에 대해 알아보았다. 앞으로 연재를 진행하며 추가로 다룰 주제들에 관해 이야기하며 이번 글을 마무리하고자 한다.

아래 계획은 조금도 틀림 없는 청사진이 아니다. 그렇다기보단, 연재 시작 전 적어도 이런 주제는 다루어야 할 것 같다는 대강의 예측에 불과하다. 주제, 분량 및 순서는 연재를 진행하면서 유연하게 변경될 수 있다.

기본 개념

추후 구체적인 주제들에 대해 논의를 전개해나기에 앞서 필요한 기본 개념들을 논한다. 강타입과 약타입, 정적 타입 검사/동적 타입 검사, 타입 선언과 점진적 타이핑 등을 다룬다.

다형성

프로그래머에게 제약으로 작용하는 타입을 적극적으로 활용하면서도 유연함을 잃지 않기 위한 하나의 수단인 다형성polymorphism에 대해 다룬다. 다형성이란 무엇이고 왜 필요한지, 어떤 종류의 다형성이 존재하며 각각 어떤 특징을 갖는지, 서로 어떻게 다른지 등을 소개한다.

타입 간의 관계

서로 다른 타입 간의 관계에 대해 다룬다. 타입 간의 호환성과 동일성을 판단하는 두 가지 접근법인 구조적 타입 시스템structural type system과 이름에 기반을 둔 타입 시스템nominal(name-based) type system을 소개한다. 덕 타이핑duck typing과 같은 연관된 개념도 함께 다룬다.

그 후, 두 타입 간의 관계로부터 각각의 타입으로부터 파생된 타입 간의 관계를 규정하는 반공변성contravariance, 공변성covariance, 불변성invariance 세 방법에 관해 이야기한다.

대수 자료형

조합 자료형을 만들 수 있는 하나의 방법인 대수 자료형algebraic data type에 대해 간단히 소개한다. 대수 자료형에는 어떤 종류가 있고, 대수 자료형을 이용한 사고 모델이 매일 마주치는 프로그래밍의 문제들을 어떻게 우아하게 풀 수 있도록 하는지 다룬다.

타입 추론

특정 언어를 사용하다 보면 정적 타이핑을 곧 번거로운 타입 어노테이션type annotation 작성과 동일시 할 수 있다. 하지만 사용자를 번거롭게 하는 강제적 타입 어노테이션은 구현의 문제일 뿐, 본질적인 제약 사항이 아니다. 명시적인 타입 선언 없이도 타입 시스템이 제공하는 대부분의 이점을 누릴 수 있게 하는 강력한 기능인 타입 추론에 대해 알아본다.

타입 시스템과 명제의 증명

프로그램의 타입 시스템이 논리적 명제의 증명과 어떤 연관을 가지는지에 대해 보다 자세히 다룬다. 커리-하워드 대응/Curry-Howard isomorphism/을 소개하고, 프로그램이 타입 검사를 통과한다는 것의 의미를 바라보는 다른 관점을 소개한다.

참고 자료

감사의 말

친절히도 글을 먼저 읽어 주시고 또 많은 유용한 조언을 주신 xtendo님, dsm_ 님, markhkim 님, lifthrasiir 님께 감사의 말씀을 전합니다.

타입과 타입 시스템 : 연재를 시작하며

타입과 타입 시스템에 대한 연재를 시작하며.