타입 시스템: 검사, 추론, 다형성, 변성, 건전성

의미론·바인딩·평가 전략은 프로그래밍 언어 의미론에, TypeScript에서의 구조적 타입과 함수 대입 규칙은 TypeScript 타입 호환성에 있다.

타입 시스템이란

타입 시스템은 식(expression)마다 그 식이 계산할 값의 종류(타입)를 붙이고, 규칙에 맞지 않는 조합을 거부하는 규칙 체계다. 「정수에 함수를 적용한다」, 「문자열을 더한다」 같은 무의미한 연산을 실행 전에 또는 실행 중에 막는다. 타입은 값의 집합으로 볼 수 있다. bool은 {true, false}, int → bool은 정수를 받아 불리언을 내는 함수 전체의 집합이다.

정적 검사와 동적 검사

구분	언제	무엇을 확인하나	언어
정적 타입 검사	컴파일(또는 실행 전 분석) 시점	소스 코드의 모든 경로에서 식의 타입이 규칙에 맞는가	Java, Go, Rust, Haskell, TypeScript
동적 타입 검사	실행 중, 연산 직전	지금 실제로 들어온 값의 런타임 태그가 연산에 맞는가	Python, JavaScript, Ruby

정적 검사는 실행하지 않은 경로의 오류도 잡지만, 보수적이라 실제로는 안전한 프로그램 일부도 거부한다(if true then 1 else "a").
동적 검사는 값에 타입 태그를 달고 다니며 연산 때 확인한다. 정적 언어도 다운캐스트, 배열 경계, null 역참조는 실행 중에 검사한다.
강한(strong)·약한(weak) 타입은 정적·동적과 다른 축이다. 암묵적 변환을 얼마나 허용하느냐("1" + 1)의 문제이고 정의가 엄밀하지 않다.

타입 검사를 통과해도 보장되지 않는 것: 종료 여부(무한 루프), 0으로 나누기·배열 범위·null 같은 값에 따른 실패(타입이 표현하지 않는다면), 논리적 정확성(정렬 함수가 실제로 정렬하는가), 자원 누수와 데이터 경쟁(타입이 소유권을 표현하지 않는다면). 타입은 「무엇을 표현하느냐」만큼만 보장한다.

타입 판단과 추론 규칙

타입 시스템은 타입 판단(typing judgment) Γ ⊢ e : T로 쓴다. 「변수의 타입을 적은 환경 Γ 아래에서 식 e는 타입 T를 가진다」는 뜻이다. 판단은 추론 규칙(inference rule) 으로만 도출된다. 가로줄 위가 전제, 아래가 결론이다.

  x : T ∈ Γ                Γ, x:T₁ ⊢ e : T₂                Γ ⊢ f : T₁ → T₂    Γ ⊢ a : T₁
 ──────────  (변수)      ─────────────────────── (추상화)   ──────────────────────────── (적용)
  Γ ⊢ x : T               Γ ⊢ λx:T₁. e : T₁ → T₂                  Γ ⊢ f a : T₂

변수 참조: 환경에서 그 변수의 타입을 찾는다. 없으면 「정의되지 않은 변수」 오류다.
함수 적용: 함수 쪽이 T₁ → T₂여야 하고, 인자가 정확히 T₁이어야 결과가 T₂다. 둘이 어긋나면 타입 오류다.
컴파일러의 타입 검사기는 이 규칙들을 식의 구조를 따라 재귀적으로 적용하는 함수다.

타입을 만드는 방법

타입	값의 구성	만들기	쓰기	언어 예
곱 타입(product)	A 그리고 B. 경우의 수는 곱	튜플·레코드 생성 `(1, "a")`	필드 접근, 분해	구조체, `record`, 튜플
합 타입(sum)	A 또는 B 중 정확히 하나 + 어느 쪽인지 태그	생성자 `Some(3)`, `Err(e)`	패턴 매칭으로 경우를 나눈다	Rust `enum`, Haskell `data`, Java `sealed` + `record`, TS 판별 유니언
함수 타입	`A → B`	람다·함수 정의	적용(호출)	모든 일급 함수 언어
재귀 타입	자기 자신을 포함하는 타입	`Cons(1, Cons(2, Nil))`	재귀적 패턴 매칭	리스트, 트리

재귀 타입은 List = Nil | Cons(Int, List)처럼 타입 정의가 자기 이름을 참조해 끝없이 큰 값을 유한한 정의로 표현한다. 재귀 함수가 계산이 자기 자신을 부르는 것이라면, 재귀 타입은 값의 모양이 자기 자신을 품는 것이다. 재귀 타입의 값을 처리하는 함수는 보통 같은 구조의 재귀 함수가 된다(구조적 재귀). 메모리 크기를 정해야 하는 언어에서는 재귀 위치를 포인터로 감싼다(Rust Box<List>).

Option과 Result: 부재와 실패를 타입에 넣는다

타입	경우	호출자가 처리할 것
`Option<T>` (`Maybe`)	`Some(T)` / `None`	값이 없을 때의 대체 동작
`Result<T, E>` (`Either`)	`Ok(T)` / `Err(E)`	성공 값과 오류 종류별 처리

null은 모든 참조 타입에 몰래 섞인 값이라 검사기가 「여기서 확인했는가」를 모른다. Option·Result는 부재·실패를 별도의 경우로 만들어, 두 경우를 모두 다루기 전에는 안의 값을 꺼낼 수 없게 한다. 일일이 매칭하는 대신 map, and_then(flatMap), unwrap_or로 합성하고, Rust는 ? 연산자로 오류를 호출자에게 그대로 올린다. Java의 Optional은 같은 발상의 라이브러리 타입이다(Java 실무 관용구).

예외와 Result의 차이

기준	예외(exception)	Result 타입
제어 흐름	`throw`가 호출 스택을 거슬러 올라가 가장 가까운 `catch`로 비지역 점프	평범한 반환값. 흐름은 그대로이고 호출자가 분기한다
함수 타입	시그니처에 보통 드러나지 않는다(Java checked 예외만 `throws`로 드러난다)	반환 타입 `Result<T, E>`에 실패가 드러난다
확인 강제	잡지 않아도 컴파일된다(unchecked). 빠뜨리면 실행 중 전파	꺼내려면 경우를 처리해야 한다. 무시하면 경고(Rust `#[must_use]`)
비용	정상 경로는 싸고 던질 때 비싸다(C++ 예외 처리의 내부 동작)	매 호출마다 분기 하나
맞는 곳	복구할 수 없는 오류, 깊은 곳에서 최상위로 한 번에 올릴 때	호출자가 예상하고 처리해야 하는 실패(파싱, 조회 실패)

Go는 (값, error) 다중 반환으로 Result와 같은 방식을 쓰되 처리를 강제하지는 않는다(Go 언어).

타입 추론

타입 검사는 주석(어노테이션)이 붙은 프로그램이 규칙에 맞는지 확인하는 일이고, 타입 추론은 주석이 없는 자리의 타입을 찾아내는 일이다. Hindley-Milner 방식의 추론은 두 단계다.

제약 생성: 모르는 타입마다 타입 변수를 붙이고, 규칙에서 나오는 등식을 모은다.
단일화(unification): 등식을 풀어 타입 변수에 대입할 값을 찾는다. 모순이면 타입 오류다.

let f = fun x -> x + 1        x : α,  f : α → β
제약:  (+) : int → int → int 이므로  α = int,  β = int
해:    f : int → int
 
let id = fun x -> x            x : α,  제약 없음  →  id : ∀α. α → α  (일반화, let 다형성)

단일화는 α = int → β 같은 등식에서 양쪽 구조를 맞춰 가며 대입을 만든다. α = α → int처럼 변수가 자기 자신을 포함하면 무한 타입이 되므로 발생 검사(occurs check) 로 거부한다. Java var, Kotlin, TypeScript, Go :=는 대부분 식의 타입을 지역적으로만 추론하는 약한 형태이고, OCaml·Haskell은 프로그램 전체에서 추론한다.

다형성

종류	뜻	결정 시점	예
매개변수 다형성(parametric)	타입을 매개변수로 받아 모든 타입에 같은 코드가 동작한다	컴파일	제네릭 `List<T>`, `id : ∀α. α → α`, C++ 템플릿
부분형 다형성(subtype)	하위 타입 값을 상위 타입 자리에 쓰고, 실제 객체의 구현이 불린다	실행	상속·인터페이스 구현 + 메서드 오버라이딩
임시 다형성(ad-hoc)	같은 이름이 타입마다 다른 구현을 가진다	컴파일(대개)	오버로딩, 연산자 오버로딩, Haskell 타입 클래스, Rust 트레이트

객체 지향에서 말하는 정적 다형성은 컴파일 시점에 어떤 구현을 쓸지 정해지는 것(오버로딩, 템플릿·제네릭)이고, 동적 다형성은 실행 시점에 실제 객체 타입으로 정해지는 것(오버라이딩, 가상 함수 호출)이다. 동적 다형성은 vtable 같은 간접 호출로 구현된다(C++ 상속과 가상 함수). Java에서 두 방식이 어떻게 다르게 고르는지는 Java 언어 기본의 오버로딩과 오버라이딩에 있다.

매개변수 다형성의 구현은 둘로 갈린다. 단형화(monomorphization) 는 쓰인 타입마다 코드를 복제해 빠르지만 바이너리가 커진다(C++, Rust). 소거·박싱은 코드 하나를 공유해 작지만 실행 중 타입 정보가 없다(Java 타입 소거). Go 제네릭은 둘을 섞은 GC 형태(gcshape) 단형화를 쓴다.

명목적·구조적 타입과 덕 타이핑

방식	타입 관계를 정하는 기준	확인 시점	언어
명목적(nominal)	선언된 이름과 상속 관계. `implements Foo`라고 적어야 Foo다	정적	Java, C#, Kotlin
구조적(structural)	멤버의 모양. 필요한 멤버를 다 가졌으면 그 타입이다	정적	TypeScript, Go 인터페이스, OCaml 객체
덕 타이핑	실제로 쓰이는 멤버가 그 순간 있는가	동적	Python, Ruby, JavaScript

구조적 타입과 덕 타이핑은 「모양이 맞으면 된다」는 발상이 같다. 차이는 언제 확인하느냐다. 구조적 타입은 실행 전에 타입 전체의 모양을 비교하고, 덕 타이핑은 실행 중 그 호출에 쓰인 멤버만 본다. Python의 typing.Protocol은 덕 타이핑 코드에 구조적 정적 검사를 더한다(Python 언어 동작). 명목적 타입은 모양이 같아도 의미가 다른 타입(UserId와 OrderId)을 구분할 수 있다.

변성: 공변, 반공변, 무공변

Cat이 Animal의 하위 타입(Cat <: Animal)일 때, 이를 감싼 타입 F<Cat>과 F<Animal>의 관계가 변성(variance)이다.

변성	관계	안전한 경우
공변(covariant)	`F<Cat> <: F<Animal>` (방향 유지)	값을 꺼내기만 하는 자리: 함수 반환 타입, 읽기 전용 컬렉션
반공변(contravariant)	`F<Animal> <: F<Cat>` (방향 반대)	값을 넣기만 하는 자리: 함수 매개변수, 소비자
무공변(invariant)	둘 사이에 관계 없음	읽기와 쓰기가 모두 되는 자리: 가변 컬렉션

함수 타입은 매개변수에 반공변, 반환에 공변이다. Animal → Cat 함수는 Cat → Animal이 필요한 자리에 쓸 수 있다. 더 넓은 입력을 받고 더 좁은 출력을 내므로 호출자의 기대를 모두 지킨다.
가변 컨테이너는 무공변이어야 안전하다. List<Cat>을 List<Animal>로 볼 수 있다면 거기에 Dog를 넣을 수 있고, 원래 List<Cat>을 쓰던 쪽이 고양이 대신 개를 꺼낸다. Java 배열은 공변으로 설계돼 이 구멍을 실행 중 ArrayStoreException으로 막는다. Java 제네릭은 무공변이고 ? extends(공변)·? super(반공변) 와일드카드로 사용 지점에서 변성을 고른다(PECS). Kotlin·C#은 선언 지점에 out·in을 붙인다.
TypeScript가 메서드 매개변수를 이변(bivariant)으로 허용하는 예외는 TypeScript 타입 호환성에 있다.

패턴 매칭의 완전성 검사

완전성 검사(exhaustiveness checking) 는 합 타입을 패턴 매칭할 때 모든 경우를 다뤘는지 컴파일러가 확인하는 것이다. 빠진 경우는 실행 중 「매칭 실패」가 되는 대신 컴파일 오류·경고가 된다.

합 타입에 새 경우(Refunded)를 추가하면, 그 타입을 매칭하는 모든 곳이 컴파일 오류로 드러난다. 수정할 곳을 검색하지 않아도 컴파일러가 목록을 준다. 대신 _·default 같은 와일드카드 분기를 쓴 곳은 조용히 통과하므로 새 경우를 놓친다.
이 검사가 가능하려면 경우의 목록이 닫혀 있어야 한다. Java는 sealed 계층과 switch 패턴(모던 Java 기능), Rust·Haskell은 enum·data, TypeScript는 판별 유니언과 never 검사로 닫힌 집합을 만든다.
이것이 표현 문제(expression problem) 의 한쪽이다. 합 타입은 새 연산(함수) 추가가 쉽고 새 경우 추가가 어렵다. 객체 지향 상속은 새 경우(하위 클래스) 추가가 쉽고 새 연산(메서드) 추가가 어렵다.

타입 건전성: 진행과 보존

타입 건전성(type soundness, type safety) 은 「타입 검사를 통과한 프로그램은 정의되지 않은 상태에 빠지지 않는다」는 성질이다. 「잘 타입된 프로그램은 잘못되지 않는다(Well-typed programs cannot go wrong)」로 요약된다. 표준 증명은 두 정리로 나눈다.

정리	내용
진행(progress)	잘 타입된 식은 이미 값이거나, 한 단계 더 계산할 수 있다. 막힌(stuck) 상태, 예컨대 `true + 1`이 아니다
보존(preservation, subject reduction)	잘 타입된 식이 한 단계 계산되면, 결과도 같은 타입으로 잘 타입된다

둘을 이어 붙이면 계산을 몇 단계 진행해도 막힌 상태에 닿지 않는다. 이는 작은 단계 의미론 위에서 정의된다.

건전성은 종료를 보장하지 않는다. 진행 정리는 「한 단계 더 갈 수 있다」만 말하므로 영원히 계산하는 프로그램도 건전하다. 종료까지 보장하는 강정규화(strong normalization)는 단순 타입 람다 계산처럼 재귀를 막은 체계에서만 성립한다.
실용 언어는 일부러 구멍을 둔다. Java 배열 공변성, TypeScript의 any와 이변 매개변수, C의 캐스트가 그렇다. 런타임 검사로 메우거나(Java) 건전성을 포기한다(TypeScript).

표현력을 넓힌 타입

의존 타입

의존 타입(dependent type) 은 타입이 값에 따라 달라지는 타입이다. 제네릭 List<T>는 타입 T에 의존하지만, 의존 타입 Vec<T, n>은 길이라는 값 n에 의존한다.

append : Vec<T, m> → Vec<T, n> → Vec<T, m + n>
head   : Vec<T, n + 1> → T          -- 빈 벡터에는 타입 수준에서 호출할 수 없다

배열 범위 오류, 빈 리스트의 head 같은 값 수준의 실패를 컴파일 시점에 막는다. 타입 검사 중에 값을 계산해야 하고 증명을 함께 써야 하므로 Idris, Agda, Coq(Rocq), Lean 같은 증명 지원 언어에서 주로 쓴다.

선형 타입과 아핀 타입

타입	값 사용 제약	표현하는 것
선형(linear)	정확히 한 번 쓴다	반드시 해제·닫아야 하는 자원(파일 핸들을 닫지 않으면 컴파일 오류)
아핀(affine)	최대 한 번 쓴다(버려도 된다)	소유권 이동. 옮긴 뒤의 값은 다시 쓸 수 없다

Rust의 소유권은 아핀 타입에 가깝다. let b = a;로 옮긴 뒤 a를 쓰면 컴파일 오류이고, 버려진 값은 스코프 끝에서 drop이 자동 호출된다. 그래서 두 번 해제(double free), 해제 후 사용(use-after-free), 스레드 간 데이터 경쟁을 GC 없이 컴파일 시점에 막는다. Haskell은 LinearTypes 확장으로 선형 함수 타입을 지원한다.

효과 시스템

효과 시스템(effect system) 은 반환 타입에 더해 계산이 무슨 부수 효과를 일으키는지를 타입에 기록한다. readFile : Path → String ! {IO, Exception}처럼 쓰고, 효과가 없는 함수 안에서 효과 있는 함수를 부르면 타입 오류다.

Java의 checked 예외(throws IOException)는 예외라는 효과 하나만 추적하는 단순한 효과 시스템이다.
Haskell은 IO a, State s a 같은 모나드 타입으로 효과를 반환 타입에 넣는다. IO가 붙지 않은 함수는 입출력을 할 수 없다.
Koka, OCaml 5의 효과 핸들러는 효과를 선언하고 호출 지점 바깥에서 처리 방법을 바꿔 끼운다(예외, 상태, 비동기를 하나의 장치로 표현).

정리

타입 시스템은 식에 타입을 붙여 무의미한 연산을 막는다. 정적 검사는 모든 경로를, 동적 검사는 실제 값을 본다.
타입 판단 Γ ⊢ e : T는 추론 규칙으로 도출되고, 추론은 제약 생성과 단일화로 한다.
곱·합·함수·재귀 타입으로 값을 구성하고, Option·Result는 부재와 실패를 처리하도록 강제한다.
다형성은 매개변수(제네릭)·부분형(오버라이딩)·임시(오버로딩)로 나뉘고, 정적·동적 다형성은 결정 시점의 차이다.
가변 컨테이너는 무공변, 함수는 매개변수 반공변·반환 공변이다.
건전성은 진행과 보존이며 종료는 보장하지 않는다. 의존·선형·효과 타입은 타입이 보장하는 범위를 넓힌다.

버그 제보