계산이 더 이상 함수 한 줄의 결과가 아니라, 동시에 살아 움직이는 여러 행위자의 합주가 될 때 무엇이 변하는가. 프로세스 계산은 그 합주의 악보를 적기 위한 가장 작은 문법이다.
람다 항이 묻는 질문은 "이 식의 값은 무엇인가"였다. 그러나 두 모듈이 동시에 돌고, 서로 신호를 주고받으며, 완료가 아닌 지속이 정상 상태인 시스템에서는 질문이 바뀐다. "이 시스템이 어떤 상호작용 패턴을 보이는가." 값 대신 행동(behavior)이 일등 시민이 되어야 한다. 프로세스 계산은 이를 위해 항을 버리고 프로세스 P, Q를 도입한다.
가장 단출한 어휘는 다음과 같다. 정지 프로세스 0, 액션 접두 a.P (먼저 a를 수행한 뒤 P로 진행), 병렬 합성 P ‖ Q, 비결정 선택 P + Q, 그리고 채널 이름 은닉 ν a. P. 액션 a는 송신 c⟨v⟩이거나 수신 c(x)이다. 동기 통신 규칙은 짝이 맞아 떨어졌을 때만 협주가 일어난다는 사실을 표현한다.
P —c⟨v⟩→ P′ Q —c(x)→ Q′P ‖ Q —τ→ P′ ‖ Q′[v/x]
여기서 τ는 외부에 보이지 않는 내부 동기이다. 외부 관찰자는 두 프로세스가 무언가 했다는 사실만 알고, 무엇을 주고받았는지는 모른다.
카페 C = order(x). brew⟨x⟩. 0과 손님 K = order⟨"라떼"⟩. 0을 C ‖ K로 합성하면 τ 한 번 뒤 brew⟨"라떼"⟩. 0이 남는다. 같은 카페에 두 손님이 동시에 줄을 서면 비결정성이 끼어든다. 누가 먼저 주문하느냐는 +가 아닌 스케줄링이 결정한다.
두 프로세스가 "같다"는 것은 무엇인가. 구문 동치는 너무 강하고, 종료 결과 비교는 종료가 없는 세계에서 의미가 없다. 답은 이중모의(bisimulation)이다. P ≈ Q는 P가 어떤 액션 a로 P′이 되면 Q도 같은 a로 Q′이 되며 P′ ≈ Q′이고, 그 역도 성립함을 뜻한다. 즉 두 프로세스는 외부 관찰자에게 구별 불가능하다. 이중모의는 합동 관계이며 동시성 정리들의 추론 도구가 된다.
순수한 프로세스 계산은 너무 헐벗었다. 우리는 함수도, 데이터 타입도, 가변 셀도 함께 쓰고 싶다. 동시성 알골은 명령형 알골 위에 채널과 병렬을 얹어 만든 하이브리드다.
실용 언어에서 동시성은 별개의 세계가 아니라 기존 표현식 안에 끼어든다. spawn(e)으로 새 프로세스를 띄우고, send·recv로 채널을 다루며, 그 모든 연산이 부수효과로 표현식의 평가에 섞여 든다. CA는 이를 위해 커맨드(command)라는 별도의 부호화를 두고, 표현식과 분리하지 않으면서도 효과의 자취를 타입에 새긴다.
타입 τ cmd는 "값을 돌려주는 동시성 작업"을 가리킨다. 핵심 구성자는 다음이다.
ret(e) : τ cmd, bnd(x.m₁; m₂) : τ cmd, spawn(m) : 1 cmd, send[c](e) : 1 cmd, recv[c] : τ cmd
채널 c : τ chan은 정적 선언으로 도입된다. 동기 의미론에서 send와 recv는 짝을 만나야 진행한다. 비동기 변형은 채널을 큐로 이해해 송신자를 차단하지 않는다. 두 의미론은 모두 작은 단계 전이로 정의되며, 전이의 라벨은 채널 액션을 외부에 노출시킬지 여부에 따라 달라진다.
요청 채널 req : task chan과 응답 채널 res : result chan이 있다고 하자. 워커는 본질적으로 μ. recv[req] ≫= λt. ret(do(t)) ≫= λr. send[res](r) ≫ μ의 무한 반복이다. 디스패처는 spawn(worker) ‖ spawn(worker) ‖ …로 풀을 만든다. CA의 매력은 이 모든 것을 타입이 잡힌 표현식으로 쓸 수 있다는 데 있다.
CA의 안전성 정리는 두 부분이다. 보존(preservation)은 어떤 전이가 일어나도 잘 타입된 프로세스 형상은 잘 타입된 형상을 낳는다는 것이다. 진행(progress)은 단일 스레드와 다르다. "막힌 채로 막혀 있는" 교착이 정상일 수 있다. 따라서 정리의 형태는 "잘 타입된 닫힌 시스템은 값으로 환원되거나, 외부 액션을 기다리는 형태이거나, 내부 τ로 한 걸음 갈 수 있다"가 된다. 즉 CA는 동시성을 합법화하면서도, 타입이 보장하는 안전 그물은 그대로 유지한다.
동시성은 같은 메모리 공간을 공유하는 여러 활동에 관한 것이지만, 분산은 다른 가정 위에 선다. 노드는 떨어져 있고, 통신은 비싸며, 어떤 자원은 그 노드를 떠날 수 없다. 타입은 그 사실을 안다.
DA의 출발점은 위치(site) w이다. 모든 표현식은 어떤 노드에서 실행되며, 어떤 값은 그 노드에 고정된다. 타입 τ@w는 "노드 w에 살고 있는 τ형 값"을 뜻한다. 함수 호출이 노드를 넘어가면 의미는 더 이상 단순한 베타 환원이 아니라 이주(migration) 또는 원격 호출이 된다.
핵심 구분은 어떤 값이 노드를 옮길 수 있는가이다. 정수는 어디든 갈 수 있다. 그러나 파일 핸들이나 잠긴 셀은 옮길 수 없다. DA는 이를 위해 이동 가능 타입(mobile type) 술어 τ mobile을 두고, 송신·수신은 이동 가능한 값에 한해서만 허용된다. 이동성은 구문이 아니라 의미적 보장이며, 타입 시스템이 그것을 정적으로 강제한다.
Γ ⊢ e : τ@w τ mobile Γ ⊢ w′ : siteΓ ⊢ at[w′](e) : τ@w′
데이터베이스가 db 노드에 있고, 로그 디스플레이가 ui 노드에 있다고 하자. db에서 무거운 질의를 돌려 요약된 결과만 ui로 보내는 패턴은 at[ui](recv(c))와 at[db](send(c, summarize(query())))로 표현된다. 핵심은 무거운 데이터가 채널을 넘지 않는다는 사실이며, 타입이 그것을 보증한다. 분산 시스템의 정설 "코드를 데이터에 보내라"가 타입 규칙으로 새겨진다.
DA의 안전성은 보존·진행 외에 위치 보존이 추가된다. τ@w로 타입된 값은 평가 후에도 정말로 w에 머문다. 부분 실패도 모형의 일부다. w 노드가 사라지면 at[w](e)는 정상 종료될 수 없으며, 이는 예외 또는 영구 차단으로 처리된다. 분산 알골이 가르치는 교훈은 단순하다. 위치는 부주의한 메타데이터가 아니라 타입의 일부여야 하며, 그래야만 시스템이 거짓말하지 않는다.
큰 프로그램은 작은 프로그램들의 그저 합이 아니다. 부품들 사이의 약속을 어떻게 정의하고, 어떻게 따로 만들고, 어떻게 함께 묶는가가 본질이다. 모듈은 약속의 단위이고, 링킹은 약속의 검증이다.
모듈을 따로 컴파일한다는 말은 두 가지를 동시에 의미한다. 첫째, 한 모듈을 작성·검사할 때 다른 모듈의 구현을 알 필요가 없다. 둘째, 합쳐진 결과는 모든 약속이 일관할 때만 정상 동작한다. 모듈 시스템은 이 두 가지를 형식화하기 위해 시그니처(signature)와 스트럭처(structure)의 구분을 도입한다. 시그니처는 약속, 스트럭처는 이행이다.
시그니처 σ는 일종의 인터페이스 타입이며, 스트럭처 M : σ는 그 인터페이스를 구현하는 항이다. 핵심 연산은 봉인(sealing)이다.
M ▷ σ ≡ "M을 σ로 가린다"
봉인 후에는 σ가 노출하지 않은 정의는 외부에서 볼 수 없다. 추상 타입은 시그니처에 type t로만 선언되고 스트럭처가 그것을 어떤 구체 타입으로 정의했는지는 봉인 너머로 새지 않는다. 이로써 표현 독립성이 정적으로 보장된다.
스택을 list로 구현한 StackL과 배열로 구현한 StackA가 있다고 하자. 둘 다 시그니처 STACK = sig type t; val empty : t; val push : … end로 봉인하면, 사용자는 t의 모양을 알 수 없고 두 구현은 치환 가능해진다. 링킹이란 사용 측의 빈자리에 어떤 봉인된 구현을 끼울지 결정하는 행위이며, 검사는 시그니처 매칭으로 환원된다.
모듈 시스템의 메타이론은 두 가지를 증명한다. 합성성: 각 모듈이 자기 시그니처를 만족하면, 링킹된 결과도 전체 시그니처를 만족한다. 정합성: 시그니처 매칭은 결정 가능하며, 추상 타입은 봉인 이후 외부의 어떤 항으로도 식별되지 않는다. 후자가 깨지면 모듈성은 이름뿐이다. 이후 장들은 이 정합성을 떠받칠 종류 시스템과 추상 메커니즘을 차곡차곡 쌓는다.
모듈을 다루다 보면 "이 추상 타입은 사실 저 타입과 똑같다"라고 잠깐 인정해야 할 때가 온다. 싱글턴 종류는 그 잠깐의 진실을 종류 수준에서 정확하게 새기기 위한 도구다.
모듈 시그니처가 type t를 추상으로 선언했다고 해도, 어떤 클라이언트는 M.t가 구체적으로 int임을 알면서 사용해야 할 수 있다. 봉인은 강한 추상이고, 투명한 어센션(transparent ascription)은 약한 추상이다. 둘을 통일된 틀에서 다루기 위해, 종류 시스템에 "이 종류는 단 하나의 타입만 포함한다"라는 진술을 더한다. 이것이 싱글턴 종류 S(τ)이다.
S(τ)와 서브카인딩S(τ)는 τ와 동일한 모든 타입을 원소로 가지는 종류이다. 즉 τ′ : S(τ)는 본질적으로 τ′ ≡ τ를 의미한다. 서브카인딩 κ₁ <: κ₂는 종류 사이의 포함 관계이다.
S(τ) <: T (싱글턴은 일반 타입 종류의 부분이다)
서브카인딩이 있는 까닭에 "정의가 노출된 타입"은 자연스럽게 "추상 타입"의 자리에 들어갈 수 있다. 반대 방향은 허락되지 않는다. 추상은 구체보다 일반적이다.
스트럭처 M = struct type t = int; … end를 시그니처 sig type t : S(int); … end로 어센드하면, 외부에서 M.t는 int와 동일하게 다뤄진다. 같은 스트럭처를 sig type t; … end로 봉인하면 M.t는 새 추상 타입이 된다. 같은 구현, 다른 시그니처, 다른 동등성. 싱글턴 종류는 이 차이를 종류 수준에서 일관되게 표현한다.
싱글턴이 들어오면 종류 동등성은 더 이상 구문 비교만으로 결정되지 않는다. η-확장과 싱글턴 단순화를 함께 다뤄야 한다. 핵심 결과는 결정 가능 동등성: 모든 잘 형성된 종류 판단은 알고리즘적으로 비교될 수 있다는 것이다. 이는 모듈 시스템의 타입 검사가 끝나는 검사가 되도록 보장한다. 싱글턴 종류는 표현력과 검사가능성 사이에서 외줄을 타는 우아한 균형이다.
"같은 인터페이스를 만족하는 여러 타입"을 다루는 두 전통이 있다. 모듈은 인터페이스를 명시적으로 끼워 넣고, 타입 클래스는 인터페이스를 암묵적으로 추론한다. 둘 다 표현력 있는 추상의 길이며, 한 뿌리에서 갈라진다.
타입 추상화의 가장 근본적인 형태는 존재 타입 ∃α. τ이다. "어떤 타입 α가 있어 그것이 τ를 만족한다." 모듈은 이 존재 타입을 이름이 있는 패킷으로 사용자가 직접 다루도록 한다. 타입 클래스는 같은 존재성을 컴파일러의 어깨 위에 얹는다. 사용자는 그저 "Eq α ⇒ α → α → bool"이라 적고, 어떤 사전(dictionary)이 들어갈지는 컴파일러가 찾아낸다.
타입 클래스 선언 class Eq α { eq : α → α → bool }는 본질적으로 사전 타입 Eq α = { eq : α → α → bool }이다. 인스턴스 선언 instance Eq int { eq = … }는 그 사전의 값을 제공한다. 다형 함수의 시그니처 (Eq α) ⇒ α → α → bool은 함수 화살표 앞에 사전 인자를 끼워 넣는 것과 같다.
(Eq α) ⇒ α → α → bool ↦ Eq α → α → bool
해법(resolution)은 컴파일러가 호출 지점의 α를 보고 적합한 인스턴스 사전을 자동으로 채워 주는 과정이다.
모나드 Monad m은 모듈로 쓰면 functor Monad(M : MONAD)가 되고, 타입 클래스로 쓰면 do 구문 뒤에 숨는다. 전자는 명시성과 일대다 인스턴스화를 허락하고, 후자는 간결함과 자동성을 준다. 어느 쪽이 우월한가는 잘못된 질문이다. 일관성(coherence) — 같은 타입에 대해 항상 같은 사전이 선택되는가 — 가 타입 클래스의 원죄이며, 모듈은 사용자에게 그 부담을 떠넘긴다.
타입 클래스의 메타이론은 전역 일관성을 핵심 정리로 둔다. 인스턴스 사전은 단 하나로 결정되어야 하며, 이는 인스턴스 중복을 막는 정적 규칙으로 보장된다. 또 하나의 결과는 번역(translation): 모든 타입 클래스 프로그램은 명시적 사전 전달 형태로 번역 가능하며, 두 형태는 등식적으로 동치이다. 즉 마법은 없다. 모든 암묵성은 컴파일 시점에 명시성으로 풀려 나간다.
모듈은 단지 큰 레코드가 아니다. 모듈이 모듈을 받아 모듈을 돌려주는 함수, 즉 functor가 있어야 비로소 모듈러리티가 합성성으로 자란다.
"순서가 있는 집합 위에 정렬을 구현하라." 이 한 줄은 매개변수화이다. 임의의 ORD 시그니처를 받아 SORT 시그니처를 반환하는 모듈 수준 함수 Sort(O : ORD) : SORT가 functor이다. functor는 약속 위에 약속을 쌓는다. 클라이언트는 어떤 ORD 인스턴스든 끼워 넣을 수 있고, 결과의 안전성은 functor의 시그니처가 보증한다.
functor 타입은 보통의 함수 타입과 다르다. 결과의 시그니처가 인자에 의존할 수 있기 때문이다. 이를 위해 종속 곱(dependent product) Π(X : σ₁). σ₂이 도입된다.
Sort : Π(O : ORD). SORT(O.t)
여기서 SORT(O.t)의 t는 인자 모듈 O의 타입 컴포넌트이다. 결과 시그니처가 인자의 타입을 참조한다. 이 의존성이야말로 functor가 단순한 일등 시민 함수와 구별되는 지점이다.
같은 인자로 functor를 두 번 적용했을 때 결과의 추상 타입이 같은가, 다른가? 적용성(applicative) functor는 같다고 답하고, 생성성(generative)은 다르다고 답한다. 적용성은 추론과 등식 추론이 매끄럽지만, 부수효과가 끼어 있을 때 의미가 흐려진다. 생성성은 매번 새 추상을 만들어 안전하지만, 같은 결과를 두 번 만드는 비용을 부른다. 실제 시스템은 둘을 섞어 쓴다. 순수 functor는 적용성, 효과를 가진 functor는 생성성으로.
functor의 합성, 즉 F ∘ G는 의존 시그니처를 정확히 따라가야 한다. 핵심 정리는 인장(seal) 보존: functor 본문에서 봉인한 추상 타입은 결과 모듈에서도 봉인되어 외부에 새지 않는다. 또한 매개변수성의 모듈 버전이 자연스럽게 따라온다. functor는 인자의 추상 타입에 대해 균일하게 동작해야 하며, 그 균일성이 모듈 계층 전체의 안전을 떠받친다. 작은 약속들의 덧셈이 큰 신뢰가 되는 곳, 그곳이 functor의 자리다.
언어 T는 자연수와 함수, 그리고 원시 재귀만 가진 단정한 세계이다. 모든 프로그램이 종료한다는 사실 하나로 등식 추론은 거의 자명해 보인다. 그러나 "거의"가 그 무게의 전부다.
두 항 e₁과 e₂가 같다는 말은 무엇인가. 가장 단순한 답은 관찰적 동치(observational equivalence): 어떤 프로그램 문맥 C[·]에 넣어도 같은 자연수로 평가된다. 이것이 정의로는 좋지만 증명에는 끔찍하다. 모든 문맥을 양화해야 하기 때문이다. 등식 추론의 임무는 이 정의와 실제로 다룰 수 있는 판정 시스템을 잇는 것이다.
Γ ⊢ e₁ ≡ e₂ : τ등식 판단은 베타·에타 규칙, 합동성, 그리고 원시 재귀의 풀어 쓰기 규칙으로 구성된다.
(λx.e)(e′) ≡ e[e′/x], λx. f x ≡ f (단 x ∉ FV(f)), rec(z; x.y.s; 0) ≡ z, rec(z; x.y.s; succ(n)) ≡ s[n, rec(…)/x, y]
이 규칙들은 평가 단계와 일치하지 않는 더 일반적인 등식까지 포함한다. 예컨대 λx. e의 본문이 닫혀 있다면 두 개의 다른 본문이 외연적으로 같은 함수일 수 있다.
add(0, m)과 add(m, 0)은 구문상 다르고, 한 단계 평가에서도 다르다. 그러나 모든 자연수 m에 대해 같은 결과를 낸다. T의 등식 추론은 이 사실을 외연성 원칙으로 인정한다. 함수에 대해서는 에타·베타로, 자연수에 대해서는 원시 재귀의 풀이로. 모든 프로그램이 종료하기에 외연성은 위험하지 않다. 무한 루프라는 함정이 없는 평지에서 수학은 본래 모습을 유지한다.
핵심 정리는 두 가지다. 건전성: Γ ⊢ e₁ ≡ e₂ : τ이면 e₁과 e₂는 관찰적으로 동치이다. 완전성(부분적): 닫힌 자연수 항에 대해서는 평가 결과가 같으면 등식이 도출된다. 함수 항에 대해서는 외연성 덕에 모든 인자에서 같다는 사실이 등식의 도출로 이어진다. T는 등식 추론이 가장 잘 작동하는 모범적 풍경이다. 다음 장에서 우리는 이 평지를 떠나 부분성의 산악 지대로 들어선다.
PCF는 fix를 가진 순간 종료를 잃는다. 그리고 종료를 잃는 순간 외연성은 더 이상 공짜가 아니다. 등식 추론은 이제 부분성과 정면으로 마주해야 한다.
모든 항이 종료하던 T에서는 "두 함수가 모든 인자에서 같다"가 안전한 진술이었다. PCF에서는 f x가 발산할 수 있다. 두 함수가 같다는 말은 이제 "값으로 환원되면 같은 값을 주고, 발산하면 둘 다 발산한다"가 된다. 관찰의 단위가 종료/비종료 여부까지 포함하도록 확장되어야 한다.
관찰 동치 e₁ ≅ e₂ : τ의 정의는 다음으로 다듬어진다. 모든 닫힌 문맥 C[·] : nat에 대해 C[e₁] ⇓ n이면 C[e₂] ⇓ n이고 그 역도 성립한다. 발산도 관찰이다. 등식 판단도 이에 맞춰 조정된다. 부동점 풀이 규칙은 다음과 같다.
fix(x.e) ≡ e[fix(x.e)/x]
그러나 이 한 번의 풀이만으로는 무한 행동을 비교할 수 없다. 최소 부동점을 다루기 위해 등식 추론은 승인 원리(admissibility)를 필요로 한다. 술어가 사슬에 대해 닫혀 있으면 부동점에서도 성립한다는 원리.
loop = fix(x.x)와 loop′ = fix(x. (λy.x) 0)은 모두 발산한다. 둘은 같은가? 답은 "그렇다, 모든 자연수 문맥에서 둘 다 같은 방식으로 발산한다." 이 단순한 사실을 등식 시스템이 직접 도출하기는 쉽지 않다. 구문 등식만으로는 무한 행동의 동치를 다 잡지 못하기 때문이다. 그래서 다음 장의 도구가 필요하다 — 논리적 관계.
건전성은 살아남는다. 등식 판단이 도출하는 모든 등식은 관찰 동치이다. 그러나 완전성은 무너진다. 관찰 동치이지만 구문 등식 시스템이 도출하지 못하는 짝이 존재한다. 이것은 결함이 아니라 풍부함의 증거이다. PCF의 의미론은 단순한 구문 변환보다 깊고, 그 깊이를 측정하려면 더 강력한 의미론적 도구가 필요하다. 다음 장의 주인공은 그 도구이다.
관찰 동치를 직접 다루는 것은 어렵다. 논리적 관계는 그것을 타입에 의해 유도되는 관계로 우회해 다룬다. 단순한 관계가 합성에 의해 풍부한 결과를 낳는 — 의미론의 가장 우아한 무기 중 하나.
핵심 발상은 단순하다. 타입 τ마다 관계 R_τ를 정의하되, 합성 타입에서는 부분 타입의 관계로부터 만들어 낸다. 자연수 타입은 동일성, 함수 타입은 "관계된 인자에 관계된 결과", 곱 타입은 성분별 관계. 관계는 타입 구조를 따라 자동으로 자란다.
R_nat(n, m) ⇔ n = m, R_(τ→σ)(f, g) ⇔ ∀(a, b). R_τ(a, b) ⇒ R_σ(f a, g b)
이 정의는 작은 베이스 케이스로부터 모든 타입 수준에 자동으로 의미를 부여한다.
논리적 관계의 운영 원리는 기본 정리(Fundamental Theorem)이다. 모든 잘 타입된 항 e는 자신과 관계된다. R_τ(e, e)가 항상 성립한다. 이것이 자명해 보이지만, 합성 타입의 정의에 따라 풀어 쓰면 강력한 결론이 따라 나온다. 함수에 대해 "어떤 두 관계된 인자에든 관계된 결과를 낸다"가 거저 얻어진다는 뜻이다.
첫째, 강한 정규화의 증명. R_τ를 "닫혀서 종료한다"로 풀이하면 모든 잘 타입된 항이 종료한다는 결과가 따른다. 둘째, 관찰 동치 분석. R_τ를 두 항 사이의 관계로 잡으면 관찰 동치를 의미론적으로 다룰 수 있다. PCF에서는 부동점 때문에 정의를 스텝 인덱스(step-indexed)로 정교화해야 하지만, 발상은 동일하다. 단순한 베이스 → 합성에 의한 자동 확장 → 강력한 결론.
논리적 관계의 한계는 참조나 존재 타입에서 드러난다. 가변 셀이 들어오면 시간이 흐르며 관계가 깨질 수 있고, 단순 정의로는 잡히지 않는다. 이를 위해 월드(world)나 스텝 인덱싱을 도입한 정교한 변형이 발전해 왔다. 그러나 모든 변형은 같은 영혼을 공유한다. 의미를 타입의 구조에 따라 짜라. 그 한 줄이 의미론의 절반을 낳았다.
다형 함수는 균일하게 행동해야 한다는 직관이 있다. 매개변수성은 그 직관을 정리로 바꾼다. 그리고 그 정리는 — 누군가의 표현을 빌리자면 — 타입을 보는 것만으로 정리를 거저 얻게 해 준다.
함수 f : ∀α. α → α가 있다. 이 함수의 행동을 우리가 무엇을 알 수 있는가? α가 무엇이든 같은 코드가 작동해야 하므로, f는 자신의 인자에 의존할 수밖에 없다. 인자를 변형할 어떤 도구도 가지고 있지 않다 — α가 무엇인지 모르기 때문이다. 결론은 강하다. f는 항등 함수일 수밖에 없다. 이것이 "타입이 정리를 낳는다"(theorems for free)의 가장 작은 사례이다.
매개변수성은 논리적 관계의 다형 버전이다. 타입 변수 α를 임의의 관계 R로 해석한다. 다형 타입 ∀α. τ의 해석은 "어떤 관계 R를 주든 결과가 τ에서 관계된다"이다.
R_(∀α. τ)(f, g) ⇔ ∀ R : Rel(A, B). R_τ[α↦R](f[A], g[B])
이 한 줄에서 모든 매개변수성 결과가 흘러나온다. 자유 정리, 추상 데이터 타입의 표현 독립성, 그리고 다형 인코딩의 정확성까지.
몇 가지 사례. f : ∀α. α list → α list이면 f는 원소를 만들어 낼 수 없으므로 결과는 입력 원소들의 어떤 재배열·삭제일 수밖에 없다. g : ∀α. (α → α) → α → α이면 g는 본질적으로 처치 수(Church numeral) 형태로, 입력 함수를 일정 횟수 합성한 것이다. 어떤 구체 코드를 보지 않고 타입만으로 이런 결론이 나온다. 매개변수성은 정적 분석의 비밀 무기이다.
매개변수성은 단순한 트릭이 아니다. 표현 독립성의 형식적 기반이다. 추상 타입 τ를 두 가지 다른 표현 τ₁과 τ₂로 구현해도, 그 두 구현이 적절한 관계로 묶여 있다면 클라이언트 코드는 차이를 알아챌 수 없다 — 그것이 매개변수성의 약속이다. 모듈성과 추상화의 메타이론이 결국 한 점에서 만난다. 다형성, 추상, 모듈은 같은 원리의 세 얼굴이다. 그 원리의 이름이 매개변수성이고, PFPL의 긴 여정이 마지막에 도달하는 산정상이다.