---
id: wiki-2026-0508-type-theory
title: Type Theory
category: 10_Wiki/Topics
status: verified
canonical_id: self
aliases: [Type System Theory, Lambda Calculus Types, Curry-Howard]
duplicate_of: none
source_trust_level: A
confidence_score: 0.9
verification_status: applied
tags: [type-theory, lambda-calculus, formal-methods, curry-howard, dependent-types]
raw_sources: []
last_reinforced: 2026-05-10
github_commit: pending
tech_stack:
  language: Haskell / Idris / Lean / Coq
  framework: theoretical
---

# Type Theory

## 매 한 줄
> **"매 타입은 명제, 매 프로그램은 증명 — Curry-Howard correspondence"**. Type theory 는 1902 Russell paradox 회피용 simple type theory 부터, 1934 Church 의 simply typed lambda calculus, 1972 Martin-Löf dependent type theory, 2026 Lean 4 / Idris 2 / Rocq (formerly Coq) 의 매 mathematical proof + program verification 의 통일 framework. 매 modern type system (Haskell, Rust, TypeScript) 의 매 핵심 개념 (parametric polymorphism, GADTs, refinement types) 의 출처.

## 매 핵심

### 매 type theory 의 계층
- **Simply Typed Lambda Calculus (STLC)**: `τ ::= ι | τ → τ` — function types only.
- **System F (parametric polymorphism)**: `∀α. τ` — generics 의 이론적 기반.
- **System Fω (type operators)**: `* → *` kinds — Haskell 의 type-level computation.
- **Calculus of Constructions (CoC)**: dependent types — Coq, Lean.
- **Homotopy Type Theory (HoTT)**: types as spaces, equality as paths.

### 매 Curry-Howard correspondence
- 매 propositions ⟺ types.
- 매 proofs ⟺ programs.
- 매 implication `A → B` ⟺ function `A → B`.
- 매 conjunction `A ∧ B` ⟺ pair `(A, B)`.
- 매 disjunction `A ∨ B` ⟺ sum `Either A B`.
- 매 universal `∀x. P(x)` ⟺ dependent function `(x: A) → P(x)`.

### 매 응용
1. Theorem proving — Lean 4 (mathlib), Coq/Rocq (CompCert verified C compiler).
2. Verified software — seL4 microkernel (Isabelle/HOL).
3. Practical type systems — Haskell GADT, Rust lifetime, TypeScript conditional types.

## 💻 패턴

### Haskell: parametric polymorphism (System F)
```haskell
-- 매 ∀α. [α] → Int
length :: forall a. [a] -> Int
length [] = 0
length (_:xs) = 1 + length xs
```

### Haskell: GADT (refined return types)
```haskell
{-# LANGUAGE GADTs #-}
data Expr a where
  IntLit  :: Int -> Expr Int
  BoolLit :: Bool -> Expr Bool
  If      :: Expr Bool -> Expr a -> Expr a -> Expr a

eval :: Expr a -> a
eval (IntLit n)  = n
eval (BoolLit b) = b
eval (If c t e)  = if eval c then eval t else eval e
```

### Idris: dependent type (vector with length)
```idris
data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect n a -> Vect (S n) a

-- 매 length encoded in type — no runtime check needed
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil ys = ys
append (x :: xs) ys = x :: append xs ys
```

### Lean 4: theorem as type
```lean
-- 매 proposition: ∀ n : ℕ, n + 0 = n
theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.succ_add, ih]
```

### TypeScript: conditional types (System Fω-ish)
```typescript
type IsArray<T> = T extends Array<any> ? true : false;
type A = IsArray<number[]>;  // true
type B = IsArray<string>;    // false

// 매 distributive
type ToArray<T> = T extends any ? T[] : never;
type C = ToArray<string | number>;  // string[] | number[]
```

### Rust: phantom type for state encoding
```rust
use std::marker::PhantomData;
struct Connection<State> { _state: PhantomData<State> }
struct Open; struct Closed;

impl Connection<Closed> {
  fn open(self) -> Connection<Open> { Connection { _state: PhantomData } }
}
impl Connection<Open> {
  fn send(&self, data: &[u8]) {}
  fn close(self) -> Connection<Closed> { Connection { _state: PhantomData } }
}
// 매 .send() on Closed 는 compile error
```

### Haskell: refinement via Liquid Haskell
```haskell
{-@ type Pos = {v:Int | v > 0} @-}
{-@ divPos :: Int -> Pos -> Int @-}
divPos x y = x `div` y  -- 매 SMT solver 가 y > 0 검증
```

## 매 결정 기준

| 상황 | Approach |
|---|---|
| Mathematical proof | Lean 4 / Rocq (Coq) |
| Verified compiler / OS | Coq (CompCert) / Isabelle (seL4) |
| Industrial typed FP | Haskell + GADT + TypeFamilies |
| Practical dependent types | Idris 2 |
| TypeScript-level type-level | conditional + mapped + template literal |
| Compile-time state machine | Rust phantom types / typestate |

**기본값**: 매 application 은 Haskell/Rust/TS 의 expressive type system; 매 critical proof 는 Lean 4.

## 🔗 Graph
- 부모: [[TypeScript 타입 시스템 (TypeScript Type System)|Type System]] · [[Formal Methods]]
- 응용: [[Coq]]
- Adjacent: [[Curry-Howard]]

## 🤖 LLM 활용
**언제**: 매 type system design 이해, advanced FP, formal verification, TS type-level wizardry.
**언제 X**: 매 일반 application 작성 — overkill.

## ❌ 안티패턴
- **Type-level "abuse" in TS**: 매 IDE 가 5분 freeze — 단순 runtime check 가 나음.
- **Dependent type 없는 곳 흉내**: 매 Haskell phantom type 으로 vector length 흉내 — 진짜 검증 안됨, runtime panic 가능.
- **Curry-Howard 의 직접 응용 실수**: 매 Hindley-Milner type inference 는 type-level recursion 에 약함 — 매 explicit annotation 필요.

## 🧪 검증 / 중복
- Verified (Pierce "Types and Programming Languages", Martin-Löf "Intuitionistic Type Theory", HoTT Book).
- 신뢰도 A.

## 🕓 Changelog
| 날짜 | 변경 |
|---|---|
| 2026-05-08 | Phase 1 |
| 2026-05-10 | Manual cleanup — type theory full content (Curry-Howard, GADT, dependent, Lean) |
