[프로그래밍 언어론] 타입 시스템

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

 

어떤 타입 시스템이 안전하다는 것은 이 타입 시스템의 타입 검사를 오류없이 통과한 프로그램은 실행중에 타입 오류를 일으키지 않을 것이 보장된다는 의미

 

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

 

타입 규칙(typing rule) :  수식, 문장, 함수 등과 같은 프로그램 구성요소의 올바른 타입 사용 및 그 결과 타입을 정하는 규칙

 

타입 시스템(type system)  :  프로그래밍 언어의 수식, 문장, 함수 등과 같은 프로그램 구성 요소의 타입 규칙들로 구성된 시스템을 그 언어의 타입 시스템이라 함

 

타입 검사를 위해서는 프로그램의 각 지점에서 유효한 변수 혹은 함수들의 타입 정보를 유지하는데 이를 타입 환경(type environment)

 

식 E 에 의해 정의되는 어떤 언어 타입의 타입 시스템은 다음 조건을 만족하면 안전한 타입 시스템(sound type system)

 - 타입 스시템에 의해 어떤 식의 타입이 t 라고 결정했으면 식 E를 실제 실행하여 계산된 값이 반드시 t 값이어야 함

 - 즉 ⊢ E:t 이면 실제 실행에서 E의 계상된 값이 반드시 t 타입이어야 함