타입 시스템은 왜 증명처럼 동작하는가

타입 검사를 컴파일 통과로만 보던 시선에서, 논리로 읽는 타입 시스템까지

Jan 25, 2026

우리는 매일 타입을 사용하며, 무수한 타입 에러를 마주한다. 그때마다 에러 메시지를 읽고, 구글링해서 해결하긴 하지만 정작 “타입 시스템이 왜 이렇게 동작하는지”를 깊게 생각하며 문제를 해결하는 경우는 드물다.

타입을 쓸 줄 아는 것이 문법을 이해하는 것이라면, 타입 시스템을 이해하는 것은 그 문법이 왜 그렇게 설계되었는지에 대한 본질을 이해하는 것에 가깝다.

사실 이러한 이해를 돕기 위해 “프로그래머를 위한 카테고리 이론” 시리즈를 번역하면서 카테고리, 펑터, 합성 같은 개념을 다뤘었는데, 지금 돌아보니 진입 장벽이 꽤 높은 내용이라, 조금 더 쉬운 버전의 포스팅을 다시 작성하려고 한다.

그래서 이번 포스팅에서는 타입과 논리학의 대응 관계를 중심으로, 타입 검사기가 “통과”라고 말할 때 그것이 정확히 무엇을 의미하는지 살펴보려 한다.

타입 검사는 정말 “검사”일 뿐일까

TypeScript를 처음 배울 때 대부분의 개발자는 타입 시스템을 일종의 린터(linter)처럼 받아들인다. 마치 린터처럼 잘못된 타입을 넣으면 빨간 줄이 그어지고, 올바른 타입을 넣으면 통과하기 때문이다.

function add(a: number, b: number): number {
  return a + b;
}

// Error: Argument of type 'string' is not assignable to parameter of type 'number'
add(1, "2");

틀린 말은 아니지만 이 관점에는 한 가지 빠진 것이 있다.

타입 시스템은 단순히 에러를 잡는 도구가 아니다. 그 뒤에는 수학적 구조가 있고, 타입 검사를 통과한다는 것은 단순히 에러가 없다는 것 이상의 의미를 가진다. 타입은 논리학의 명제에 대응하고, 그 타입을 만족하는 코드는 그 명제의 증명에 대응한다.

그렇다면 우리가 마주하는 타입 에러는 무엇일까? 단순한 실수일까, 아니면 우리가 암묵적으로 맺은 어떤 계약이 깨졌다는 신호일까.

이 이야기를 이해하려면 가장 먼저 타입 시스템에 사용되는 기본적인 수학의 개념들에 대한 이야기를 해야한다.

타입 시스템의 세 기둥: 형식 논리학, 집합론, 람다 대수

타입 시스템은 세 가지 수학적 아이디어 위에 서 있다. 갑자기 수학에 대한 이야기가 나와서 어렵게 느껴질 수 있지만 걱정할 필요 없다. 이 개념들은 우리가 이미 코드로 매일 다루고 있는 것들이다.

형식 논리학: “참이다”를 증명한다는 것

형식 논리학은 $A$ 이고 $B$ 이다, $A$ 이거나 $B$ 이다, $A$ 이면 $B$ 이다 같은 논리들을 다루는 체계다. 핵심 아이디어는 “참이라고 주장하려면, 그것을 증명해야 한다는 것”이다.

기호	일상적 의미	예시
∧	그리고	“우산도 있고 장화도 있다”
∨	또는	“버스를 타거나 지하철을 탄다”
→	~하면 ~이다	“비가 오면 땅이 젖는다”

예를 들어 $A \lor B$ 가 참이라고 말하려면, $A$ 가 참임을 보여주거나, $B$ 가 참임을 보여줘야 한다. “둘 중 하나는 참이겠지만 어느 쪽인지는 몰라요”라는 식의 주장은 증명으로 인정되지 않는다.

그리고 일단 ” $A \lor B$ “를 받아들이면, 그로부터 무언가를 이끌어내기 위해서는 두 경우( $A$ , $B$ )를 모두 다루는 분기가 필요하다는 것도 알 수 있다. 이는 마치 코드에서 string | number를 다룰 때 타입 좁히기가 필요한 이유와 같은 구조다.

  // "A 또는 B"가 참이라고 주장하려면, 둘 중 하나를 구체적으로 보여줘야 한다
  type Result = string | number;

  function process(x: Result) {
    // "둘 중 하나겠지"로는 안 된다. 어떤 경우인지 확인해야 한다.
    if (typeof x === 'string') {
      return x.toUpperCase();
    } else {
      return x.toFixed(2);
    }
  }

집합론: 타입은 원소들의 모임이다

집합은 비슷한 것들을 모아놓은 주머니라고 생각하면 된다. 예를 들어 number 타입은 프로그램 상에서 표현할 수 있는 모든 숫자를 담은 주머니, string 타입은 모든 문자열을 담은 주머니이고, number | string은 이 두 주머니의 내용물을 합친 것이다.

// 숫자 주머니에서 하나 꺼냄
const n: number = 42;

// 문자열 주머니에서 하나 꺼냄
const s: string = "hello";

// 둘 중 아무 주머니에서나 꺼낸 것
const x: number | string = Math.random() > 0.5 ? 42 : "hello";

타입을 집합으로 생각하면 많은 것이 자연스러워진다. never 타입은 빈 주머니이고, unknown 타입은 세상 모든 것이 들어있는 주머니다.

물론 엄밀하게 이야기하자면 TypeScript의 실제 타입 시스템은 순수한 집합론과 다른 부분이 있지만, 이 정도 이해로도 직관을 잡기에는 충분하다.

람다 대수: 함수, 그 이상의 의미

람다 대수는 1930년대 알론조 처치(Alonzo Church)라는 수학자가 “계산이란 무엇인가?”라는 질문에 답하려고 만든 개념이다. 이름은 무시무시하게 느껴지지만, 사실 개발자라면 이미 매일 쓰고 있는 것이다.

// 람다 대수로 표현하면 λx.x
const identity = x => x;

// 람다 대수로 표현하면 λx.λy.x
const first = x => y => x;

화살표 함수는 람다( $\lambda$ ) 표기의 현대적 문법에 가깝고, 람다 대수의 핵심 아이디어인 “함수 정의와 적용”을 가장 직접적으로 보여준다. 처치가 증명한 놀라운 사실은 이 단순한 개념만으로도 사칙연산, 조건문, 반복문, 심지어 숫자 자체까지 모두 표현할 수 있다는 것이다.

물론 실제 JavaScript 함수는 부수효과, 예외, this 바인딩, 런타임 객체 모델 같은 것 때문에 람다 대수와 100% 동일하다고 말하기는 어렵다. 하지만 “계산이란 결국 함수를 만들고 적용하는 것”이라는 핵심적인 통찰은 공유하기 때문에 이 정도 이해로도 충분하다.

세 세계가 만나는 지점: Curry-Howard 대응

그렇다면 이 세 가지 개념이 타입 시스템에 어떻게 사용되고 있다는 것일까? 이 질문에 대한 답을 하려면 이 개념들을 하나로 묶어주는 Curry-Howard 대응에 대해 이야기해야한다.

Curry-Howard 대응 또는 Curry-Howard 동형이라고 불리는 개념은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계를 의미한다. 더 정확하게 말하자면 논리학의 증명 규칙과 타입 시스템의 타입 규칙이 서로 대응한다는 주장이다.

이 개념은 이미 1930년대에 하스켈 커리(Haskell Curry)라는 논리학자가 람다 대수에 타입을 붙여보다가 발견한 규칙이며, 이후 1969년 윌리엄 하워드(William Howard)가 이 발견을 더 깊이 파고들어 아래와 같은 대응 관계를 확립했다.

논리학에서	프로그래밍에서
명제	타입
증명	프로그램
A이면 B	A를 받아 B를 반환하는 함수
A 그리고 B	A와 B를 둘 다 가진 튜플/객체
A 또는 B	A이거나 B인 유니온 타입
거짓 (증명 불가능)	never (값이 존재할 수 없음)

결국 이 개념의 핵심을 한 줄로 요약해보면 아래와 같다.

타입은 명제에 대응하고, 그 타입의 값을 만드는 프로그램은 그 명제의 증명에 대응한다.

TypeScript는 실용을 위해 이 아이디어를 부분적으로 차용한 언어다. 부분적으로 차용한 언어라는 의미는 any나 타입 단언 같은 탈출구가 있기 때문이다.

그래서 이 글에서 “증명”이라는 표현은 “타입 규칙이 요구하는 계약을 충족한다” 정도로 이해하면 된다. TypeScript의 한계에 대해서는 글 끝에서 다시 이야기해보겠다.

타입으로 보는 논리적 구조

그렇다면 이 Curry-Howard 대응이 실제로 어떻게 나타나는지 하나씩 뜯어보자.

함수: “A이면 B”의 증거

먼저 가장 핵심적인 대응인 함수 타입부터 살펴보자. 함수 타입 (a: A) => B는 논리학에서 $A$ 이면 $B$ 에 해당한다.

이게 무슨 말일까? 이해를 돕기 위해 조금 더 일상적인 비유로 풀어보면 이렇다.

친구가 “네가 밀가루를 주면, 내가 빵을 만들어줄게”라고 약속했다고 하자. 이것은 “밀가루 → 빵”이라는 명제다. 그렇다면 이 약속이 진짜인지는 어떻게 확인할 수 있을까? 간단하다. 실제로 밀가루를 줬을 때 빵이 나오면 된다.

function makeBread(flour: Flour): Bread {
  // 밀가루를 반죽하고, 발효시키고, 굽는 과정을 거친 뒤...
  return bread;
}

이 함수가 타입 검사를 통과한다는 것은, “밀가루를 주면 빵을 만들 수 있다”는 약속이 타입 규칙 안에서 이행 가능함을 보여준 것이다. 함수의 구현체 자체가 그 계약의 이행인 셈이다.

그렇다면 반대로 타입 에러가 발생한다면 어떻게 되는 걸까?

function makeBread(flour: Flour): Bread {
  // Error: Type 'Flour' is not assignable to type 'Bread'
  return flour;  
}

원래 밀가루를 주면 빵을 만들어서 주기로 했는데, 뜬금없이 밀가루를 다시 돌려줬으니 이것은 계약 불이행이라고 볼 수 있고, 따라서 타입 에러가 발생한다.

또한 이 계약과 구조가 제대로 지켜지면 이제 우리는 함수의 동작 결과를 추론할 수 있게 된다.

논리학에는 전건 긍정(Modus Ponens)이라는 추론 규칙이 있는데, 간단하게 정리해보면 아래와 같다.

” $A$ 이면 $B$ 이다”가 참이고, $A$ 가 참이면, $B$ 도 참이다.

예를 들어 “비가 오면 땅이 젖는다”는 명제가 참이고 “비가 온다”라는 명제도 참이라면, 이에 따라 “땅이 젖는다”라는 명제도 참이라는 것을 손쉽게 추론할 수 있다. 이 구조는 프로그래밍에서 함수 호출과 같은 구조이기 때문에 우리는 함수의 결과 타입을 추론할 수 있게 되는 것이다.

// "밀가루 → 빵" 약속
const makeBread: (flour: Flour) => Bread = /* ... */;  

// 밀가루가 있음
const flour: Flour = getFlour();

// 따라서 빵을 얻음
const bread: Bread = makeBread(flour);

함수 makeBread는 “밀가루를 주면 빵을 만들어준다”라는 명제이다. 즉, 이 명제가 참이고 “밀가루를 준다”라는 명제도 참이라면 자연스럽게 bread 변수에 담기는 값이 Bread 타입이라는 명제도 참이 되는 것이다.

우리가 매일 하는 함수의 호출과 결과 타입의 추론은 이러한 논리적 추론과 같은 구조를 가지고 있는 것이다.

튜플: “그리고”의 증거

논리학의 ” $A$ 그리고 $B$ “는 프로그래밍의 튜플이나 객체에 해당한다.

일상적인 예로 생각해보자. 해외여행을 가려면 “여권이 있고 비행기 표도 있다”는 조건을 만족해야 한다. 이 조건을 충족하려면? 여권과 비행기 표를 둘 다 보여주면 된다.

type CanTravel = [Passport, Ticket];

// "여행 가능" 조건의 충족 = 여권과 티켓을 모두 갖춘 튜플
const proof: CanTravel = [myPassport, myTicket];

이렇게 CanTravel 타입이 만족했다면, 다른 말로 “여권도 있고 비행기 표도 있다”는 조건이 만족했다면 아래와 같이 CanTravel 타입의 튜플에서 여권이나 비행기표 모두 자유롭게 꺼내올 수 있다.

function getPassport(travel: CanTravel): Passport {
  // "A 그리고 B"에서 A를 꺼냄
  return travel[0];
}

function getTicket(travel: CanTravel): Ticket {
  // "A 그리고 B"에서 B를 꺼냄
  return travel[1];
}

이것은 논리학에서 ” $A \land B$ 가 참이면 $A$ 도 참이다”라는 규칙과 같은 구조다. 튜플에서 요소를 꺼내는 것이 논리적 추론과 대응되는 셈이다.

유니온: “또는”의 증거

TypeScript의 유니온 타입 A | B는 논리학의 ” $A$ 또는 $B$ “에 해당한다. 여기서 중요한 점은 우리가 ” $A$ 또는 $B$ “가 참이라고 주장하려면 반드시 $A$ 가 참이라는 사실을 보여주거나, $B$ 가 참이라는 사실을 보여줘야 한다는 것이다. 두 논리 중 하나를 구체적으로 제시해야한다.

type PaymentMethod = CreditCard | BankTransfer;

// "신용카드 또는 계좌이체"의 충족 = 둘 중 하나를 구체적으로 제시
const payment1: PaymentMethod = { type: 'credit', cardNumber: '1234...' };
const payment2: PaymentMethod = { type: 'bank', accountNumber: '5678...' };

또한 ” $A$ 또는 $B$ “라는 명제가 참이라고 해도 $A$ 와 $B$ 둘 중 뭐가 참인지 구체적으로 확인하기 전까지는 알 수가 없다는 것과 같다.

그래서 이 명제로부터 다른 무언가를 이끌어내려면 $A$ 와 $B$ 에 대한 처리를 모두 해줘야한다.

function processPayment(method: PaymentMethod): Receipt {
  if (method.type === 'credit') {
    // A인 경우 처리
    return chargeCreditCard(method);
  } else {
    // B인 경우 처리
    return processBankTransfer(method);
  }
}

이것이 TypeScript에서 Exhaustiveness check가 중요한 이유다. 논리적으로 ” $A$ 또는 $B$ “를 다룰 때는 두 경우 모두에 대한 전략이 있어야만 완전한 처리가 되기 때문이다.

다만 TypeScript가 모든 케이스를 다뤘는지 자동으로 체크해주는 것은 설정과 코드 패턴에 따라 달라진다. 그러니 확실하게 Exhaustiveness check를 강제하고 싶다면 아래와 같은 패턴을 사용하는 것이 좋다.

function assertNever(x: never): never {
  throw new Error("Unexpected value");
}

type Shape = { type: 'circle'; radius: number }
  | { type: 'square'; side: number }
  | { type: 'triangle'; height: number };

function area(shape: Shape): number {
  switch (shape.type) {
    case 'circle':
      return Math.PI * shape.radius ** 2;
    case 'square':
      return shape.side ** 2;
    default:
      // Argument of type '{ type: "triangle"; height: number; }' is not assignable to parameter of type 'never'.
      return assertNever(shape);
  }
}

기본적으로 유니온 타입의 모든 케이스를 처리했다면 default에 도달할 일이 없고, shape는 never 타입이 된다. 하지만 만약 새로운 도형을 추가했는데 처리를 깜빡했다면, shape가 never 타입이 아니게 되고 컴파일 에러가 발생한다.

never: “불가능”의 표현

TypeScript의 never 타입은 “이런 값은 존재할 수 없다”를 의미한다. 논리학에서는 이것을 모순 또는 거짓이라고 표현한다.

앞서 언급했던 집합론으로 비유하자면, never 타입은 빈 주머니다. 즉, never라는 주머니 안에는 아무것도 없고, 앞으로도 없을 것이다.

function throwError(message: string): never {
  throw new Error(message);
  // 이 함수는 정상적으로 반환되지 않는다
  // 반환값이 "존재할 수 없다"
}

여기서 논리학의 재미있는 원리 하나가 나온다. 바로 “모순으로부터는 무엇이든 도출할 수 있다”는 것이다. 이는 라틴어로 “Ex falso quodlibet”이라고 하는데, 쉽게 말하면 불가능한 상황이 발생했다면, 그 다음에는 뭐든지 가능하다는 것이다.

이 원리는 타입스크립트에서 아래와 같은 함수를 선언해봄으로써 구현해볼 수 있다.

function absurd<T>(x: never): T {
  return x;  // never에서는 어떤 타입으로든 변환 가능
}

이 함수는 ”never이면 T이다”라는 규칙을 표현하고 있다. 한번 never 타입을 다른 구체적인 타입으로 바꿔보면 바로 에러가 발생하는 것을 알 수 있다. never는 거짓, 모순이기 때문이 그 다음에는 어떤 타입이 오든 논리적으로 틀린 것이 아닌 것이다.

사실 이 부분도 정확하게 뜯어보면 TypeScript가 Ex falso을 정확하게 구현한 것은 아니긴 하다.

never 타입은 모든 타입의 서브 타입으로 취급되는 바닥 타입(Bottom Type)이기 때문에, never 타입의 값은 어떤 타입 위치에도 대입 가능한 것으로 간주된다. 논리학의 Ex falso 원리와 닮긴 했지만 실제로는 서브타이핑의 결과라고 볼 수 있다.

제네릭: “모든 경우에 통하는” 계약

우리는 제네릭을 처음 배울 때 보통 “타입을 나중에 정하는 것”이라고 배운다. 사실 이것도 틀린 말은 아니지만, 제네릭이 의미하는 바는 더 심오하다.

논리학에는 전칭 명제라는 것이 있는데, 이는 “모든 $x$ 에 대해 $P(x)$ 가 성립한다”는 형태의 명제다. 예를 들어 “모든 사람은 죽는다”처럼 말이다.

그리고 제네릭 함수는 바로 이 전칭 명제와 비슷한 구조를 가진다.

function identity<T>(x: T): T {
  return x;
}

이 함수는 “모든 타입 T에 대해, T를 주면 T를 돌려줄 수 있다”는 계약을 표현한다.

여기서 중요한 것은 “모든 경우”에 대해 성립함을 보여야한다는 점인데, 이게 가능하려면 어떠한 특정 경우에 대한 가정도 하면 안된다.

그래서 우리가 제네릭 타입을 사용했을 때 아래와 같은 가정을 하면 바로 타입 에러가 발생하는 것이다.

function broken<T>(x: T): T {
  // 모든 T가 number임을 가정하면...
  // Operator '+' cannot be applied to types 'T' and 'number'.
  return x + 1;
}

위와 같이 T가 number라고 가정하는 순간, 이것은 더 이상 모든 T에 대한 계약이 아니라, number에 대한 계약으로 범위가 좁아져 버린다. 더이상 전칭 명제라고 보기 어려운 것이다.

그래서 우리는 “모든” 이라는 전제에 제약을 추가함으로서 이 문제를 해결할 수 있다.

function addOne<T extends number>(x: T): number {
  return x + 1;  // OK
}

위와 같이 T가 number를 상속받았다면 자연스럽게 T는 이제 ”number의 부분 집합인 T“로 개념이 변경된다. 즉, “모든” 이라는 개념의 범위를 조정하는 제약을 거는 것이다. 그래서 우리는 이런 제약을 걸때 extends라는 상속 키워드를 사용한다.

합성과 변환

지금까지는 타입과 논리학의 기본적인 대응 관계를 살펴봤다. 이제부터는 이것들을 조합하고 변환하는 방법에 대해서 이야기해보도록 하자.

함수 합성: 추론을 연결하기

논리학에는 삼단논법이라는 것이 있다. 가장 기본적인 정언적 삼단논법은 “만약 $A$ 가 $B$ 이고, $B$ 가 $C$ 라면, $A$ 는 $C$ 이다”로 표현할 수 있다.

이러한 삼단논법은 가정을 기반으로 한 가언적 삼단논법으로 표현할 수도 있는데, 이 경우 아래와 같은 명제가 된다.

$A$ 이면 $B$ 이다. $B$ 이면 $C$ 이다. 그러므로 $A$ 이면 $C$ 이다.

예를 들어 “밥을 먹으면 배부르다”라는 명제가 참이고, “배부르면 잠이온다”라는 명제가 참이라면, “밥을 먹으면 잠이 온다”라는 명제도 참이라는 것이다. 그리고 이것이 프로그래밍에서는 함수의 합성으로 표현된다.

function compose<A, B, C>(
  f: (a: A) => B,
  g: (b: B) => C
): (a: A) => C {
  return (a) => g(f(a));
}

const parseNumber = (s: string): number => parseInt(s, 10);
const isPositive = (n: number): boolean => n > 0;

// string → number와
// number → boolean을 연결하면
// string → boolean이 된다
const isPositiveString = compose(parseNumber, isPositive);

isPositiveString("42"); // true

이는 마치 작은 추론들을 연결해서 더 크고 복잡한 추론을 만드는 것과 동일한데, 이렇게 작고 간단한 구조를 쌓아나가며 큰 구조를 만들 수 있다는 점이 함수 합성이 강력한 이유이다.

그래서 함수형 프로그래밍에서는 pipe나 compose와 같은 개념이나 펑터(Functor)나 모나드(Monad)와 같이 함수의 합성과 관련된 개념들이 핵심이 된다.

사실 카테고리 이론에서는 이 합성이야말로 카테고리의 본질이라고 말한다. 만약 관심이 있다면 “프로그래머를 위한 카테고리 이론 - 1. 카테고리: 합성의 본질”도 참고해보자.

커링: 논리적으로 자연스러운 변환

커링(Currying)은 여러 인자를 받는 함수를 한 인자씩 받는 함수의 체인으로 바꾸는 패턴을 의미한다. 커링을 사용하면 어떤 함수든 단항 함수라는 공통의 패턴으로 만들 수 있기 때문에 합성하기가 편해진다는 장점이 있다.

한 가지 재미있는 점은 다항 함수를 단항 함수의 합성으로 변환하는 것이 항상 가능하다는 점이다. 왜 이 변환이 항상 가능한 것일까?

논리학에는 수출 법칙(Exportation)이라는 동치 관계가 있는데, 커링은 바로 이 개념을 활용한 패턴이다.

$(A \land B) \rightarrow C \equiv A \rightarrow (B \rightarrow C)$

“(A 그리고 B)이면 C이다”와 “A이면 (B이면 C이다)“는 논리적으로 동치다.

엄밀히 말하면 $(A \land B) \rightarrow C$ 는 ” $A$ 와 $B$ 를 튜플로 받아 $C$ 를 반환하는 함수”에 대응하며, JavaScript의 다중 인자 함수는 이를 실용적으로 근사한 형태라고 이해하는 것이 정확하다.

조금 더 일상적인 상황을 예를 들어 보면, “밀가루와 물이 있으면 반죽을 만들 수 있다”라는 명제와 “밀가루가 있으면, (물이 있으면 반죽을 만들 수 있다)“라는 명제는 같은 의미를 가진다는 것이다. 그래서 이 변환은 항상 안전하게 진행된다는 것이 보장된다.

// 두 인자를 한번에 받음
function makeDough(flour: Flour, water: Water): Dough {
  return mix(flour, water);
}

// 한 인자씩 받음 (커링)
function makeDoughCurried(flour: Flour): (water: Water) => Dough {
  return (water) => mix(flour, water);
}

// 둘은 논리적으로 동등하다
const dough1 = makeDough(flour, water);
const dough2 = makeDoughCurried(flour)(water);

즉, 다항 함수를 단항 함수로 변경하는 커링이 가능한 이유는 단순한 프로그래밍 기법이 아니라 논리적 동치 관계와 닮아있기 때문이다.

타입 대수: 덧셈과 곱셈처럼

혹시 대수적 데이터 타입(Algebraic Data Type)이라는 말을 들어본 적이 있는가? 이 말은 타입에도 대수학에서의 사칙연산과 같은 연산 법칙들을 적용할 수 있다는 것이다.

예를 들어 곱 타입과 합 타입이 있는데, 대표적인 곱 타입은 위에서 한번 언급했던 “그리고”를 의미하는 튜플, 그리고 합 타입은 “또는”을 의미하는 유니언 타입이 있다.

type Bool = true | false;  // 2가지 값
type Pair = [Bool, Bool];  // 2 * 2 = 4가지 값
// [true, true], [true, false], [false, true], [false, false]

type Three = 'a' | 'b' | 'c';  // 3가지 값
type Five = Three | Bool;       // 3 + 2 = 5가지 값
// 'a', 'b', 'c', true, false

이것이 대수적 데이터 타입(Algebraic Data Types)이라는 이름이 붙은 이유다. 타입을 값의 경우의 수 관점에서 바라보면 합 타입은 덧셈처럼, 그리고 곱 타입은 곱셈처럼 동작한다.

더 흥미로운 점은 대수학에서처럼 타입에서도 분배법칙이 등장한다는 것이다. 수학적으로는 다음과 같은 관계가 성립한다.

$A \times (B + C) \equiv (A \times B) + (A \times C)$

TypeScript에서도 이 구조는 특정 지점에서 매우 명확하게 드러난다. 바로 조건부 타입(Conditional Type) 이다.

TypeScript의 조건부 타입은 유니온 타입에 대해 자동으로 분배(distribute)된다. 이 성질을 이용하면 타입 대수의 분배법칙을 직접 확인할 수 있다.

type PairWith<A, B> = B extends any ? [A, B] : never;

type A = string;
type B = number | boolean;

// boolean = true | false이기 때문에 3가지 곱의 합으로 분배된다
// [string, number] | [string, false] | [string, true]
type Result = PairWith<A, B>;

위 예시는 B가 number | boolean이라는 합 타입일 때, [A, B]라는 곱타입은 다시 [A, number] | [A, boolean]이라는 합 타입으로 분배될 수 있음을 보여준다.

즉, 타입 레벨에서도 대수의 분배 법칙과 동일하게 $A \times (B + C) \equiv (A \times B) + (A \times C)$ 의 모습이 보여지는 것이다.

물론 TypeScript의 타입 시스템은 이러한 분배 구조를 항상 자동으로 동일한 타입으로 취급하지는 않는다. 하지만 최소한 타입을 계산하고 변환하는 규칙의 수준에서는 대수적 데이터 타입의 덧셈, 곱셈, 분배라는 아이디어가 분명하게 살아있다고 볼 수 있다.

카테고리 이론에서는 이 곱과 합을 보편적 구성(Universal Construction)이라는 더 추상적인 관점에서 다룬다. “프로그래머를 위한 카테고리 이론 - 9. 함수 타입”에서 이 대수적 구조가 어떻게 확장되는지 볼 수 있다.

TypeScript는 100% 논리적이지 않다

기본적인 개념들에 대해서 살펴봤다면, 이제는 필자가 위에서 언급했던 TypeScript의 한계에 대해 한번 알아보자.

필자는 TypeScript가 Curry-Howard 대응을 부분적으로 차용한 언어라고 했는데, 그 한계가 뭘까?

TypeScript는 언어의 실용성을 높이기 위해 의도적으로 논리적 모순을 초래할 수 있는 몇 가지 탈출구를 제공한다. 이 포스팅에서는 그 중 대표적인 두 가지에 대해서 이야기해보려 한다.

첫 번째 탈출구는 any와 타입 단언의 존재이다. any는 어떤 타입이든 검사하지 않고 통과시키겠다는 선언이다. 즉, 논리학적으로 보면 “검증 없이 뭐든 참으로 인정”하는 것과 같다. as를 통한 타입 단언도 마찬가지다.

이것들은 증명 체계를 우회하는 탈출구이고, 이로 인해 TypeScript는 논리적인 모순을 허용하는 언어가 되어버렸다.

const x: any = "hello";
const y: number = x; // number 타입에 문자열 할당

const z = "hello" as unknown as number;  // 타입 강제 변환

두 번째 탈출구는 바로 구조적 타이핑의 코너 케이스들이다. 대표적으로는 함수 파라미터의 이변성(Bivariance), 인덱스 시그니처, 옵셔널 프로퍼티 등의 탈출구로 인해 논리적 해석이 흔들리는 경우가 존재한다.

논리적으로 함수 파라미터는 반공변(Contravariant)적이어야 한다. 쉽게 말해 Dog가 Animal의 서브타입이라면, (animal: Animal) => void가 (dog: Dog) => void의 서브타입이어야 한다는 것이다. 이는 더 넓은 타입을 받는 함수가 더 좁은 타입을 받는 함수를 대체할 수 있기 때문이다.

하지만 TypeScript는 메소드 문법으로 선언된 함수에서 이를 이변적으로 처리한다.

  interface Animal { name: string }
  interface Dog extends Animal { breed: string }

  type Handler = { handle(animal: Animal): void };

  const dogHandler: Handler = {
    // Dog만 처리하는 함수인데 Animal을 받는 자리에 할당됨
    // strictFunctionTypes로도 잡히지 않음
    handle(dog: Dog) { console.log(dog.breed) }
  };

  dogHandler.handle({ name: "cat" }); // 런타임 에러 가능

그리고 인덱스 시그니처 또한 논리적인 모순을 초래할 수 있다. 객체에서 존재하지 않는 키에 접근하더라도 TypeScript는 undefined가 아닌 선언된 타입으로 추론하기 때문이다.

const scores: { [name: string]: number } = { alice: 100 };

const bobScore = scores["bob"]; // 타입은 number, 실제 값은 undefined
console.log(bobScore.toFixed(2)); // 런타임 에러

조금 더 엄밀한 타입 체를 원한다면 tsconfig의 noUncheckedIndexedAccess 옵션을 활성화하면 제대로 number | undefined로 추론되도록 만들 수 있다.

마지막으로 옵셔널 프로퍼티와 undefined의 혼동도 문제가 된다. 예를 들어 { a?: string }이라는 타입에서 a가 undefined인 상태와 아예 존재하지 않는 것이 논리적으로 구분되지 않는다.

type Config = { timeout?: number };

const config1: Config = { timeout: undefined }; // OK
const config2: Config = {}; // OK

// 둘 다 같은 타입으로 취급되지만,
// Object.hasOwn(config1, 'timeout')과 Object.hasOwn(config2, 'timeout')은 다르다

이 부분 또한 TypeScript 4.4 이후 도입된 exactOptionalPropertyTypes 옵션을 사용하면 “존재하지 않음”과 ”undefined로 존재함”을 더 엄밀하게 구분할 수 있다.

이런 탈출구들은 TypeScript가 100% 논리적인 정합성보다는 실용적으로 JavaScript와의 호환성을 선택한 결과라고 볼 수 있다.

마치며

이 글은 타입스크립트를 잘 쓰는 방법을 설명하려는 글은 아니다. 이미 실무에서 타입을 충분히 다뤄본 사람이라면, 여기서 등장하는 대부분의 예시는 익숙할 수도 있다.

다만 필자가 이 글을 통해 전하고 싶었던 건, 타입 시스템을 대하는 관점에 가깝다. 타입 에러를 “통과시켜야 할 장애물”로 보는 대신, 내가 어떤 계약을 선언했고, 그 계약이 어디에서 깨지고 있는지를 읽어내는 도구로 바라보는 시선 말이다.

이 관점이 한 번 자리 잡히면, 타입 에러를 대하는 태도도 자연스럽게 달라진다. 왜 안 되는지를 묻기 전에, 무슨 계약을 어기고 있는지를 먼저 떠올리게 된다.

타입 시스템은 생각보다 많은 이야기를 하고 있다. 다만 그걸 단순한 컴파일 통과 여부로만 읽고 지나치기엔, 조금 아까운 도구일지도 모르겠다.

이 글이 흥미로웠다면, “프로그래머를 위한 카테고리 이론” 시리즈도 읽어보자. 여기서 다룬 합성, 곱과 합 타입, 함수 타입 같은 개념들이 카테고리 이론에서 어떻게 일반화되는지, 그리고 펑터나 자연 변환 같은 개념이 이 아이디어를 어떻게 확장하는지 볼 수 있다.