타입은 어떻게 증명이 되는가 — TypeScript 타입 시스템과 Curry–Howard 대응

요약:

• TypeScript의 타입 시스템을 단순한 정적 타입 검사기가 아니라 논리학의 증명 시스템으로 해석하는 관점을 제시합니다.
• Curry–Howard 대응(Type = Proposition, Program = Proof)을 기반으로, 타입 추론이 가능한 이유를 개념적으로 설명합니다.
• 함수 타입, 제네릭, 조건부 타입, 타입 좁히기 등의 TypeScript 기능을 논리적 함의, 보편 양화, 경우 분석에 대응시켜 설명합니다.
• 타입 체크 과정을 규칙 적용이 아닌 명제 간 관계를 검증하는 과정으로 해석합니다.
• 구현 디테일보다는 TypeScript 타입 시스템의 설계 배경과 수학적 구조에 초점을 둡니다.

상세요약:

1. 배경: 타입 추론은 왜 가능한가?
   정적 타입 언어에서 타입 추론은 “컴파일러가 어떻게 타입을 맞춰보는가”라는 구현 문제로 자주 설명됩니다.
   이 글은 그보다 한 단계 뒤로 물러나, 타입 추론이 원천적으로 가능한 이유를 묻습니다.
   그 답으로 타입 시스템을 논리학의 증명 시스템으로 바라보는 관점을 제시합니다.

2. 이론적 기반: Curry–Howard 대응
   Curry–Howard 대응에 따르면 타입(Type)은 명제(Proposition)에 대응하고 프로그램(Program)은 그 명제의 증명(Proof)에 대응합니다.
   이 관점에서 타입 체크는 프로그램이 특정 명제를 만족하는지를 검증하는 과정으로 해석됩니다.

3. TypeScript 기능과 논리 구조의 대응
   글에서는 TypeScript의 주요 기능을 다음과 같이 연결합니다.

• 함수 타입 → 논리적 함의(Implication)
• 제네릭 → 보편 양화(Universal Quantification)
• 조건부 타입 / 타입 좁히기 → 경우 분석(Case Analysis)
  이를 통해 왜 특정 타입 표현은 자연스럽고,
  왜 어떤 타입은 구조적으로 표현하기 어려운지를 설명합니다.

4. 타입 시스템의 한계와 설계 선택
   이 관점에서 TypeScript의 제약과 한계는 “기능 부족”이 아니라 논리적 일관성을 유지하기 위한 설계 선택으로 이해됩니다.
   글은 실무 테크닉이나 트릭보다는, 타입 시스템이 어떤 철학과 수학적 배경 위에서 형성되었는지를 설명하는 데 집중합니다.