4. 언어 이론과 타입 시스템 — 코드는 문법만 맞는다고 프로그램이 되지 않는다

프로그램을 이해하려면 세 질문을 분리해야 한다. 문법상 허용되는가, 어떤 값으로 실행되는가, 실행 전에 어떤 실패를 배제할 수 있는가. 이 챕터는 작은 표현식 언어 하나를 기준 모델로 삼아 스코프·클로저·타입 추론·서브타이핑을 서로 연결된 규칙으로 읽는다.

학습 목표

• 구문, 실행 의미, 정적 타입 판단의 책임을 구분한다.
• 환경과 closure를 이용해 이름이 어떤 값을 가리키는지 추적한다.
• 타입 검사가 배제하는 실패와 종료·I/O·논리 오류처럼 남는 실패를 구분한다.
• 다형성·서브타이핑·변성을 표현력, 안전성, 복잡성의 교환으로 판단한다.

배경: 익숙한 문법이 감추는 규칙

다음 JavaScript 코드는 문법상 문제가 없고 TypeScript에서도 상황에 따라 타입 검사를 통과한다. 그러나 handlers가 모두 마지막 값만 출력하는지, 0·1·2를 각각 출력하는지는 var와 let의 바인딩 생성 규칙에 달려 있다.

const handlers: Array<() => void> = [];
for (var index = 0; index < 3; index++) {
  handlers.push(() => console.log(index));
}
handlers.forEach((handler) => handler()); // 3, 3, 3

closure가 변수 이름을 복사한 것이 아니라 하나의 mutable binding을 캡처했고, 세 함수가 같은 binding을 읽기 때문이다. var를 let으로 바꾸면 반복마다 새 binding이 만들어져 0, 1, 2가 된다. 표면의 화살표 함수 문법만 알아서는 결과를 설명할 수 없다. 환경을 언제 만들고 closure가 어느 환경을 보존하는지 알아야 한다.

반대 방향의 사례도 있다.

function average(total: number, count: number): number {
  return total / count;
}

average(10, 0); // 타입은 number, 실행 결과는 Infinity(JavaScript)

타입 검사는 두 인자가 number라는 계약은 확인하지만 count !== 0은 타입에 표현되어 있지 않다. 검사를 통과했다는 사실은 "모든 런타임 실패가 없다"가 아니라 그 타입 규칙이 금지한 오류는 없다는 뜻이다. 타입 보장을 평가하려면 타입 이름보다 규칙과 약속의 경계를 읽어야 한다.

세 층을 분리하는 판단 지도

층	입력과 질문	대표 산출물	이 층이 답하지 않는 것
구문(syntax)	문자·토큰이 문법에 맞는가	AST	이름이 가리키는 값, 연산의 결과
실행 의미(dynamic semantics)	AST와 환경이 만나 어떤 값·효과가 되는가	값 또는 실행 진단	실행 전 허용 여부
정적 의미(static semantics)	타입 환경에서 식에 어떤 타입을 줄 수 있는가	타입 또는 타입 진단	종료, 외부 시스템 성공, 논리적 정답

챕터 5의 parser는 첫 번째 층을 담당한다. 이 챕터는 parser가 만든 AST를 입력으로 가정하고 두 번째와 세 번째 층에 집중한다. 기준 인터페이스는 단순하다.

evaluate(expression, valueEnvironment) -> value | runtime error
infer(expression, typeEnvironment)      -> type  | type error

두 함수는 같은 AST를 보지만 환경과 결과가 다르다. 평가 환경은 이름을 실제 값에 연결하고, 타입 환경은 이름을 타입 스킴에 연결한다. let id = fun x -> x in id(true)에서 평가기는 id를 closure로 찾고 true를 대입해 실행한다. 타입 추론기는 id를 ∀a. a -> a로 찾고 이 사용 지점에 새 타입 변수로 인스턴스화한다.

언어 기능은 세 비용의 교환이다

언어 기능을 "있으면 편리하다"로 평가하면 경계에서 잘못된 결정을 한다. 최소한 세 축을 함께 본다.

• 표현력: 더 많은 프로그램과 추상화를 짧고 일반적으로 표현하는가?
• 안전성: 어떤 잘못된 프로그램을 실행 전에 거부하는가? 실제로 안전한 프로그램도 함께 거부하는가?
• 구현·학습 복잡성: 추론 알고리즘, 오류 메시지, 컴파일 시간, API 설명 비용이 얼마나 늘어나는가?

let 다형성은 identity 함수 하나를 여러 타입에서 재사용하게 하지만 일반화 경계와 mutation이 만나면 value restriction이 필요하다. 구조적 타입은 기존 JavaScript 객체를 자연스럽게 연결하지만 우연히 모양이 같은 도메인 개념까지 호환시킬 수 있다. 가변 배열의 공변성은 사용하기 편하지만 잘못된 원소를 넣는 길을 열어 런타임 검사를 필요로 한다. 표현력이 늘 때 안전 조건과 설명 비용도 함께 움직인다.

이 챕터의 기준 언어

본문과 실습은 숫자·불리언, 산술·비교, 조건식, 변수, 함수, 호출, let만 가진 Toy 언어를 공유한다.

let id = fun x -> x in
let ignored = id(1) in
id(true)

레코드·클래스·mutation·재귀·예외·서브타이핑은 의도적으로 제외한다. 환경 평가기와 Hindley–Milner 추론기를 끝까지 실행 가능한 크기로 유지하기 위해서다. 서브타이핑과 변성은 별도의 대체 가능성 모델로 다루며 HM 추론기에 섞지 않는다.

학습 순서

1. 4.1 언어 의미론은 AST를 환경에서 평가하며 lexical scope, closure, strict/lazy 평가를 추적한다.
2. 4.2 타입 안전성과 추론은 같은 AST에 타입 규칙을 적용하고 제약·단일화·일반화로 principal type을 구한다.
3. 4.3 추상화와 서브타이핑은 다형성, 명목적·구조적 타입, 함수·컨테이너 변성을 대체 가능성으로 판단한다.

읽는 동안 모든 예제에 세 질문을 반복한다. "어느 환경을 조회하는가?", "무슨 규칙이 이 식을 허용하는가?", "그 규칙이 약속하지 않은 것은 무엇인가?" 이 질문이 특정 언어의 키워드를 다른 언어에서도 통하는 모델로 바꾼다.

정리

• 구문은 구조를 만들고, 실행 의미는 값을 계산하며, 정적 의미는 실행 전에 허용할 프로그램을 근사한다.
• closure 버그는 이름보다 환경과 binding의 수명으로, 타입 보장은 통과 여부보다 배제한 오류 집합으로 설명해야 한다.
• 언어 기능은 표현력·안전성·복잡성의 교환이다. 하나만 보고 기능이나 API를 선택하면 경계 비용을 놓친다.

확인 문제

1. 타입 검사를 통과한 readConfig(path)가 파일 부재로 실패했다. 이것을 타입 시스템의 비건전성이라고 바로 결론 내릴 수 없는 이유는 무엇인가?

정답과 해설

타입 안전성은 타입 규칙이 약속한 오류의 부재다. 반환 타입이 Config이고 I/O 실패가 예외나 프로세스 오류로 모델링되어 있다면 파일 존재 여부는 그 타입이 표현하지 않은 성질이다. 비건전성을 주장하려면 "잘 타입된 프로그램이 타입 규칙상 불가능하다고 한 상태에 도달했다"는 반례가 필요하다. 실패를 Result<Config, IOError> 같은 타입에 포함시키면 보장의 경계가 이동하지만 호출자의 처리 비용도 늘어난다.

2. 두 언어가 같은 fun x -> x 문법을 허용해도 다른 결과를 낼 수 있는가? 어떤 규칙이 달라져야 하는지 예를 들어 설명하라.

정답과 해설

가능하다. lexical scope 언어는 함수 정의 시점 환경을 closure에 저장하고, dynamic scope 언어는 호출 시점 환경에서 자유 변수를 찾는다. 함수 본문에 자유 변수 rate가 있다면 같은 AST라도 어느 환경을 조회하느냐에 따라 값이 달라진다. strict와 lazy처럼 인자를 언제 평가하는지 달라도 예외·부작용·종료 결과가 달라질 수 있다.

참고 자료

• Benjamin C. Pierce, Types and Programming Languages (2002), Ch. 3–11 — operational semantics와 타입 안전성을 하나의 작은 언어 위에서 연결하는 기준 모델이다.
• Robin Milner, “A Theory of Type Polymorphism in Programming” (1978) — let 다형성과 타입 안전성의 원전이다.
• Robert Nystrom, Crafting Interpreters — 환경·closure 기반 tree-walk interpreter를 실행 가능한 구현으로 확장할 때 참고한다.