3과: 기여 정리와 타입 판단 Γ ⊢ t : T

한 문장 버전: 이 논문의 목표는 「컴포넌트가 런타임에 동적으로 장착되고, 또 깔끔하게 분리되는」 일을 추론 가능하고 검증 가능하게 만드는 것입니다. 이번 과에서는 먼저 논문의 전체 지도를 봅니다——네 가지 기여가 각각 어떤 두 종류의 조합 가능성을 뒷받침하는지. 그리고 두 작은 토대를 보강합니다: 타입 판단 Γ ⊢ t : T가 도대체 무엇을 말하는지, 그리고 효과 주석 T^effect가 왜 우리가 「구현을 보지 않고도 부수 효과를 알 수」 있게 해 주는지.

1. 논문의 네 가지 기여: 먼저 전체 지도 보기

논문의 1.3절은 네 가지 기여를 한 번에 제시합니다. 이것들은 단순한 「네 가지 성과」가 아니라 이후 모든 과의 목차이기도 합니다:

뜯어보는 것처럼, 네 가지 기여는 하나의 사슬입니다:

먼저 「장착하면 분리할 수 있다」를 해결하고(기여 1, 시간 차원) → 다음으로 「안정적으로 설 수 있다」를 해결하고(기여 2, 공간 차원) → 둘을 하나의 통합 모델에 담고(기여 3, 프로그래밍 패러다임) → 실제 프레임워크로 작성해 생태계로 검증합니다(기여 4, 실현).

🎁 비유: 플러그인은 호스트에 꽂는 「USB 메모리」와 같습니다——기여 1은 「뽑은 후에도 시스템이 원래대로」인 것을, 기여 2는 「꽂은 후 필요한 드라이버를 자동으로 찾는」 것을, 기여 3은 「USB 메모리의 전체 사용 주기가 규범적으로 관리되는」 것을 담당하고, 기여 4는 「핫플러그를 지원하는 컴퓨터를 실제로 만들어 낸」 것입니다.

💡 이후 과에서는 하나씩 자세히 다룹니다: 6과에서 되돌릴 수 있는 효과, 8과에서 반응형 여효과, 9과에서 생명주기, 10과에서 통합 컨텍스트 타입, 11~12과에서 Cordis 코어 라이브러리와 Koishi 사례를 다룹니다. 이번 과에서는 이 지도를 벽에 붙여 두는 것으로 충분합니다.

2. 타입 판단 Γ ⊢ t : T란 무엇인가?

논문 2장은 시작하자마자 독자가 기본적인 타입 이론과 범주론에 익숙하다고 가정한다고 말합니다. 당황하지 마세요——이번 과에 필요한 것은 딱 하나의 개념뿐입니다: **타입 판단(typing judgment)**입니다. 이것은 전혀 신비로운 것이 아니라, 여러분이 TypeScript에서 매일 겪는 일을 수학 기호로 옮겨 적은 것에 불과합니다. (범주론에 대해서는 4과에서 모나드를 다룰 때 가장 소박한 방식으로 꺼내 보일 것입니다.)

단순 타입 람다 계산법(STLC)에는 수학 공식처럼 생긴 표기가 있습니다:

Γ ⊢ t : T

소리 내어 읽으면 한 문장이 됩니다: 「타입 환경 Γ 아래에서, 항 t는 타입 T를 갖는다.」 기호를 하나씩 뜯어보겠습니다:

TypeScript와 대조해 볼 수 있게 되면 완전히 이해한 것입니다:

const x: number = 5;
const y = x + 1;   // 컴파일러: x는 number이고, x + 1도 number이다

컴파일러가 둘째 줄을 검사할 때, 마음속에는 「x : number」라는 작은 표가 있습니다——이 표가 바로 Γ입니다. 검사하고 있는 표현식 x + 1이 t이고, 도출한 결론 「타입은 number」이 T입니다. 타입 판단이란 「표 조회 + 검증 + 결론 도출」이라는 이 일련의 동작 전체를 격식 있게 적은 것에 불과합니다.

⚠️ Γ의 읽는 법에 주의하세요: 대문자 그리스 문자 「감마」이지 영문자 G가 아닙니다. 논문에서는 언제나 「현재 스코프에서 무엇을 알고 있는가」를 나타냅니다.

3. 효과 주석 T^effect: 타입이 「부수 효과」를 기억하게 하기

보통의 타입 판단 Γ ⊢ t : T는 한 가지 질문에만 답합니다: t가 무엇을 반환하는가. 하지만 실제 프로그램에서 함수는 결과를 반환하는 것 외에도 바깥 세계에 손을 댑니다——파일을 읽고, 데이터베이스에 쓰고, 전역 변수를 바꾸고, 네트워크 요청을 본냅니다. 이것들이 바로 부수 효과입니다.

효과 시스템(effect system)은 타입을 정교하게 다듬습니다: 타입 위에 효과 주석을 얹어 다음을 얻습니다:

Γ ⊢ t : T^effect

추가된 effect는 두 번째 질문에 답합니다: t가 T를 반환하는 것 외에 어떤 부수 효과를 만들어 내는가. 이것은 아묠게나 쓴 라벨이 아니라 「효과 대수」의 한 원소입니다——효과는 합성할 수도 비교할 수도 있고, 합집합을 구할 수 있는 집합과 같습니다. 고전적인 예:

• Maybe 효과: 실패할 수 있음(부분성)
• State 효과: 가변 상태
• IO 효과: 외부 세계와의 상호작용(파일 읽기, 네트워크)

💡 논문은 이 역사를 소개합니다: 효과 주석의 아이디어는 Lucassen과 Gifford에서 비롯되었고, 모나드 모델링은 Moggi로부터 나와 Wadler가 Haskell에서 널리 퍼뜨렸으며, 대수적 효과는 Plotkin과 Power로부터 나왔습니다. 이번 과에서 기억할 것은 하나뿐입니다: 효과 주석 = 타입 수준의 「부수 효과 설명서」.

왜 이것이 「조합적 추론」을 뒷받침하는가?

조합적 추론(compositional reasoning)은 이 구절에서 가장 값어치 있는 두 단어입니다. 그 의미는: 합성된 표현식의 성질을 판단할 때 각 구성 요소의 성질만 볼에 되고, 그 구현은 볼 필요가 없다는 것입니다.

구체적인 예를 들어 봅시다. 두 함수가 있다고 가정합니다:

// f: 파일을 읽음 (IO 효과를 가짐)
// g: 순수 함수, 산술 연산만 함 (부수 효과 없음)

// 그렇다면 f(g(x))는 어떤 효과를 가질까? — IO.
// f와 g의 소스를 읽을 필요 없이, 주석만 보고도 단정할 수 있다.

추론 과정은 한 문장이면 됩니다: 바깥쪽 f는 IO를 갖고, 안쪽 g는 순수하며, 부수 효과는 허공에서 사라지지 않으므로, 전체 f(g(x))에는 반드시 IO가 있습니다.

왜 이것이 중요한가? 실제 코드베이스는 수십만 줄에 달하기 십상이기 때문입니다. 효과 주석이 없다면, 어떤 함수가 몰래 전역 변수를 바꾸는지 알려면 그 구현을 처음부터 끝까지 읽는 수밖에 없습니다——게다가 그 함수가 호출하는 모든 함수까지 함께 읽어야 합니다. 주석이 있으면 부수 효과도 타입처럼 「국소적으로 검사」할 수 있습니다: 모든 함수가 설명서를 갖추고 있고, 합성할 때는 설명서를 이어 붙이기만 하면 됩니다.

🎁 비유: 보통의 타입은 「배달 주문서에 적힌 요리 이름」(당신이 무엇을 시켰는가)과 같고, 효과 주석은 「알레르기 유발 성분 목록」(그 요리에 들어 있는, 당신이 먹을 수 없는 것)과 같습니다. 한 상 가득 요리를 차릴 때, 각 요리의 알레르기 유발 성분 목록만 이어 붙이면 상 전체를 먹을 수 있는지 알 수 있습니다——주방에 들어가 조리 과정을 볼 필요가 없습니다.

4. 효과와 여효과를 두 차원에 대응시키기

논문 1.3절 맨 앞의 한 문장이 논문 전체의 열쇠입니다:

동적 조합 가능성의 두 차원은 각각 계산이 환경을 어떻게 변경하는가와 계산이 환경에 어떻게 의존하는가에 관한 것이다.

• 효과 = 「계산이 환경을 무엇을 변경했는가」에 답함(내가 무엇을 바꿨는가)
• 여효과(coeffect) = 「계산이 환경에 무엇을 제공받아야 하는가」에 답함(내가 필요한 것)

두 방향은 정확히 반대이며, 아래 그림은 둘을 함께 그린 것입니다:

전통적으로 효과와 여효과는 모두 어휘적으로 고정된 스코프 안에서 컴파일 시점에 정적 분석할 수밖에 없었습니다——즉, 컴파일러가 코드를 열기만 하면 전부 볼 수 있었는데, 모든 것이 코드를 작성할 때 이미 확정되어 있었기 때문입니다. 하지만 Cordis의 시나리오는 컴포넌트가 런타임에 동적으로 참가하고 이탈하는 것입니다: 런타임에 또 무엇이 로드될지는 아묘도 모릅니다. 그래서 논문은 둘을 한 단계씩 업그레이드했습니다:

여기까지 오면, 네 가지 기여와 두 차원이 순환 고리를 이룹니다:

• 기여 1(되돌릴 수 있는 효과) → 시간적 조합 가능성: 컴포넌트는 일생 동안 「환경을 변경」하므로, 바꾼 후에는 되돌릴 수 있어야 합니다.
• 기여 2(반응형 여효과) → 공간적 조합 가능성: 컴포넌트는 의존 그래프 안에 서 있으므로, 의존이 갖춰졌는지 감지할 수 있어야 합니다.
• 기여 3(생명주기 + 통합 컨텍스트 타입) → 이 두 차원을 하나의 프로그래밍 모델에 반죽해 넣습니다.
• 기여 4(Cordis + Koishi) → 이것이 정말로 돌아간다는 것을 증명합니다.

5. 핵심 정리

이번 과의 내용을 다섯 문장으로 압축하면:

1. 네 가지 기여는 하나의 사슬: 되돌릴 수 있는 효과→시간적 조합 가능성. 반응형 여효과→공간적 조합 가능성. 생명주기 + 통합 컨텍스트 타입→프로그래밍 패러다임. Cordis + Koishi→실현 검증.
2. Γ ⊢ t : T = 「타입 환경 Γ 아래에서, 항 t는 타입 T를 갖는다」. Γ는 「변수명 → 타입」의 스코프 표로, TypeScript 컴파일러가 마음속에 품고 있는 그 표와 같은 것입니다.
3. **효과 주석 T^effect**은 타입을 「반환값만 기록하는」 것에서 「부수 효과도 기록하는」 것으로 업그레이드합니다.
4. 효과 주석의 가치는 조합적 추론: f가 IO를 갖고 g가 순수함을 알면, f(g(x))가 IO를 갖는다고 단정할 수 있습니다——구현을 읽을 필요가 없습니다.
5. 두 차원, 두 방향: 효과 = 환경 변경 = 시간. 여효과 = 환경 의존 = 공간. Cordis는 이것들을 「컴파일 시점 정적 분석」에서 「런타임 동적 메커니즘」으로 업그레이드했습니다.

🚀 다음 과에서는 모나드를 다룹니다——이 절에서 언급한 IO, State, Maybe를 기억하시나요? 이것들은 모두 모나드의 인스턴스입니다. 효과 주석은 「타입 수준의 선언」이고, 모나드는 「런타임 수준의 상자」이며, 둘은 같은 것의 두 얼굴입니다.