Lecture 7: Type System

7-1) 타입 오류와 타입 검사

 

타입 오류(type error)는 프로그램 실행 중에 수식, 문장, 함수 등의 프로그램 구성요소가 타입에 맞지 않게 잘못 사용되어 발생하는 오류이다

 

타입 검사는 타입 정보를 이용하여 실행 중에 발생 가능한 타입 오류를 미리 검사하는 것 이다.

 

안전한 타입 시스템을 갖춘 대표적인 언어로는 ML, Haskell, Java 등이 있다

 

타입 오류를 찾아 낼 수 있는 언어를 강한 타입 언어(strongly typed language)라고 한다. 예를 들어, Java, ML, C#, Py thon 등은 강한 타입 언어의 대표적인 예이다

엄격하게 타입 검사를 하여 실행 중 타입 오 류가 발생할 가능성을 원천적으로 차단할 수 있는 타입 시스템을 안전한 타입 시스템(sound type system) 이 라고 한다.

 

느슨한 타입 규칙을 적용하는 언어는 약한 타입 언어(weakly typed language)라고 한다. 예 를 들어, C/C+ + , PHP, Perl, Java Script 등은 약한 타입 언어의 예이다. 약한 타입 언어에 서는 타입 규칙이 엄격하지 않으므로 타입 규칙을 적용하여 타입 검사를 하더라도 이 검사 를 통과한 프로그램이 실행 중에 타입 오류가 발생할 수 있다.

 

정적 타입 검사는 프로그램 내에 선언된 변수나 함수의 타입 정보를 이용해서 프로그램의 구성요소(변수, 수식, 문장 등)가 타입에 맞게 올바르게 사용되고 있는지를 컴파일 시간에 검사하는 것이다

 

정적 타입 검사를 하는 대표 적인 언어로는 C, C++, Java, Pascal, ML, Haskell 등을 들 수 있다.

 

실행 시간에 타입 검사를 하는 동적 타입 언어도 있는데 컴파일을 하지 않고 인터프리터에 의해 수행하는 Lisp, Scheme, Perl, Python, JavaScript 등의 언어가 여기에 해당된다. 동적 타입 언어 중에서도 엄격한 타입 검사를 하는 엄격 타입 언어가 있는데 Erlang, Python 등 이 이러한 언어에 속한다

 

7-2) 타입 시스템 개요

 

이 문장을 기호화된 타입 규칙으로 표현하면 다음과 같다. “x : t”는 “x has type t”이라 는 것을 나타낸다.

                                      (E1 : int A E2 : int) -> El + E2 : int

 

⊢ e:t 표현은 타입 규칙에 의해서 e가 t 타입임이 성립함 또는 증명 가능함을 의미한다.

타입 환경 Γ 는 다음과 같이 변수 혹은 함수의 이름인 식별자 집합 Identifier에서 타입 집합 Type으로 가는 함수로 표현될 수 있다.

 

프로그램의 어느 지점에서 유효한 변수가 x,y이고 그들의 타입이 int 이면 그 지점에서 타입 환경은 당므과 같이 표현할 수 있다.

 

 

 

 

 

 

언어를 설계할 떄 그 언어의 수식이나 문장들의 타입 규칙을 설계하며 이들을 총칭하여  그 언어의 타입 시스템이라고 한다.

 

7-3 언어 S의 타입 시스템

 

대입문

 

리턴문

대입문과 유사

 

 

if문

 

 

1. 조건식 E는 bool 타입이어야하고

2. then 부분문장 s1과 else부분 문장S2가 같은 타입이어야한다.

 

복합문

fun int f(int x){
	x=x-1;
    if(x>0) then return x;
    else return -x;
}

1. 복합문의 첫번째 문장 S1은 반드시 void타입이어야한다.

2. 복합문의 두번째 문장 s2는 임의의 타입이 가능하며 이 타입의 복합문의 결과 타입이 된다.

 

while문

1. while문의 조건식 E는 bool 타입이어야 한다.

2. while 문 내에서 return 하면 안 된다. 이렇게 하기 위해서 S는 반드시 void 타입이어야 한다.

 

 

ML, Java는 안전한 타입시스템을 갖추고 있고 컴파일 과정에서 엄격하게 타입 검사를 함으로써 실행시간에 타입을인한 오류를 예방하고 안전성을 높인다.

(Pascal과 Ada는 허상 포인터 등의 문제로 완전하게 안전하지 않다)

 

C/C++언어는 느슨하면서 안전하지 않은 타입 시스템을 갖추고 있다.(캐스트나 포인터 연산 때문) 

 

7-4) 타입 검사 구현

 

-타입 환경은 Stack 형태로 유지

-입력 명령어의 AST를 순회하면서 해당 타입 규칙을 적용하여 검사한다.

-타입 오류에 대해서 오류 메시지를 출력한다.

 

이항 연산의 타입 검사

두 식(b.term1과 b.term2)의 타입을 먼저 검사(Check)하고 그 두 타입 t1, t2를 비교함으로써 구현할 수 있다. 산술연산의 경우에는 두 식이 모두 정수 타입(Type.INT)인지 검사한다. 비교 수식의 경우에는 두 식이 같은 타입인지 검사한다.

 

 

단항 연산의 타입 검사

 

피연산자인 수식(u,expr)의 타입을 먼저 검사하고 단항 연산자의 종류('!' 혹은 '-')에 따라 피연산자의 타입이 부울 타입(Type.BOOL)인지 정수 타입(Type.INT)인지 확인함으로써 구현할 수 있다.

 

 

복합문의 타입 검사

복합문에서 앞의 문장은 반드시 void타입이어야하고 return 문이 먼저 오고 그 다음에 다른 문장이 오면 타입 오류를 으미힌다.

따라서 복합문(Stmts) 내의 문장들(ss.stmts)의 타입을 순서대로 하나씩(Check)함으로써 구현할 수 있다. 마지막 문장을 제외한 다른 문장에서 리턴하면 타입 오류에 해당한다.

 

if문의 타입 검사

조건식이 부울 타입(Type.BOOL)인지 검사하고 then 문장(c.stml)과 else문장(c.stmt2)의 타입을 검사(Check)하고 이 둘의 타입이 같은지 비교하여 구현 가능

 

while문의 타입 검사

while문의 조건식은 bool타입이어야 하고 반복문 내에서 return 할 수 없도록 본체는 반드시 void 타입이어야한다. 

조건식이 부울 타입(Type.BOOL)인지 검사하고 반복문의 본체 문장(l.stmt)을 타입 검사(Check)하고 그 결과 타입이 Type.VOID인지 확인함으로써 구현 가능

 

let문의 타입 검사

1. let문이 시작되면 선언된 변수 id가 유효해짐으로 변수 id의 타입 정보를 타입 환경에 추가(addType)

2. 이 새로운 타입 환경에서 문장S의 타입을 검사하고 결정한다.(Check)

3. 결정된 문장S의 타입이 let문의 타입이 된다.(return l.type)