[UPL] Type System

 

 

 

프로그램은 그냥 문자열일 뿐인고 Parser는 그 문자열을 특정 시각으로 바라보고 AST로 변환한다.

인터프리터는 AST로 변환된 프로그램을 바로 Interpret 하고, 컴파일러는 기계어로 컴파일 후 실행한다. 

 

Syntax가 올바르다고 모두 올바른 프로그램은 아니다. 

모든 프로그래밍 언어에는 Undefined Behaviors가 존재하고, AST로 제대로 변환되더라도 의도하지 않은 실행 결과를 마주할 수 있다.

Undefined - 정의하지 않음 

Unspec - 기술하지 않았지만 어떻게 실행되든 상관없음

 

 

 

 

 

UB의 예시로는.. null값에 대한 dereference, 주소 값 끼리의 대소비교, 파라미터 계산 순서 등이 있다. 

Semantics를 정의할 때 Inference Rule을 사용하는데, Inference Rule의 윗부분 끼리도 순서가 정해져 있지 않은 Unspec이다.

 

UB가 발생하는 순간 프로그램을 예측할 수 없다. 

 

Testing을 통해 프로그램을 실행하고 해당 프로그램이 올바르게 동작하는지를 확인할 수 있지만, 테스트 대상 입력에 대해서만 검증할 수 있다.

Formal Verification을 사용하면 수학, 논리학, 프로그램의 전문가가 개입해 논리 구조로 프로그램의 올바름을 증명할 수 있지만, 비용이 많이 든다. 

 

 

 

 

Type System은 요약 기반으로 프로그램의 올바름을 증명하는 방법으로, 컴파일 과정에 적용되는 가벼운 검증이다.

즉, 프로그램을 실행 가능한 형태로 번역하기 전에 Type Checker를 통해 해당 프로그램이 올바른지 확인하고 UB가 없는지 확인한다.

 

타입은 계산 결과에 대한 Approximation으로, 특정 표현식을 계산했을 때 도출될 수 있는 값을 집합으로 어림잡는 작업을 의미한다.

 

 

 

Complete Approximation과 Sound Approximation이 다름에 주의하자. 

 

if (x > 0) then 3 else true   (* error *)

 

Type System은 해당 문장을 Sound하게 막아버린다.

 

Type System은 Sound Approximation을 통해 UB를 최대한 방지한다.

Well-Typed 프로그램은 UB를 수행하지 않는다. (언어에 따라 모든 UB를 검증할 수는 없고, Well-Typed는 예외를 발생시켜도 된다)

 

프로그램이 올바르게 동작함을 보장하는 것과 올바르지 않은 프로그램을 잡아내는건 다르다.

 

 

 

 

---

 

 

 

프로그램을 해석하기 전 Type Checker를 통해 UB가 없음을 검증하는 기능을 추가하기 위해 MiniC에 Type System을 추가해보자.

MiniC 프로그램에 Type Annotation을 추가해 타입 시스템이 사용하는 타입 힌트를 제공하자. (Python, TypeScript를 생각하면 됨)

 

 

 

 

 

 

Concrete Syntax에 Type Annotation 및 사용자 입력 구문을 추가하자.

Type Annotation은 실행 Context에서는 전혀 영향을 미치지 않으니 타입이 붙은 함수 정의 및 변수 선언에 대한 Semantics도 예전과 같다.

 

 

𝝉 ⩴ unit | int | bool | 𝝉 ∗ | 𝝉 → 𝝉

 

 

이번 프로그램에서의 타입은 네 종류로, 타입 값이 저장된 메모리의 주소 값으로 계산되는 표현식과 𝝉타입을 인자로 받아 𝝉타입을 반환하는 함수를 포함한다. 

Currying Form을 지원하고, unit은 인자를 받지 않는 함수의 파라미터 타입을 기술할 때 사용한다.

 

Γ 𝑙 ⊢ 𝑒 : 𝜏

 

 

Γlocal 은 지역 변수를 위한 타입 문맥으로 변수와 타입 사이 매핑의 집합을 의미한다.

[𝑥 : int, 𝑦 : int] ⊢ 𝑥 + 𝑦 : int => "타이핑 환경 [𝑥 : int, 𝑦 : int] 에서 표현식 x+y 는 타입 int 를 가진다" 로 해석하자. 

 

Γglobal 은 전역 변수를 위한 타입 문맥으로 함수와 타입 사이 매핑의 집합을 의미한다. 

Top-Level 명령문은 반환 타입이 항상 unit이고, 함수는 어디서든 lookup 할 수 있는 위치인 global context에 정의되어야 한다.

 [𝑓 : int → bool], [𝑥 : int] ⊢ def 𝑦 = true ⇛𝑆 [𝑥 : int, 𝑦 : bool] => "전역 타입 환경 [𝑓 : int → bool], 로컬 타입 환경 [𝑥 : int] 이 주어진 상황에서 명령문 def y = true를 실행하면 로컬 타입 환경이 [𝑥 : int, 𝑦 : bool]로 확정된다" 로 해석하자

 

⇛𝑆 기호는 명령문에 대한 타입 판별 결과를 나타낼 때 사용한다.

 

Expression은 계산만 하니까 지역변수만 사용해도 괜찮고, Statement는 Side Effect가 있으니 지역변수와 전역변수도 사용해야 한다.

 

Type System은 프로그래밍 언어의 또 다른 의미이다.

Type System은 Static Semantics (Abstract Semantics), 기존 Interpret는 Dynamic Semantics (Concrete Semantics)를 의미한다.