6.4 타입 검사 (Type Checking)

의미 없는 프로그램들 let x = 1 in call x(2) end let y = true in x = x + y let proc f(x) : x = x + 1 in f + 2 in call f(f))

의미 있는 프로그램 의미 있는 프로그램만 돌리고 싶다! 실행 중에 문제없이 돌아가는 프로그램 의미 있는 프로그램들 문법에 맞는 프로그램들 의미 있는 프로그램들

질문 어떤 프로그램이 의미 있는지 어떻게 결정할까요? 완전하지는 않지만 타입을 이용해서 결정할 수 있다. 이것이 바로 타입 검사(Type Checking)

타입 검사가 왜 필요한가? 타입 검사란 무엇인가? 정적 타입 검사 프로그램의 신뢰성 향상에 기여 프로그램이 의미가 있는지 타입을 중심으로 검사하는 것 프로그램에서 타입이 올바르게 사용되고 있는지 검사 정적 타입 검사 실행 전에 타입 오류 검사 컴파일 시간에 타입이 잘못 사용된 오류를 검출할 수 있다. 프로그램 신뢰성을 위해 매우 중요한 일 ! 프로그램의 신뢰성 향상에 기여 엄격한 타입 검사는 실행 중에 오류로 갑자기 죽는 프로그램을 미리 예방할 수 있다.

타입 검사 개요 정적 타입 검사(Statically typed) 동적 타입 검사(Dynamically typed) 거의 모든 타입 검사를 컴파일 시간에 한다 Java, Pascal, C++, ML, Haskell 엄격 타입(strongly typed) 언어라고 함 동적 타입 검사(Dynamically typed) 실행 시간에 타입 검사 Lisp, Scheme 타입 검사 안 함 어떤 종류의 타입 검사도 하지 않음(어셈블리어)

타입 및 타입 검사 프로그래머는 식별자의 타입을 선언한다 타입 추론(type inference) 타입 검사 각 식(expression)의 타입을 추론한다. 타입 검사 프로그램에서 타입이 올바르게 사용되고 있는지 검사한다.

지금까지 한 것/앞으로 할 것! Topic Logic Implementation -------------------------------------------- Syntax Grammar Parser Semantics Semantics rules Interpreter Type Typing rules Type checker

타입 규칙(Typing Rule) 타입 검사에 사용되는 규칙 논리적 추론 규칙(logical inference rule) “If this expression has this type and that expression has the other type, then this third expression must have another type.” “if X and Y then Z”

영어를 타입 규칙으로 표현 Read “x : T” as “x has type T”. 규칙 예 If e1 has type Int and e2 has type Int, then e1+ e2 has type Int (e1 has type Int  e2 has type Int)  e1+ e2 has type Int (e1 : Int  e2 : Int)  e1+ e2 : Int

영어를 타입 규칙으로 표현 추론 규칙 예 (e1 : Int  e2 : Int)  e1+ e2 : Int 일반적 형태 Hypothesis1  …  Hypothesisn  Conclusion 추론 규칙 Hypothesis1 … Hypothesisn Conclusion

타입 규칙 예 정수와 + 식에 대한 타입 규칙: ⊢ n : int ⊢ e1 : int ⊢ e2 : int ⊢ e1+e2 : int 식 2 + 5의 타입은 ? ⊢ 2 : int ⊢ 5 : int ⊢ 2+5 : int 그런데 x+y의 타입은 ? 변수 x와 y의 타입에 따라 다르다! 유효한 변수의 타입을 유지하는 Type env가 필요하다!

타입 규칙 예 Type environment 각 지점에서 유효한 변수들의 타입 정보를 유지한다. T: Var → Type Example: T = {x ↦ int, y ↦ int} 변수 x의 타입은 ? T(x) = t T ⊢ x : t 식 x + y의 타입은 ? T ⊢ x : int T ⊢ y : int T ⊢ x+y : int

타입 규칙의 의미 ⊢는 타입 규칙에 의해서 “증명 가능함”을 의미한다. 안전한(sound) 타입 시스템 ⊢ e : t이면 실제 실행에서 e의 계산된 값이 t 타입이다. If ⊢ e : t and e → v, then v : t

우리 언어 Stmt S  x = E; | S1; S2 | if E then S | if E then S1 else S2 | while E do S | read x | print E | let t x = e in S end | let t2 proc f(t1 x) : S1 in S2 end | return E | call f(E) Expr E  n | x | true | false | E + E | E – E | E * E | E / E | E == E | E < E | E > E | !E

타입 규칙: 상수/변수/식 상수를 위한 규칙 T ⊢ n: int T ⊢ true : bool T ⊢ false : bool 변수를 위한 규칙 T(x) : t T ⊢ x : t 식을 위한 규칙 T ⊢ E1 : int T ⊢ E2 : int T ⊢ E1 : t T ⊢ E2 : t T ⊢ E1+E2 : int T ⊢ E1 == E2 : bool

타입 규칙: 대입문/복합문/조건문 대입문을 위한 규칙 T ⊢ x: t T ⊢ E: t T ⊢ x = E : void 복합문을 위한 규칙 T ⊢ S1: t1 T ⊢ S2: t2 T ⊢ S1; S2 : t2 조건문를 위한 규칙 T ⊢ E: bool T ⊢ S: t T ⊢ E: bool T ⊢ S1: t T ⊢ S2: t T ⊢ if E then S : t T ⊢ if E then S1 else S2 : t

타입 규칙: 반복문/입출력/블록 반복문을 위한 규칙 T ⊢ E: bool T ⊢ S: void T ⊢ while E do S : void 입출력을 위한 규칙 T ⊢ x: t T ⊢ E: t T ⊢ read x : void T ⊢ print E : void 블록을 위한 규칙 T ⊢ E: t1 T[x ↦ t1] ⊢ S: t2 T ⊢ let t1 x = E in S end : t2

Example let int x = 0 in x = x + 1 end 타입 검사 {x ↦ int} ⊢ x : int {x ↦ int} ⊢ 1 : int {x ↦ int} ⊢ x : int {x ↦ int} ⊢ x + 1 : int { } ⊢ 0 : int {x ↦ int} ⊢ x = x + 1 : void { } ⊢ let int x = 0 in x = x + 1 end : void

타입 규칙: 함수/프로시저 함수 정의 및 타입 리턴문의 타입 규칙 T ⊢ E: t T ⊢ return E : t 함수 정의 bool f(int x) : if x > 0 then return true else return false 함수의 타입 f: int  bool 리턴문의 타입 규칙 T ⊢ E: t T ⊢ return E : t

타입 규칙: 함수/프로시저 T(f) = t1  t2 T ⊢ E: t1 함수 정의의 타입 규칙 T[x ↦ t1] ⊢ S: t2 T ⊢ proc t2 f(t1 x) S : t1  t2 함수 호출의 타입 규칙 실매개변수 타입 = 형식 매개변수 타입 호출 결과 타입 = 함수의 f의 반환 타입 T(f) = t1  t2 T ⊢ E: t1 T ⊢ call f(E) : t2

Example 다음 함수의 타입은 bool f(int x) : if x > 0 then return true else return false T[x ↦ int] ⊢ x : int T[x ↦ int] ⊢ 0 : int T[x ↦ int] ⊢ true : bool … T[x ↦ int] ⊢ x > 0 : bool T[x ↦ int] ⊢ return true : bool … T[x ↦ int] ⊢ if … : bool T ⊢ proc bool f(int x) if … : int  bool

Example 다음 문장에 대한 타입 검사 ? T(f) = int  bool T ⊢ 1: int call f(1); T ⊢ call f(1) : bool

타입 검사 과정 타입 검사는 각 식 e에 대해서 e:t라는 것을 증명한다. 각 식 종류에 대해서 하나의 타입 규칙이 있다. 이 증명은 AST와 같은 모양을 갖는다. AST의 각 노드에 대해서 하나의 타입 규칙이 사용된다. 식 e의 노드에서 가정은 e의 부분식들이고 결론은 e의 타입이다. 각 식 종류에 대해서 하나의 타입 규칙이 있다. 타입 검사 과정은 AST에 대한 상향식 패스이다.

타입 검사 과정 예 (x+y)*z x y z * + int int int int int