[프언] #11. Type System

2023-2학기/프로그래밍언어

[프언] #11. Type System

AlriC 2023. 12. 4. 20:57

Safe / Unsafe

소스 코드를 받아 그 코드를 실행하는 프로그램, 혹은 환경을 Interpreter, 인터프리터라고 부릅니다.

지금까지 저희가 개발한 프로그래밍 언어는 소스 코드를 인터프리터에 넣었을 때 정상적으로 실행될지, 실행에 실패할지 판단할 수 있는 능력이 없습니다. 인터프리터가 실행할 수 없는 소스 코드를 Unsafe Program이라고 합니다.

예를 들어, 아래와 같은 프로그램들은 전부 Unsafe Program입니다.

if 3 then 88 else 99

위 프로그램은 3이 Boolean이 아니기 때문에 실행될 수 없습니다.

Let x = iszero 0
in (3 - x)

위 프로그램은 - 기호가 Boolean에 대해 정의되어 있지 않기 때문에 실행될 수 없습니다.

어떤 프로그램이 Safe한지 Unsafe 한 지를 자동적으로 판단할 수 있는 메커니즘, 혹은 프로그램을 Analyzer라 부릅니다.

Sound Analyzer Vs. Complete Analyzer

Analyzer는 아래의 2가지 특징을 가집니다.

Static : 프로그램을 직접 실행하지 않음
Automatic : 사람의 개입이 없음

여기서 재미있는 사실을 하나 말씀드리겠습니다. 어떤 프로그램이 실행될 수 있는지 없는지를 판단하는 문제를 Halting Problem이라고 부릅니다. 그리고 이 Halting Program은 해결 불가능함이 이미 증명되어 있습니다.

이 말은 어떤 프로그램에 에러가 있는지, 없는지를 완벽하게 판단할 수 있는 Analyzer는 존재할 수 없다는 말과 같습니다. 그래서 Analyzer는 아래 2가지 특성 중 하나만을 가지는데요.

만약 Analyzer가 에러가 없음을 증명할 수 있다면, 이 Analyzer는 Sound 합니다. 만약 Sound 한 Analyzer가 프로그램을 Accept 하면, 이 프로그램에는 에러가 없음을 확신할 수 있습니다. 그러나, 프로그램을 Reject 한다고 해서 이 프로그램에 에러가 있다는 확신은 할 수 없습니다. 즉, Safe Program도 Reject되는 한계점이 존재합니다.

반대로 만약 Analyzer가 에러가 있음을 증명할 수 있다면, 이 Analyzer는 Complete 합니다. 만약 Complete 한 Analyer가 프로그램을 Reject 한다면, 이 프로그램에는 에러가 있음을 확신할 수 있습니다. 그러나, 프로그램을 Accept 한다고 해서 이 프로그램에 에러가 없다는 확신은 할 수 없습니다.

일단 저희는 Sound한 Analyzer에 대해 먼저 생각해 보겠습니다. 이런 Analyzer는 프로그램을 받아 프로그램을 이루는 요소들의 Type을 체크합니다. 예컨대, 아래와 같은 프로그램이 있다고 생각합시다.

if A then B else C

(A, B, C는 Expression입니다.)

Analyzer가 하는 일은 A의 Type을 확인하는 것입니다. 그래서 A의 Type이 Boolean이면 패스, 그 외의 타입이면 Reject하는 방식이죠. 이렇게 작동하는 프로그램을 Type Checker라고 부릅니다.

이 Type Checker는 Sound한 Analyzer입니다. Type Error가 있는 프로그램은 절대 Accpet 되지 않기 때문이죠. 반면, Complete하진 않습니다. Type Error가 있어도 정상적으로 실행되는 프로그램이 있을 가능성이 있기 때문이죠.

Type System

이때까지 저희가 만들어왔던, 위 프로그래밍 언어에 대한 Type System을 이제 직접 만들어보겠습니다.

먼저 저희 언어에는 총 3가지 Type이 있습니다. Int, Bool, Proc 입니다. 그리고 Proc Type은 또 어떤 Type을 받아 어떤 Type을 리턴하는지에 따라 구분이 가능합니다.

Type Checker를 만들기 위해, 저희는 각 Expression의 Type을 계산해야 합니다. 그래야 어떤 위치에 올바른 Type이 들어갔는지를 확인할 수 있으니깐요.

if (iszero x) then 88 else 99

예시로, 위 코드의 Type Checking을 위해서는 먼저 Expression "iszero x"의 Type이 무엇인지를 알아내야겠죠. 이를 위해 저희는 각 Variable이 어떤 Type인지 기억해 둘 필요가 있습니다. 이 과정을 수행하는 것이 Type Environment입니다.

$$\tau = Var\to T$$

Type Environment는 일반적인 Environment와 같은 형식으로 정의됩니다. 만약 $\tau \vdash e:t$라고 썼다면, 이것은 Expression $e$가 $t$의 Type을 가지고 있음을 의미합니다.