[Programming Languages #3] 타입 시스템: 프로그램이 안전하다는 것을 어떻게 보장할까?
Programming Languages 시리즈 3편 – 타입 시스템이 무엇인지, 그리고 프로그램의 안전성을 어떻게 보장하는지 이해하기
타입 시스템이란 무엇인가
앞에서 우리는 프로그램의 의미를 정의하는 방법을 봤다.
- Evaluation Relation
- Derivation
- 프로그램 실행 = 규칙 적용
이제 한 가지 중요한 질문이 남는다.
“이 프로그램, 실행해도 괜찮은가?”
실행 이전의 문제
지금까지의 관점에서는
프로그램을 “실행하면 무엇이 되는가”에 집중했다.
하지만 이 접근에는 한 가지 문제가 있다.
잘못된 프로그램도 실행 단계까지 가야 오류를 알 수 있다
예시
다음 프로그램을 보자.
1
1 + true
이건 Syntax적으로는 문제가 없다.
하지만 실행하려고 하면 문제가 생긴다.
- 숫자 + 불리언
- 정의되지 않은 연산
즉,
실행 중(runtime)에 오류가 발생한다
핵심 아이디어
그래서 등장하는 것이 바로 타입 시스템이다.
“실행하기 전에 문제를 잡자”
타입 시스템의 역할
타입 시스템은 프로그램을 실행하기 전에
다음 질문을 한다.
“이 프로그램은 타입적으로 올바른가?”
이를 수식으로 표현하면 다음과 같다.
\[\Gamma \vdash e : t\]이 식의 의미
이 식은 이렇게 읽는다.
“타입 환경 \(\Gamma\)에서, 프로그램 \(e\)는 타입 \(t\)를 가진다”
Execution vs Type System
이제 두 가지 관점이 생긴다.
| 관점 | 의미 |
|---|---|
| Evaluation | 프로그램을 실행해서 값을 얻는다 |
| Type System | 프로그램이 안전한지 검사한다 |
중요한 직관
여기서 꼭 가져가야 할 감각은 이것이다.
타입 시스템은 실행을 “막기 위한” 것이 아니라
잘못된 실행을 “미리 차단하는 것”이다
왜 중요한가
이 개념이 중요한 이유는 명확하다.
- runtime error를 줄일 수 있고
- 프로그램의 성질을 미리 보장할 수 있으며
- 자동 검증이 가능해진다
즉,
프로그램을 더 안전하게 만들기 위한 핵심 도구
다.
한 줄 정리
\[\text{Type System} = \text{프로그램의 안전성을 실행 전에 검사하는 시스템}\]타입 환경 (Γ)
앞에서 우리는 다음과 같은 식을 봤다.
\[\Gamma \vdash e : t\]여기서
“Γ (Gamma)가 무엇일까?”
핵심 아이디어
Γ는 한 문장으로 정의된다.
“변수들의 타입을 기록해두는 환경”
즉,
- 변수 → 타입
- 이름 → 정보
를 저장하는 일종의 테이블이다.
왜 필요한가
프로그램을 다시 보자.
1
x + 1
이 식에서 우리는 이런 질문을 해야 한다.
- \(x\)는 int인가?
- 아니면 bool인가?
이걸 모르면 타입을 판단할 수 없다.
그래서 Γ가 필요하다.
예시
다음과 같은 환경이 있다고 하자.
\[\Gamma = \{ x : int \}\]이제 우리는 말할 수 있다.
\[\Gamma \vdash x : int\]즉,
“환경 Γ에서는 x가 int 타입이다”
환경은 어떻게 확장되는가
프로그램을 보면 새로운 변수가 계속 등장한다.
예를 들어:
1
let x = 1 in x + 2
이 경우, 타입 검사 과정은 이렇게 진행된다.
1) x의 타입을 결정
\[1 : int\]2) 환경 확장
\[\Gamma' = \Gamma \cup \{ x : int \}\]3) 확장된 환경에서 검사
\[\Gamma' \vdash x + 2 : int\]중요한 감각
여기서 핵심은 이것이다.
타입 검사는 “환경을 따라가면서” 진행된다
즉,
- 프로그램을 내려가면서
- 환경을 확장하고
- 그 환경에서 판단한다
Evaluation과의 차이
이 개념은 앞에서 본 environment (ρ)와 비슷하다.
하지만 역할이 다르다.
| 기호 | 역할 |
|---|---|
| \(\rho\) | 변수 → 값 |
| \(\Gamma\) | 변수 → 타입 |
핵심 차이
- \(\rho\) → 실행할 때 사용
- \(\Gamma\) → 타입 검사할 때 사용
즉,
하나는 값, 하나는 타입
왜 중요한가
이 개념이 중요한 이유는 단순하다.
모든 typing rule은 이 Γ를 기반으로 정의된다.
즉,
타입 시스템 전체의 “기반 구조”
다.
한 줄 정리
\[\Gamma = \text{변수의 타입을 저장하는 환경}\]Typing Relation — 프로그램에 타입을 부여하는 규칙
앞에서 우리는 타입 시스템을 이렇게 표현했다.
\[\Gamma \vdash e : t\]이 식을 이제 정확하게 이해할 차례다.
이 식의 의미
이 식은 다음과 같이 읽는다.
“환경 \(\Gamma\)에서, 프로그램 \(e\)는 타입 \(t\)를 가진다”
구성 요소 다시 보기
- \(\Gamma\) : 타입 환경 (변수 → 타입)
- \(e\) : 프로그램 (expression)
- \(t\) : 타입 (int, bool, function 등)
핵심 관점
여기서 중요한 포인트는 이것이다.
이건 단순한 계산 결과가 아니라 “판단(judgment)”이다
즉,
- Evaluation → 값을 계산
- Typing → 타입을 판단
Evaluation과 비교
앞에서 본 식과 비교해보자.
Evaluation
\[\rho \vdash e \Rightarrow v\]→ 실제로 실행해서 값을 얻는다
Typing
\[\Gamma \vdash e : t\]→ 실행하지 않고 타입을 판단한다
중요한 차이
| 구분 | 의미 |
|---|---|
| Evaluation | 실행 결과 |
| Typing Relation | 타입 판단 |
왜 “Relation”인가
여기서 “Relation”이라는 단어가 중요하다.
타입은 계산되는 것이 아니라 “정의되는 것”이다
즉,
- 함수처럼 계산하는 것이 아니라
- 규칙 집합으로 정의된다
직관적으로 보면
이걸 이렇게 생각하면 쉽다.
“이 프로그램은 int인가?”
이 질문에 대해
타입 시스템은 Yes / No를 판단한다.
예시
다음 프로그램을 보자.
1
1 + 2
우리는 다음을 말할 수 있다.
\[\Gamma \vdash 1 + 2 : int\]또 다른 예:
1
1 + true
이 경우에는:
\[\Gamma \nvdash 1 + true : int\]즉,
타입 시스템이 거부한다
중요한 감각
여기서 꼭 가져가야 할 핵심은 이것이다.
Typing Relation은 프로그램의 “타입 가능성”을 정의한다
즉,
- 타입이 맞으면 → accept
- 타입이 틀리면 → reject
왜 중요한가
이 개념이 중요한 이유는 명확하다.
이제 우리는:
- 프로그램이 실행되기 전에
- 문제가 있는지 판단할 수 있다
즉,
정적 검증 (static checking) 이 가능해진다
한 줄 정리
\[\Gamma \vdash e : t = \text{프로그램 e가 타입 t를 가진다는 판단}\]Typing Rules — 타입 시스템은 규칙이다
앞에서 우리는 다음을 봤다.
\[\Gamma \vdash e : t\]그리고 이것이 단순한 계산이 아니라
판단 (judgment) 이라는 것도 확인했다.
이제 중요한 질문이 남는다.
“이 판단은 어떻게 만들어지는가?”
그 답이 바로 Typing Rules다.
핵심 아이디어
Typing Rule은 한 문장으로 정리된다.
“어떤 프로그램이 어떤 타입을 가지는지 정의하는 규칙”
형태
Typing Rule은 항상 이런 형태를 가진다.
\[\frac{\text{premises}}{\text{conclusion}}\]의미는 간단하다.
위가 성립하면 아래도 성립한다
가장 기본적인 규칙들
이제 실제 규칙을 보자.
숫자
\[\frac{}{\Gamma \vdash n : int}\]의미
숫자는 항상 int 타입이다
변수
\[\frac{x : t \in \Gamma}{\Gamma \vdash x : t}\]의미
변수의 타입은 환경에서 가져온다
덧셈
\[\frac{ \Gamma \vdash e_1 : int \quad \Gamma \vdash e_2 : int }{ \Gamma \vdash e_1 + e_2 : int }\]의미
두 값이 모두 int일 때만 덧셈이 가능하다
중요한 감각
여기서 핵심은 이것이다.
타입은 “구조를 따라” 결정된다
즉,
- 작은 식부터 타입을 정하고
- 그걸 이용해서 큰 식의 타입을 결정한다
Derivation Tree (타입 버전)
이 규칙들도 트리로 표현할 수 있다.
예를 들어:
1
x + 1
환경:
\[\Gamma = \{ x : int \}\]이걸 트리로 보면:
1
2
3
Γ ⊢ x + 1 : int
/ \
Γ ⊢ x : int Γ ⊢ 1 : int
이 트리가 의미하는 것
이건 단순한 구조가 아니다.
“이 프로그램이 타입적으로 올바르다는 증명”
실행과의 연결
여기서 중요한 연결이 나온다.
- Evaluation → 실행 과정의 derivation
- Typing → 타입 판단의 derivation
즉,
타입 검사도 하나의 “증명 과정”이다
왜 중요한가
이 방식이 중요한 이유는 단순하다.
이제 우리는:
- 타입 시스템을 정확하게 정의할 수 있고
- 자동으로 타입 검사기를 만들 수 있으며
- 프로그램의 성질을 증명할 수 있다
한 줄 정리
\[\text{Typing Rules} = \text{프로그램의 타입을 정의하는 inference rule 집합}\]타입 시스템은 왜 중요한가 — 프로그램의 안전성 보장
지금까지 우리는 타입 시스템을 이렇게 정의했다.
- \[\Gamma \vdash e : t\]
- Typing Rules = 규칙 집합
- 타입 검사 = derivation 과정
이제 마지막 질문이다.
“그래서 타입 시스템이 왜 중요한가?”
핵심 역할
타입 시스템의 역할은 한 문장으로 정리된다.
“잘못된 프로그램을 실행 전에 걸러내는 것”
실행 관점에서 다시 보면
우리가 이미 본 것:
\[\rho \vdash e \Rightarrow v\]이건 프로그램을 실제로 실행하는 과정이다.
하지만 이 과정에는 문제가 있다.
잘못된 프로그램도 실행을 시도한다
예시
1
1 + true
이 프로그램은:
- Syntax ✔️
- 실행 ❌ (runtime error)
타입 시스템이 개입하면
타입 시스템은 실행 전에 판단한다.
\[\Gamma \nvdash 1 + true : int\]즉,
애초에 실행 자체를 막는다
핵심 직관
여기서 가장 중요한 감각은 이것이다.
“실행 전에 오류를 제거한다”
더 깊은 의미 (중요)
타입 시스템은 단순한 필터가 아니다.
이론적으로는 이렇게 말할 수 있다.
“타입이 맞는 프로그램은 실행해도 안전하다”
이걸 formal하게 표현하면:
- Progress: 잘 타입된 프로그램은 멈추지 않는다
- Preservation: 실행해도 타입이 유지된다
직관적으로 보면
- Progress → “이상한 상태에 빠지지 않는다”
- Preservation → “타입이 깨지지 않는다”
한 문장으로 요약하면
“잘 타입된 프로그램은 runtime error를 일으키지 않는다”
왜 중요한가
이 성질 덕분에 우리는:
- 프로그램의 안전성을 보장할 수 있고
- 컴파일 단계에서 오류를 잡을 수 있으며
- 대규모 시스템을 신뢰할 수 있다
지금까지의 흐름 정리
이번 글에서 한 것은 다음과 같다.
- 타입 시스템이 무엇인지
- Γ (타입 환경)
- Typing Relation
- Typing Rules
- 그리고 안전성
전체 흐름에서의 위치
이제 우리는 다음을 모두 갖게 되었다.
- Syntax → 프로그램의 구조
- Semantics → 프로그램의 의미
- Type System → 프로그램의 안전성
다음 단계
이제 자연스럽게 다음 질문이 나온다.
“이 타입은 어떻게 자동으로 계산할 수 있을까?”
다음 글에서는:
- Type Inference (타입 추론)
- Unification
- 자동 타입 시스템
을 다룬다.