[프로그래밍 언어론] 타입 시스템
타입 오류
앞선 포스팅을 통해 여러 언어의 타입 검사 방식에 대해 알아보았는데, 몇몇 언어는 타입 검사를 통과하지 못하면 타입 오류가 발생해 프로그램을 실행하지 않았다. 이것은 코드가 문법에는 오류가 없지만 내용적 측면에 오류가 있기 때문인데, 코드에 문법적인 문제는 없으므로 Parser에서 해당 오류는 검출되지 않는다. . 내용적 측면에서 발생할 수 있는 오류는 여러 가지가 있으며, 이중 수식이나 문장 등이 타입에 맞지 않게 잘못 사용되는 것을 타입 오류(Type Error)라 한다. 타입 오류의 정확한 정의는 다음과 같다. 타입 오류는 프로그램 실행 중 수식, 문장, 함수 등의 프로그램 구성 요소가 타입에 맞지 않게 잘못 사용되어 발생하는 오류이다. int 타입 변수에 논리 부정 연산 !을 적용하는 것도 타입 오류의 한 예시이다.
타입 검사의 필요성
앞의 포스팅에서 프로그래밍 언어는 프로그램 실행 전 타입 검사를 하여 실행 중 발생 가능한 타입 오류를 모두 찾아낼 수 있는가에 따라 강한 타입, 약한 타입의 언어로 분류할 수 있다고 하였다. 강한 타입 언어는 타입 검사에서 오류 발생 가능성이 있는 프로그램은 아예 실행하지 않고 안전한 프로그램만 실행시켜 프로그램 실행에서 안정성을 얻을 수 있다.
타입 검사 이외에도 구문 검사(Syntax Grammar)라는 것이 있는데, 이것은 프로그램이 구문법(Syntax)에 맞게 작성되었는지 검사하는 1세대 기술이다. 타입 검사는 프로그램 구성 요소가 데이터 타입에 맞게 올바르게 사용되는지 검사하는 2세대 기술이며, 안전한 타입 시스템을 가진 언어에는 ML, Haskell, Java 등이 있다. 안전한 타입 시스템의 타입 검사를 통과하면 타입 오류가 발생하지 않음을 보장한다.
엄격한 타입 검사를 하는 강한 타입의 언어로는 Java, ML, C#, Python이 있고, 느슨하게 타입 검사를 하는 약한 타입 언어에는 C, C++, PHP, Perl, JavaScript 등이 있다. 앞서 언급하였듯 강한 타입 언어는 타입 검사를 통해 프로그램 실행 중 타입 오류 발생을 최대한 막으며, 약한 타입 언어는 느슨한 타입 검사를 하므로 타입 검사를 통과하여도 프로그램 실행 중 타입 오류가 발생할 수 있다.
타입 검사의 종류
타입 검사를 어느 시간에 실행하느냐에 따라 정적 타입 검사 혹은 동적 타입 검사로 나눌 수 있다. 정적 타입 검사는 타입 검사를 프로그램 실행 전 컴파일 시간에 하여 타입 오류를 발견하면 오류 메세지를 출력한다. 정적 타입 검사를 하는 언어에는 C, C++, Java, Pascal, ML, Haskell 등이 있다. 반대로 프로그램 실행 시간, 즉 런타임에 타입 검사를 하는 언어는 동적 타입 언어이며 이러한 언어에는 Lisp, Scheme, Perl, Python, JavaScript 등이 있다. 이 언어들은 컴파일을 하지 않고 인터프리터에 의해 수행된다. 동적 타입 언어에도 엄격한 타입 검사를 하는 강한 타입 언어가 있는데 Erlang, Python이 이에 해당한다. 그렇다면 이런 타입 오류는 어떻게 검사할까?
타입 시스템
타입 규칙이란 수식, 문장, 함수 등의 프로그램 구성 요소의 올바른 타입 사용 및 그 결과 타입을 정하는 규칙이며, 언어의 타입 규칙으로 이루어진 시스템을 타입 시스템이라 한다. 즉, 프로그램 구성 요소의 타입 규칙들로 구성된 시스템을 그 언어의 타입 시스템이라 한다. 타입 검사는 논리적 추론 형태로 기술할 수 있는데, "X와 Y가 성립하면, Z가 성립한다"를 "if X and Y then Z"와 같이 표현한다.
그 예시로 S 언어의 E1 + E2를 예로 들어보자. S 언어에서 수식의 덧셈은 E1, E2 모두 int 타입이어야 하며, 그 결과 타입 역시 int 타입이어야 한다. E1 + E2의 결과 타입이 boolen, string 등이라면 이것은 타입 오류이다. 이것을 p -> q 형태로는 (E1 has type int and E2 has type int) -> E1 + E2 has type int로 기술할 수 있고, 기호로도 표현할 수 있다. e가 t 타입임을 의미하는 |- e: t 표현을 이용해서 논리 형태로도 표현할 수 있다. 1) |- n: int, 2) |- E1: int, |- E2 : int -> |- E1 + E2: int.
타입 환경
그렇다면 변수를 포함하는 a + b와 같은 수식의 타입을 결정해보자. 이 수식에서는 변수 a와 b의 타입에 따라 a + b 수식의 타입을 결정해야 하므로, 문장에서 유효한 변수의 타입 정보를 유지해야 한다. 타입 검사를 위해서는 프로그램의 각 지점에서 유효한 변수 혹은 함수들의 타입 정보를 유지하며, 이것을 타입 환경(Type Environment)이라 한다. 타입 환경 T는 다음과 같이 변수 / 함수의 이름인 식별자 집합 Identifier에서 타입의 집합 Type으로 가는 함수 T: Identifier -> Type으로 표현할 수 있다.
T = { x |-> int, y |-> int}는 프로그램의 특정 지점에서 x와 y 변수가 유효하며, 두 변수의 타입은 모두 int임을 뜻한다. 이전에 알아본 상태(state)는 변수의 의미(값)을 유지하는 반면, 타입 환경은 변수의 타입 정보를 유지한다. 따라서 이제 어떤 변수의 타입 정보를 결정할 때에는 타입 환경과 함께 정의할 수 있다. T(x) = t -> T |- x: t는 타입 환경 T에서 변수 x의 타입이 t라면, x의 타입이 t라는 것을 의미한다. 그렇다면 이제 타입 환경 T에서 수식 x + y의 타입을 결정한다면 T |- x: int, T |- y:int -> T |- x + y: int와 같이 표현할 수 있다.
타입 안정성
일반적으로 |- E: t 표현은 타입 시스템에 의해 E가 t 타입인 것을 증명 가능함 또는 E가 t 타입임이 성립하는 것을 뜻한다. 식 E에 의해 정의되는 어떤 언어의 타입 시스템이 다음 조건을 만족하면 안전한 타입 시스템(Sound Type System)이라 한다.
1) 타입 시스템에 의해 어떤 식의 타입이 t라 결정했으면, 식 E를 실제로 실행하여 계산된 값의 타입은 반드시 t 타입이어야 한다.
2) 즉, |- E: t이면 실제 실행에서 계산된 E의 값은 반드시 t 타입이어야 한다.
위 조건을 정형화하면 If |- E: t and V(E) = v, then v: t이다. 이는 이 타입 시스텡믈 이용한 검사에서 식 E가 타입 오류가 없다면 실제로 수식 E의 실행에서도 타입 오류가 없음을 뜻한다. 조금 어려울 수 있는데, 언어를 설계할 때 수식 E를 t 타입으로 설계하였다면, 실제 실행에서도 반드시 수식 E의 실행 결과 값은 t 타입이어야 함을 뜻한다.
Unsound Type System 언어는 C, C++ 등으로 이 언어들은 느슨한 타입 시스템을 가지고 있다. Pascal과 Ada는 허상 포인터에서 오류가 발생할 수 있으므로 Sound Type System 언어라 할 수 없으며, ML과 Java 언어는 Sound Type System을 가진 언어이다.
타입 검사의 구현
타입 검사를 위해서는 타입 환경을 우선 구현해야 하는데, 이것은 스택 자료구조를 이용하여 구현할 수 있다. 타입 t의 변수 혹은 함수가 선언되면 해당 엔트리를 타입 환경을 의미하는 스택에 추가하면 된다. 즉, int 타입의 변수 v1이 선언되면 스택에 변수 명 v1과 변수의 타입 int를 엔트리 형태로 stack에 push하면 된다.
타입 환경을 구현하였으므로 다음은 타입 검사를 구현한다. 타입의 검사는 어떻게 할 수 있을까? 앞서 E1 + E2의 예시에서 살펴보았듯 수식(Expr)이 어떤 타입을 가지는지에 따라 검사하면 된다. 언어 S의 타입은 int, bool, string이므로 E1의 타입이 int이고 E2의 타입도 int라면 + 연산에서 타입 검사를 통과할 수 있다. 따라서 if (E1.type == Type.int && E2.type == Type.int)의 조건문을 통과하면 타입 검사를 통과한 것이고, 이 조건문을 통과하지 못하면 타입 오류를 발생시키면 된다.
비교 연산 역시 마찬가지다. E1 < E2에서 두 수식의 타입이 같아야 비교 연산을 할 수 있으며, 두 수식의 타입이 같지 않은 경우에 타입 오류를 발생시키는 방법으로 수식의 타입 검사를 구현할 수 있다. 이와 같은 방식으로 수식 이외에 여러 문장의 타입 검사를 구현할 수 있다.