[PLT] Type Systems (타입 시스템)

Type Systems, 타입 시스템, static typing, dynamic typing, type inference, Hindley-Milner, structural typing, nominal typing, gradual typing, sound type system, type soundness

정의

타입 시스템 (Type System) 은 프로그램의 값과 표현식에 타입 (type) 을 부여하고, 이 타입들이 규칙에 맞게 결합되는지 검증하는 형식 체계입니다.

타입 = 값의 집합 + 그 값들에 정의된 연산.

• number: 수의 집합 + 산술 연산
• string: 문자열 + 결합/추출
• Array<T>: T의 배열 + push/pop 등
• () => number: 인자 없이 number 반환하는 함수

목적: 특정 종류의 오류를 컴파일 시 (또는 런타임 시) 방지.

왜 타입 시스템인가

방지하는 오류

• "hello" + 3 (문자열/숫자 혼합, 언어별)
• null.foo (null 참조)
• array[100] (index out of bounds)
• divideByZero(10, 0) (0 나눗셈)
• Map<string, number> 에 boolean 저장

얻는 이익

• 문서화: 함수 시그니처로 사용법 명시
• 자동완성: IDE 가 타입 기반 제안
• 리팩터링 안전성: rename, extract method
• 성능: 컴파일러가 최적화 (JIT 는 타입 추측)

정적 vs 동적

Static Typing (정적 타이핑)

컴파일 시 타입 검사.

예: TypeScript, Rust, Java, C++, Haskell, Go, Kotlin

function add(a: number, b: number): number {
  return a + b;
}
add("hello", 1);  // 컴파일 오류

장점:

• 오류 조기 발견
• 리팩터링 안전
• 컴파일러 최적화 여지

단점:

• 프로토타이핑 느림
• 표현력 제약 (극한 케이스)

Dynamic Typing (동적 타이핑)

런타임 시 타입 검사.

예: Python, JavaScript (기본), Ruby, PHP, Lua, Clojure

function add(a, b) {
  return a + b;
}
add("hello", 1);  // "hello1" (JS 자동 변환)

장점:

• 유연성, 빠른 프로토타이핑
• 메타프로그래밍 자연스러움

단점:

• 런타임 오류
• IDE 지원 부족
• 대규모 코드베이스에서 유지보수 어려움

Strong vs Weak

Strong Typing: 타입을 엄격히 지킴. 자동 변환 최소.

• Python: "hello" + 3 → TypeError

Weak Typing: 자유로운 자동 변환.

• JavaScript: "hello" + 3 → "hello3"
• PHP: "1" == 1 → true

Strong vs Weak 은 스펙트럼. Static 인지 동적인지와 무관.

Type Checking

Nominal Typing

이름 기반. 두 타입이 같은 이름을 가지면 호환.

class Cat { String name; }
class Dog { String name; }

Cat c = new Cat();
Dog d = c;   // Java: 오류 (다른 이름)

C++, Java, C# 대표.

Structural Typing

구조 기반. 같은 shape 이면 호환.

interface Named { name: string; }
class Cat { name: string = ""; }

const n: Named = new Cat();   // TypeScript: OK (구조 같음)

TypeScript, Go, OCaml 대표.

Duck typing = “오리처럼 걷고 꽥꽥 하면 오리” = structural typing 의 dynamic 버전.

Trade-offs

• Nominal: 명확한 의도. 실수로 호환 불가.
• Structural: 유연. Boilerplate 감소.

Type Inference

명시 없이 컴파일러가 타입 추론.

Local (지역 추론)

변수 초기값에서 타입 결정:

let x = 42;         // number
let s = "hello";    // string

C++ (auto), Java (var), C# (var), Swift, Go (:=).

Global (전역 추론): Hindley-Milner

함수 시그니처도 추론. Haskell, ML, OCaml, Elm.

add x y = x + y
-- 추론: add :: Num a => a -> a -> a

컴파일러가 사용 문맥으로부터 타입 방정식 세우고 통합 (unification).

Damas-Milner 알고리즘: 다항 시간 안에 principal type 결정.

TypeScript / Rust

지역 추론 + contextual typing. 완전한 Hindley-Milner 는 아니지만 실용적.

Sound vs Unsound

Sound 타입 시스템: 컴파일 통과한 프로그램은 런타임에 타입 오류 없음.

Unsound: 통과해도 런타임 오류 가능.

예:

• Haskell, Rust, OCaml: sound (거의)
• Java, C#: sound (array covariance 등 예외)
• TypeScript: 의도적으로 unsound. 실용성 우선.

// TypeScript 는 unsound 인 예
const arr: number[] = [];
const anyArr: any[] = arr;
anyArr.push("string");   // 컴파일 OK
arr[0].toFixed(2);        // 런타임 오류

TypeScript 는 “developer productivity” 우선. 100% soundness 는 실전 부담.

주요 타입 시스템 개념

Union / Intersection

• Union (A | B): A 또는 B
• Intersection (A & B): A 이고 B

자세한 것은 TypeScript Union/Intersection 참조.

Generics (Parametric Polymorphism)

타입 매개변수:

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

Java <T>, C++ template<T>, Haskell forall a.

Subtyping

Dog extends Animal → Dog 는 Animal 의 subtype. Liskov Substitution.

Variance

Generic 안 subtype 관계:

• Covariant (out T): List<Dog> → List<Animal> OK
• Contravariant (in T): Consumer<Animal> → Consumer<Dog> OK
• Invariant: 관계 없음

Higher-Rank / Higher-Kinded Types

• HKT: 타입 생성자를 타입 매개변수로. Functor<F>. Haskell, Scala.
• Rank-N: 함수 인자로 다형 함수. Rust for<'a> ....

Dependent Types

값이 타입을 결정. Vector<N: nat> (길이 N의 벡터).

Idris, Agda, Coq, Lean, F*. 형식 증명.

Refinement Types

서브셋 타입. PositiveInt = { x: int | x > 0 }.

LiquidHaskell, F*.

Type Erasure vs Reified

Type Erasure: 컴파일 후 타입 사라짐. Java generics, TypeScript.

Reified: 런타임에 타입 유지. C#, Kotlin (reified), Rust (monomorphization).

Gradual Typing

정적 + 동적 혼합. any 타입으로 escape.

예:

• TypeScript: JavaScript 위에 점진 도입
• Python + mypy / TypeScript-like
• PHP with type hints
• Sorbet (Ruby)
• Flow

프로덕션 코드베이스에 실용적.

언어별 특징

TypeScript

• 구조 타이핑 + 강력한 추론
• Union / intersection / mapped / conditional
• Unsound (intentionally)
• 자세한 것은 TypeScript 참조

Rust

• Sound, ownership + lifetimes
• Trait 기반 (Haskell type class 스타일)
• Monomorphization (reified)

Haskell

• Hindley-Milner 완전 추론
• 타입 클래스 (ad-hoc polymorphism)
• Pure (side effect 도 타입 안)

Java

• Nominal, subtyping
• Erased generics
• Wildcard variance

Python

• 동적 + gradual (typing module, mypy)
• Duck typing

Type-safe Programming 팁

• any 최소화 (TypeScript, Python)
• Discriminated union 활용 (Rust enum, TS union)
• Exhaustive matching (compiler 가 case 누락 감지)
• NewType 패턴: UserId vs ProductId (branded types)
• Immutability by default

실전 튜토리얼

간단한 타입 검사기 (의사코드)

check(expr, env):
    switch expr.kind:
        case NumberLiteral: return NumberType
        case StringLiteral: return StringType
        case BooleanLiteral: return BoolType

        case Identifier:
            if sym in env: return sym.type
            error(f"Undefined: {expr.name}")

        case BinaryOp:
            lt = check(expr.left, env)
            rt = check(expr.right, env)
            if expr.op in ['+', '-', '*', '/']:
                if lt == NumberType and rt == NumberType:
                    return NumberType
                error(f"Type mismatch: {lt} {expr.op} {rt}")
            if expr.op in ['==', '<', '>']:
                if lt == rt:
                    return BoolType
                error(...)

        case IfExpr:
            ct = check(expr.cond, env)
            if ct != BoolType: error("if condition must be bool")
            tt = check(expr.then, env)
            et = check(expr.else, env)
            if tt != et: error("if branches must have same type")
            return tt

        case FunctionCall:
            ft = check(expr.callee, env)
            if not isinstance(ft, FunctionType):
                error("Not callable")
            for arg, paramType in zip(expr.args, ft.paramTypes):
                argType = check(arg, env)
                if not isAssignable(argType, paramType):
                    error(...)
            return ft.returnType

함정

관련 위키

• PLT 개요
• Semantic Analysis
• AST
• TypeScript
• TypeScript Generics
• Union/Intersection
• TypeScript Strict Mode