곁가지 — "타입"이라는 말이 가리키는 층🔗

여기서 한 번 정리하고 가면 뒤가 편하다. 이 저장소를 읽다 보면 "타입"이라는 말이 서로 다른 것을 가리키며 여러 번 나오는데, 섞이면 §1.1과 §1.2의 구분 자체가 흐려진다.

지금까지 나온 것을 층으로 세워 보면 이렇다.

구문(syntax)          ⟨intexp⟩          구문 트리들의 집합
                          │
                          │  ⟦-⟧intexp    (트리를 받아 값을 계산하는 함수)
                          ▼
표시(denotation)      Σ → ℤ             상태를 받는 의미 함수
                          │  σ를 적용
                          ▼
값(value)             ℤ                 이 상태에서 얻은 값

⟨intexp⟩의 원소는 트리다. 1+1에 해당하는 원소는 c₊(c₁(), c₁())이라는 트리이지 정수 2 가 아니다. 트리를 정수로 보내는 것이 ⟦-⟧intexp이고, 그것이 §1.2에서 한 일이다.

Lean으로 옮기면 IntExp String이 위층이고 Int가 아래층이다. IntExp.eval이 화살표다. IntExp String을 "정수 타입"이라고 부르면 안 되는 이유가 그것이다 — 그 타입의 원소는 정수가 아니라 트리다.

타입이 붙은 언어로 가면 층이 하나 더 생긴다🔗

15장에서 타입 체계를 다루면 구문 쪽에 층이 하나 더 얹힌다. 타입 표현 int, bool, τ → σ 자체가 하나의 구문이 되고, 그 구문에도 자기만의 의미 함수가 붙는다.

타입의 구문     ⟨type⟩        int, bool, →, × 로 만들어지는 트리
                    │  ⟦-⟧type
                    ▼
타입의 의미     ⟦τ⟧            값들이 사는 그릇 (⟦int⟧ = ℤ)
                    △  값이 그 그릇 안에 있다
항의 의미       ⟦e⟧σ ∈ ⟦τ⟧
                    △  ⟦-⟧term
항의 구문       ⟨term⟩

여기서 자주 어긋나는 대응 하나를 짚어 둔다. ⟨intexp⟩와 같은 층에 있는 것은 ⟦τ⟧가 아니라 ⟨type⟩이다. 둘 다 구문의 집합이고, 둘 다 생성자와 세 조건으로 만들어지는 같은 종류의 대상이다. ⟨intexp⟩가 ⟦-⟧intexp를 거쳐 도달하는 곳이 ℤ = ⟦int⟧이고, 그쪽이 ⟦τ⟧에 해당한다.

Reynolds 1장을 억지로 타입이 붙은 언어로 다시 읽으면 이렇게 된다.

⟨intexp⟩

int 타입을 갖는 항들의 구문. 타입이 하나뿐이라 타입 표현을 따로 둘 이유가 없었다.

ℤ

⟦int⟧. 값들이 사는 그릇.

⟨assert⟩와 𝔹

같은 이야기의 진릿값 판이다. Reynolds의 𝔹는 실행 가능한 Bool 평가기를 뜻하지 않는다. 이 형식화는 객체언어의 양화를 Lean의 양화로 바로 옮기기 위해 Prop을 쓴다.

집합, 도메인, 범주론의 역할🔗

집합론, 도메인 이론, 범주론(category theory)은 같은 질문에 내놓은 세 가지 답이 아니다. 먼저 값이 어디에 사는지를 정한다.

집합론적(set-theoretic)

⟦τ⟧가 그냥 집합이다. ⟦int⟧ = ℤ, ⟦τ → σ⟧는 함수들의 집합. 1장이 이 관점이고, 비종료가 없으므로 이걸로 충분하다.

도메인 이론적(domain-theoretic)

⟦τ⟧에 근사 순서를 주고, 모든 가산 증가 사슬의 최소 상계와 최소원 ⊥을 갖추면 이 책이 말하는 도메인이 된다. 2장에서 while이 들어오면 이쪽으로 넘어간다. 보통 집합도 Option 같은 타입으로 비종료를 부호화할 수는 있다. 도메인의 순서와 연속성은 재귀 의미 방정식의 여러 고정점 가운데 최소 고정점을 골라 근사 사슬로 구성하게 해 준다.

도메인은 집합을 버리는 대안이 아니라 집합에 순서 구조를 더한 의미 공간이다. 범주론적 관점은 셋째 그릇이 아니다. 집합도 범주 Set의 대상이고, 도메인도 알맞은 범주의 대상이다. 범주론은 이런 대상과 그 사이의 함수를 한 언어로 설명한다. 예를 들어 Depth/SignatureFunctor.lean의 초기 대수는 여기서 구문을 재귀적으로 만드는 과정을 설명한다. 값이 사는 ⟦τ⟧까지 대신 정해 주지는 않는다.

Curry–Howard 대응도 여기서 선택할 의미론 하나를 더 보태는 말이 아니다. 명제를 타입으로, 증명을 그 타입의 항으로 읽는 대응이다. Assert.eval의 결과를 Prop으로 둔 직접적인 이유는 객체언어의 양화를 Lean의 ∀와 ∃로 그대로 표현하기 위해서다. 이 책은 1장에서 값을 보통 집합으로 다루고, 2장에서는 비종료와 재귀를 다루려고 근사 순서가 있는 도메인을 도입한다.

범주론 렌즈 — 의미는 유일한 준동형이다🔗

IntExp.eval과 Assert.eval은 구문 대수에서 이 절의 의미 대수로 가는 준동형 조건을 만족하는 유일한 함수 쌍이다(Depth/Algebra.lean의 초기성 정리). 그 조건 자체가 합성성 (compositionality)의 다른 이름이다 — 생성자 하나의 값이 그 조각들의 값으로만 정해지기 때문이다. 합성성의 귀결, 곧 뜻이 같은 부분구를 바꿔 끼워도 전체 뜻이 바뀌지 않는다는 성질은 선택 심화: 합성성과 합동에서 더 본다. 선택 심화: 의미와 자유 변수는 어떤 접기인가는 이 유일한 함수 쌍을 접기(catamorphism)로 직접 구성해 본다.