타입 이론 (type theory)

한 줄 정의: 프로그램의 값과 표현식에 '타입'이라는 분류를 부여하여, 프로그램이 실행되기 전에 특정 종류의 오류를 형식적으로 배제할 수 있도록 하는 수학적 논리 체계.

쉽게 풀면

타입 이론은 '이 값은 정수다', '이 함수는 문자열을 받아 불리언을 반환한다'처럼 프로그램의 각 부분에 타입이라는 꼬리표를 붙이고, 이 꼬리표들이 서로 앞뒤가 맞는지를 규칙에 따라 검사하는 이론이다. 정수에 문자열을 더하려는 시도처럼 타입이 맞지 않는 연산을 프로그램 실행 전에 미리 걸러낼 수 있어 많은 프로그래밍 언어의 컴파일러가 이 이론을 기반으로 타입 검사를 수행한다. 커리-하워드 대응을 통해 논리학의 증명 체계와도 깊이 연결되어 있다.

왜 중요한가

타입 이론은 프로그래밍 언어의 정적 검증뿐 아니라 정리 증명기(theorem prover)와 정형 검증(formal verification) 연구의 이론적 토대가 되기 때문에 프로그래밍 언어학과 논리학을 잇는 핵심 주제로 다뤄집니다. 커리-하워드 대응 덕분에 "타입을 검사하는 것"과 "수학적 증명을 검증하는 것"이 같은 문제로 취급될 수 있어, 소프트웨어의 정확성을 수학적으로 보장하려는 연구에서 반드시 언급됩니다.

논문에서는 이렇게 쓰입니다

"본 언어의 타입 시스템은 의존 타입 이론에 기반하여, 배열의 인덱스 범위를 컴파일 시점에 검증할 수 있도록 설계되었다."

프로그래밍 언어의 정적 타입 검사 메커니즘의 수학적 기반을 설명할 때 사용된다.

"Coq 및 Agda와 같은 증명 보조기는 타입 이론을 기반으로 하여, 프로그램의 명세를 타입으로 표현하고 그 타입에 맞는 항을 구성함으로써 정리의 증명을 완성한다."

정리 증명기 연구에서 타입 이론이 어떻게 실제 증명 작업의 기반이 되는지를 설명하는 문장입니다. 형식 검증 분야 논문에서 자주 등장합니다.

"선형 타입 이론(linear type theory)을 활용하여 자원이 정확히 한 번씩만 사용되도록 강제함으로써 메모리 누수 및 이중 해제 오류를 타입 수준에서 방지하였다."

자원 관리를 타입 규칙으로 제어하는 접근을 설명하는 문장으로, 시스템 프로그래밍 언어 설계 논문에서 볼 수 있는 표현입니다.

조금 더 깊게 보면

타입 이론에는 단순 타입 이론(simply typed lambda calculus)부터 다형성을 다루는 시스템 F, 값에 의존하는 타입을 허용하는 의존 타입 이론(dependent type theory)까지 표현력이 점차 확장되는 여러 체계가 있습니다. 표현력이 강해질수록 더 정교한 성질을 타입으로 검증할 수 있지만 타입 검사 자체의 결정 가능성과 계산 복잡도가 함께 증가하는 트레이드오프가 존재합니다. 논문을 읽을 때는 어떤 타입 이론 체계를 전제로 하는지(단순 타입인지, 의존 타입인지 등)를 확인하면 논증의 범위를 가늠하는 데 도움이 됩니다.

주의할 점

타입 이론이 모든 런타임 오류를 막아주는 것은 아니며, 타입 시스템이 표현할 수 있는 성질의 범위 안에서만 오류를 사전에 차단할 수 있다.