부구조적 타입 시스템(Substructural Type Systems)은 변수 사용 횟수나 순서를 타입 시스템으로 제어하는 타입 체계다. 선형 타입(Linear Types)과 어파인 타입(Affine Types)이 대표적이며 메모리 안전성을 컴파일 타임에 보장한다.
구조적 규칙 분류
고전 논리의 구조적 규칙:
약화(Weakening): A ⊢ B → A, C ⊢ B (사용 안 해도 됨)
축약(Contraction): A, A ⊢ B → A ⊢ B (복제 가능)
교환(Exchange): A, B ⊢ C → B, A ⊢ C (순서 무관)
부구조적 시스템:
선형(Linear): 약화 X, 축약 X → 정확히 1번 사용
어파인(Affine): 약화 O, 축약 X → 최대 1번 사용
관련(Relevant): 약화 X, 축약 O → 최소 1번 사용
순서(Ordered): 교환도 X → 순서대로만 사용
Rust의 소유권 시스템 (어파인 타입)
rust
fn main() {
let s1 = String::from("hello");
let s2 = s1; // s1의 소유권 이동 (move)
// println!("{}", s1); // 컴파일 에러! s1은 이미 이동됨
// 빌림(Borrow): 소유권 없이 참조
let s3 = String::from("world");
let len = calculate_length(&s3); // 불변 빌림
println!("{} has length {}", s3, len); // s3 여전히 유효
// 가변 빌림: 동시에 하나만
let mut s4 = String::from("hello");
let r1 = &mut s4;
// let r2 = &mut s4; // 에러! 가변 빌림은 하나만
}
선형 타입의 응용
1. 메모리 관리: malloc/free 짝 보장
2. 파일 핸들: open/close 정확히 1회
3. 채널 통신: 메시지를 정확히 1회 소비
4. 암호화 키: 재사용 방지
Haskell Linear Haskell:
f :: Int %1 -> Int -- 인자를 정확히 1번 사용
Linear ML (LLVM 기반):
let! x = malloc() -- 선형 자원
use(x) -- 정확히 1번 사용
-- free 자동 삽입
세션 타입 (Session Types)
선형 타입의 확장으로 통신 프로토콜을 타입으로 표현.
인증 프로토콜 세션 타입:
Client: !Username . !Password . &{Success: ?Token . End, Fail: End}
Server: ?Username . ?Password . ⊕{Success: !Token . End, Fail: End}
!: 송신, ?: 수신, &: 외부 선택, ⊕: 내부 선택
타입이 맞으면 교착 상태(deadlock) 없음이 보장됨
관련 개념
