집합, 러셀의 역설, 타입 이론, 하스켈과 람다 계산, 처치 인코딩, 그리고 타입 시스템과 범주 사이의 관계를 그림과 함께 설명합니다.
이 장에서는 타입에 대해 이야기할 것입니다. 가능한 한 많은 새로운 범주에 대해 배우기를 기대했다면(그리고 뜻밖의 반전이 있기 전까지 그것들이 사실 범주라는 것조차 눈치채지 못했다면) 조금 실망할 수도 있습니다. 우리는 첫 장부터 이미 어떤 프로그래밍 언어에서의 타입의 범주에 대해 이야기해 왔고, 그것들이 어떻게 범주를 이루는지도 이미 알고 있습니다. 하지만 타입은 단지 프로그래밍 언어에만 관한 것이 아닙니다. 그리고 그것들은 그저 또 하나의 범주 이상입니다. 타입은 또한 _타입 이론_으로 알려진 수학 이론의 핵심에 놓여 있습니다.
타입 이론은 수학의 기초 언어로서 집합론의 대안이자, 범주론 자체의 대안이기도 하며, 그러한 형식 체계들 못지않게 강력한 도구입니다.
우리는 다시 집합 이야기를 시작했습니다. 범주론에 관한 대부분의 책들(그리고 일반적인 수학 책들)은 집합에서 시작하고, 종종 다시 집합으로 돌아갑니다. 이 책처럼 범주론에 관한 책에서도, 대부분의 수학적 대상에 대한 표준 정의는 집합을 포함합니다. 실제로 모노이드가 하나의 객체를 가진 범주라는 정의를 듣고 나면, 집합만 아는 사람은 이렇게 말할지도 모릅니다.
“그건 잊어버려! 집합 본 적 있지? 똑같은 건데, 거기에 이항 연산이 하나 더 있는 거야.”
또는 _순서_를 하나의 사상만 있는 범주라고 할 때는:
“집합 본 적 있지? 똑같은 건데, 어떤 원소는 다른 원소보다 더 큰 거야.”
이런 “집합 중심적” 관점이 널리 퍼진 이유는 사실 아주 단순합니다. 집합은 이해하기 쉽기 때문입니다. 특히 입문 자료에서 흔히 사용하는 개념적 수준에서 그렇습니다.
예를 들어 우리는 어떤 활동에 필요한 물건들을 한데 묶어 생각합니다. (예를 들어 수학 수업을 위한 각도기, 컴퍼스, _연필_이나, 그림을 그릴 때의 종이, 물감 통, _붓_처럼) 그래야 빠뜨리지 않기 때문입니다. 또는 자주 함께 어울리는 사람들을 이 모임, 저 모임으로 묶어 생각하기도 합니다. 그래서 몇몇 것들 주위에 동그라미를 그리면, 모두가 우리가 무엇을 말하는지 압니다.
하지만 집합에 대한 이런 초기 이해는 다소 _너무 단순_합니다. (수학자들은 이를 순진한 이해라고 부릅니다.) 왜냐하면 이를 자세히 들여다보면 해결하기 쉽지 않은 여러 역설로 이어지기 때문이며, 그중 가장 유명한 것이 러셀의 역설입니다.
러셀의 역설은 그 자체로도 흥미롭지만, 타입 이론이 만들어진 동기 가운데 하나이기도 하므로, 이 장은 그것이 어떻게 그리고 왜 발생하는지를 이해하는 것부터 시작하겠습니다.
우리가 본 대부분의 집합들(공집합이나 한 원소 집합 같은 것들)은 자기 자신을 포함하지 않습니다.
하지만 집합의 원소도 다시 집합이므로, 집합은 자기 자신을 포함할 수 있습니다.
바로 이 가능성이 러셀의 역설의 근본 원인입니다.
이 역설은 _자기 자신을 포함하지 않는 모든 집합의 집합_을 그려 보려 할 때 발생합니다. 원래의 집합 표기에서는, 자기 자신의 원소가 아닌 모든 집합을 포함하는 집합으로 정의할 수 있습니다.
하지만 이 그림에는 뭔가 잘못된 점이 있습니다. 정의를 보면, 방금 정의한 그 집합 자체도 자기 자신을 포함하지 않으므로 역시 그 안에 들어가야 한다는 것을 알 수 있습니다.
음, 이것도 어딘가 맞지 않습니다. 우리가 방금 한 수정 때문에, 이 집합은 이제 자기 자신을 포함하게 되었기 때문입니다.
그리고 그 집합을 다시 제거해서 자기 자신의 원소가 아니게 만들면 처음 상태로 돌아갈 뿐이므로, 어디로도 나아갈 수 없습니다. 이것이 바로 러셀의 역설입니다.
자기 자신을 포함하지 않는 집합들의 집합은 그다지 쓸모 있어 보이지 않습니다. 실제로도 그렇습니다. 사실 러셀의 역설을 만드는 경우 말고는 다른 이유로 언급되는 것을 본 적이 없습니다. 그래서 대부분의 사람들은 러셀의 역설을 처음 배우면 대략 이렇게 반응할 것입니다.
“잠깐, 그냥 자기 자신을 포함하지 않는 집합들의 집합은 그릴 수 없다고 규칙을 추가하면 안 돼?”
바로 이것이 수학자 에른스트 체르멜로와 아브라함 프렝켈이 하려고 했던 일이었습니다. (말장난 의도는 없습니다.) 그리고 그들이 추가한 규칙들은 체르멜로-프렝켈 집합론 또는 ZFC(_C_는 또 다른 이야기입니다)로 알려진 새로운 집합론 정의로 이어졌습니다. 이것은 역설이 없는 집합론의 한 버전입니다. ZFC는 성공적이었고 오늘날에도 여전히 사용되지만, 집합이 가진 가장 좋은 특징 가운데 하나, 즉 _단순함_을 일부 포기하게 만듭니다.
무슨 뜻일까요? 원래의 집합론 정식화(오늘날 순진한 집합론이라고 부르는 것)는 단 하나의(다소 모호한) 규칙/공리 위에 세워졌습니다. “성질 P가 주어지면, 그 성질을 가진 모든 대상을 포함하는 집합이 존재한다.” 즉, 어떤 대상들의 묶음이든 집합을 이룰 수 있다는 것입니다.
반면 ZFC는 더 많은 수의(그리고 더 제한적인) 공리들로 정의됩니다. 예를 들어 _짝짓기 공리_는 임의의 두 집합이 주어지면 그것들을 원소로 포함하는 집합이 존재한다고 말합니다.
…또는 _합집합 공리_는 두 집합이 있으면 그 둘의 모든 원소를 담은 집합도 있다고 말합니다.
이런 공리들은(이론의 버전에 따라) 대략 8개 정도 있습니다. 이것들은 흥미로운 모든 집합을 만들 수 있도록, 그러나 악명 높은 자기 자신을 포함하는 집합은 만들 수 없도록 세심하게 정리되어 있습니다. 하지만 ZFC를 받아들인다는 것은 집합론이 겉보기만큼 단순하고 직관적이지 않다는 점도 받아들인다는 뜻입니다.
실제로 그것은 범주론보다 더 복잡하고, 잠시 후 배울 또 다른 이론보다도 더 복잡합니다…
체르멜로가 러셀의 역설을 피하기 위해 집합론의 공리들을 다듬고 있을 때, 러셀 자신은 자신의 역설을 해결하기 위해 다른 길을 택했습니다. 그는 아예 집합을 버리고, 설계 자체로 역설이 없는 완전히 새로운 수학적 개념을 만들기로 했습니다. 즉, 비논리적인 구성을 피하려고 추가 공리로 덧대지 않아도 되는 개념 말입니다. 그렇게 해서 1908년, 체르멜로가 ZFC의 첫 번째 버전을 발표한 바로 그 해에, 러셀은 자신의 _타입 이론_을 내놓았습니다.
타입 이론은 집합론과 전혀 비슷하지는 않지만, 동시에 완전히 다르지도 않습니다. _타입_과 _항(term)_의 개념은 _집합_과 _원소_의 개념을 분명히 떠올리게 하기 때문입니다.
| Theory | Set theory | Type Theory |
|---|---|---|
| Element | Term | |
| Belongs to a | Set | Type |
| Notation | a∈A | a:A |
둘 사이의 가장 큰 차이는 _구조_의 측면에서, 항은 자기 타입에 묶여 있다는 점입니다.
그래서 집합론에서는 하나의 원소가 여러 집합의 원소가 될 수 있지만
타입 이론에서는 하나의 항은 오직 하나의 타입만 가질 수 있습니다. (작은 원 안의 빨간 공과 큰 원 안의 빨간 공은 서로 다른 것이라는 점에 주의하세요.)
이 법칙 때문에 타입은 자기 자신을 포함할 수 없고, 따라서 러셀의 역설은 완전히 피할 수 있습니다.
이 법칙은 다소 이상하게 들릴 수 있습니다. 예를 들어 항은 하나의 타입에만 속할 수 있으므로, 타입 이론에서 자연수 1은 로 표기되며, 이것은 정수 1(로 표기되는)과는 완전히 다른 객체입니다.
하지만 첫 장에서 배운 상(image) 함수를 사용하면 값의 한 버전을 다른 버전으로 언제든 변환할 수 있다는 것을 깨닫고 나서야 어느 정도 말이 되기 시작합니다.
곧 보게 되겠지만, 타입의 개념은 함수의 개념과 아주 깊은 관련이 있습니다.
“모든 명제 함수 φ(x)는—이렇게 주장된다—진리값의 범위에 더해 의미의 범위도 가진다. 즉, φ(x)가 참이든 거짓이든 애초에 명제가 되려면 x가 놓여 있어야 하는 범위가 있다. 이것이 타입 이론의 첫 번째 요점이다. 두 번째 요점은 의미의 범위들이 타입을 이룬다는 것이다. 즉, x가 φ(x)의 의미 범위에 속한다면, x의 _타입_이라 불리는 객체들의 부류가 있고, 그 모든 것도 φ(x)의 의미 범위에 속해야 한다.” — Bertrand Russell - Principles of Mathematics
앞 절에서 우리는 타입을 “집합과 비슷하지만…”이라고 설명할 뻔했습니다. (예를 들어 집합과 비슷하지만 항은 오직 하나의 타입에만 속한다는 식으로요.) 하지만 기술적으로 맞을지는 몰라도, 그런 설명은 전혀 적절하지 않습니다. 타입은 집합의 대안으로 시작했지만, 실제로는 상당히 다른 것으로 발전했기 때문입니다. 그러므로 집합의 관점으로 생각해서는 멀리 갈 수 없습니다. 실제로 앞 절의 비유적 집합론자에게 타입에 대해 물으면, 솔직한 대답은 이래야 할 것입니다.
“집합 본 적 있지? 음, 그거랑은 아무 상관도 없어.”
그러니 타입 이론을 그 자체로 어떻게 정의하는지 봅시다.
하지만 먼저…
시작하기 전에, 이 긴 주의사항부터 치우고 갑시다.
방금 우리는 “type theory”나 “the type theory”가 아니라 a type theory라고 말했습니다. 이는 타입 이론의 서로 다른(하지만 관련 있는) 정식화가 하나가 아니라 여러 개 있으며, 혼란스럽게도 그것들을 모두 type _theories_라고 부르기 때문입니다. (덜 혼란스럽게는 _type systems_라고도 부릅니다.) 예를 들어 _Simply-typed lambda calculus_나 Polymorphic Lambda calculus 같은 것들입니다. 그래서 a type theory라고 말하는 것이 맞습니다.
충분히 헷갈리셨나요? 아직도요?
어떤 문맥에서는 “type theory”라는 말이, 범주론이 범주를 연구하듯이, 타입 이론 전체 분야를 가리키기도 합니다. 하지만 (숨 한 번 크게 쉬고) 서로 다른 타입 시스템들을 “타입 이론의 여러 버전”처럼 생각할 수도 있으므로, 모든 타입 시스템에 공통적인 어떤 기능 집합을 말할 때 사람들은 “type theory”라는 말을 그런 기능을 가진 아무 타입 시스템이나 가리키는 뜻으로 쓰기도 합니다.
어쨌든 다시 주제로 돌아갑시다. (뭐라고 부르든 간에 말입니다.) 앞서 말했듯이, 타입 이론은 러셀이 흥미로운 객체들의 모음을 모두 정의하면서도, 실수로 우리를 잘못된 길로 이끄는 모음(예를 들어 그의 이름이 붙은 역설로 가는 것)을 정의하지 않고, 또 ZFC처럼 수많은 추가 공리를 만들어내지 않기 위한 방법을 찾는 과정에서 탄생했습니다.
그는 많은 생각을 했고(적어도 저는 그랬으리라 상상합니다), 모든 조건을 만족하는 형식 체계를 고안해냈습니다. 그 바탕에는 혁명적인 새 아이디어가 있었는데… 기본적으로는 범주론의 핵심에도 있는 바로 그 아이디어입니다. (왜 그가 범주론의 선구자로 인정받지 못했는지 모르겠습니다.) 그 아이디어는 다음과 같습니다. 우리가 애초에 이야기하고 싶은 흥미로운 모음이란 _함수의 출발점과 도착점이 되는 모음_이라는 것입니다. 그래서 이렇게 말할 수 있습니다.
타입이란 화살의 출발점이거나 도착점이 될 수 있는 어떤 것이다.
(정의를 더 일반적으로 만들기 위해 더 일반적인 용어인 “화살”을 쓰지만, 지금은 화살을 함수라고 생각해도 좋습니다.)
다시 자기 자신을 포함하지 않는 모든 집합의 집합을 생각해 봅시다. 이것은 러셀의 역설을 일으키는 것 외에는 별로 쓸모가 없습니다. (역설을 일으키는 것을 쓸모 있다고 친다면 또 모르지만요.) 더 파고들어 보면 결국 이유를 알게 됩니다. 다른 어떤 집합에서 이 집합으로 가는 (흥미로운) 함수가 없으므로, 어디에서도 거기로 갈 수 없습니다. 반대로 그 집합에서 다른 어디로도 갈 수 없습니다. (그것이 출발점인 함수도 없습니다.) 이 집합은 사막 한가운데의 오아시스 같기도 하고… 아니면 큰 오아시스 한가운데의 작은 사막 같기도 합니다… 더 좋은 비유가 떠오르면 알려 주세요.
우리는 타입 이론이 _만들어내는 구조_라는 점에서는 집합론과 그리 다르지 않다는 것을 보았습니다. 모든 타입은(적어도 첫 단계에서는) 집합이지만, 모든 집합이 타입인 것은 아닙니다. 그리고 모든 함수는… 음, 함수입니다. 하지만 _그 구조가 생겨나는 방식_이라는 점에서 타입 이론은 집합론과 아주 다릅니다. 이는 직관주의 논리가 고전 논리와 다른 것과 비슷합니다. (그런데 만약 이 비유 때문에 타입 이론과 직관주의 논리의 연결이 너무 뻔해졌다면, 부탁이니 우리가 나중에 그것을 명시적으로 말할 때는 놀란 척해 주세요.)
집합론에서는(특히 순진한 버전에서는) 가능한 모든 집합과 함수가 처음부터 이미 다 존재합니다. 마치 플라톤적인 이데아의 세계처럼 말입니다. 우리가 하는 일은 그중 관심 있는 것들을 탐험하는 것뿐입니다.
타입 이론에서는 비어 있는 공간에서 시작합니다.
[diagram omitted]
거기서부터 우리는 타입을 만들어야 합니다. 하나씩. 맨손으로. (좋아요, 우리를 도와주는 멋진 수학적 도구들이 있긴 합니다.)
“일반적으로 우리는 데이터를 어떤 선택자와 생성자의 모음으로 정의된 것으로 생각할 수 있으며, 더불어 그러한 절차들이 유효한 표현이 되기 위해 충족해야 하는 조건들이 지정된다.” — Harold Abelson, Gerald Jay Sussman, Julie Sussman — Structure and Interpretation of Computer Programs
구체적인 타입 구성 공식을 소개하기 전에, 일반적인 아이디어를 조금 더 설명하고 싶습니다. 앞 절에서 우리는 이렇게 말했습니다.
타입이란 화살의 출발점이거나 도착점이 될 수 있는 어떤 것이다.
이 정의는 조금 모호하게 보일 수 있지만, 컴퓨터 프로그래밍에서 타입이 어떻게 정의되는지 보면 자명해집니다. 전통적인 명령형 언어의 관점에서 보더라도, 타입의 정의는 함수(더 일반적으로는 화살)를 구성하는 규칙들을 정의하는 것으로 이루어진다는 점이 분명합니다.
class MyType<A> {
a: A;
constructor(a) {
this.a = a;
}
getA() {
return this.a;
}
}
어떤 종류의 규칙일까요? 크게 세 부류로 나눌 수 있습니다.
우선 타입에는 그것이 무엇인지 명시하는 _정의_가 있어야 합니다. 이 화살은 우리가 값 수준에서 생각하는 화살과는 다르다는 점에 주의하세요. 이것은 한 타입에서 다른 타입으로 가는 값 수준의 화살이 아니라, 타입들의 한 범주에서 다른 범주로 가는 타입 수준의 화살입니다. 이것을 _타입 형성 규칙_이라고 합니다.
다음으로, 새로운 타입을 향해 적어도 하나의 화살이 있어야 합니다. 이것을 _항 도입 규칙_이라고 합니다. (“항”은 “값”을 뜻하는 말입니다.) 프로그래밍에서는 _생성자_라고 부르며, 이것은 값 수준의 화살입니다. (예를 들어 함수입니다.)
마지막으로, 단지 새로운 타입을 만들기 위해 타입을 만드는 것은 원하지 않으므로, 이 새 타입에서 나오는 화살도 적어도 하나 있어야 합니다. 이것 역시 값 수준의 화살(함수)이며, _항 제거 규칙_이라고 부릅니다. (마치 그 타입을 메서드의 결과로 치환하여 제거하는 것처럼 말입니다.)
요약하면
타입은 다음 세 화살을 정의함으로써 정의된다:
- 하나의 타입 수준 화살(타입 형성).
- 그 타입이 도착점인 값 수준 화살을 적어도 하나(항 도입).
- 그 타입이 출발점인 값 수준 화살을 적어도 하나(항 제거).
좋습니다. 실제로 타입 이론을 정의하지도 않고 타입 이론을 정의하려고 너무 멀리 온 것 같네요. 그러니 이제 공식으로 넘어가겠습니다… 두 번째 긴 주의사항 뒤에요.
첫 번째 긴 주의사항에서 말했듯이, 타입 이론은 하나가 아니라 여러 개입니다. 따라서 타입 이론을 하려면 먼저 하나의 타입 이론을 골라야 합니다. (이 문장이 헷갈리면 첫 번째 주의사항을 다시 읽으세요.)
타입 이론(혹은 타입 시스템이라고 해도 좋겠습니다)을 고른다는 것은, 그 이론을 어떤 _언어_로 기술할지도 고른다는 뜻입니다. 언어라는 말을 들으면 프로그래머들은 TypeScript나 Java 같은 기능이 풍부한 대중적 프로그래밍 언어를 떠올릴 것입니다. 반면 _타입 이론가들_의 취향은 다릅니다. 그들은 언어 자체보다 타입 시스템에 관심이 있기 때문에 기능에는 별로 신경 쓰지 않으며, 그래서 대부분이 택하는 언어는 존재 가능한 한 가장 단순하고 최소한의 언어, 즉 _람다 계산_입니다. 들어본 적이 없다면, 이것은 (익명) 함수만 있고 다른 것은 아무것도 없는 언어입니다.
양쪽을 모두 만족시키기 위해서 (그리고 동시에 양쪽을 모두 약간 짜증 나게 만들기 위해서), 우리는 그 중간쯤 되는 언어, 즉 _Haskell_의 (일부분)을 사용하겠습니다. 이론적으로는 큰 차이가 없습니다. Haskell은 람다 계산에 기반하기 때문입니다. 다만 프로그래머들에게는 더 쉬울 것입니다. 람다 계산은 함수만 있지만, Haskell은 곱 생성자를 원시적으로 정의할 수 있습니다. (형식적인 관점에서는 이 역시 큰 차이가 없습니다. 커링과 언커링을 통해 곱과 함수 사이를 쉽게 오갈 수 있기 때문입니다.)
또 하나, 마지막으로 아주 중요한 점은 Haskell의 생성자와 함수에는 이름을 붙일 수 있다는 것입니다. (믿으세요, 이건 도움이 됩니다.)
우리가 Haskell을 택했으므로, Haskell의 타입 이론/타입 시스템 안에서 작업하겠습니다. 이것은 1972년 Jean-Yves Girard가 발견한 타입 시스템으로, Polymorphic Lambda Calculus 또는 _System F_라고 불립니다.
우리는 아무것도 정의되지 않은 빈 공간에서 시작합니다. 단 하나, Haskell에서 타입이라고 불리는 싱글턴 타입만은 예외입니다.
오직 하나의 값만 가지는 타입으로, 이것을 시작점으로 사용할 수 있습니다.
타입 ()는 하나의 값을 가지는 타입이다.
사실 설명하기가 그리 쉽지 않은 전제조건이 하나 더 있습니다. 바로 객체의 각 쌍에 대한 화살 타입, 즉 Lambda 타입입니다. 람다 계산에서는 타입 사이의 화살도 역시 타입입니다. (프로그래밍 문맥에서는 때때로 “first-class functions”라고 부르는 특징입니다.)
임의의 타입 와 에 대해, 라는 타입이 있으며, 이것을 와 의 Lambda 타입이라고 하고, 와 를 잇는 모든 화살을 값으로 가진다.
여기서는 더 자세히 들어가지 않겠습니다. Lambda 타입은 이전 장에서 정의한 직관주의 논리의 함의 객체와 똑같은 방식으로 정의되고 작동하기 때문입니다. 그리고 곧 알게 되겠지만, 역할도 같습니다.
출발점이 생겼으니 몇 가지 타입을 정의할 수 있습니다. 어떻게 할까요? 불리언 같은 기초 타입부터 시작해 봅시다. 이런 경우 과정은 아주 단순합니다. 그 값들을 그냥 곧바로 나열하면 되기 때문입니다.
이 정의를 따라가 봅시다.
먼저, 는 “Bool”이라고 부르는 타입이 존재한다고 말합니다.
그다음, 는 “ 는 불리언이다”라고 말합니다. 즉, 방금 만든 새 데이터 타입에 값 하나를 추가합니다. 그림에서는 이를 Haskell의 타입이라 불리는 싱글턴 타입에서 오는 화살로 나타낼 것입니다. 이는 2장에서 본 집합 범주의 기초 이론에 따른 것입니다.
그리고 는 또 하나의 그런 값을 만듭니다.
짜잔, 우리는 방금 타입 하나를 정의했습니다!
잠깐, 방금 말은 취소하겠습니다. 사실 아직 타입을 정의한 것이 아닙니다. 아니, 정의하긴 했지만 꽤 쓸모없는 타입입니다. 적어도 하나의, 이 타입에서 나오는 화살을 정의해야만 유용해지기 때문입니다. (그렇지 않으면 일방통행일 뿐입니다.) 불리언의 경우, 이 함수는 보통 라고 부릅니다.
Haskell의 함수 정의는 꽤 단순하다는 것을 볼 수 있습니다. 그저 한 타입의 각 값을 다른 타입의 값에 하나씩 대응시키면 됩니다.
아래는 이 함수를 사용한 몇 가지 식과 그 반환값입니다. (--는 Haskell의 주석 문법입니다.)
ifElse True 1 2 --1
ifElse False 1 2 --2
하지만 왜(반복이 될 위험을 무릅쓰고 묻자면) 바로 이 타입이 반드시 불리언 타입이어야 할까요? 뭐든 자기 방식대로 하고 싶어 하는 동료 Bobby가 자기만의 Bool 버전을 정의해서 프로젝트에서 쓰는 것을 막는 게 무엇일까요?
대답은 “아무것도 없다”입니다. 하지만 그건 큰 문제가 아닙니다. 그들의 Bool을 우리의 Bool로 바꾸는 함수를 하나 뚝딱 만들면 되니까요.
이 함수는 되돌릴 수도 있습니다. 즉, 두 타입은 동형입니다. 다시 말해, 유일한 동형사상까지 고려하면 둘은 같은 타입입니다.
깜빡할 뻔했네요. 불리언을 만들었던 것과 같은 방식으로, 공들의 타입 같은 다른 유한한/기초 타입도 만들 수 있습니다.
이제 Haskell에서 로 알려진 타입을 정의하겠습니다. (다른 언어들에서는 보통 이라고 부릅니다.) 처음 본다면 Haskell 문서에 아주 좋은 설명이 있습니다.
The Maybe type encapsulates an optional value. A value of type Maybe a either contains a value of type a (represented as ), or it is empty (represented as ). Using is a good way to deal with errors or exceptional cases without resorting to drastic measures such as error.
하지만 읽는 법만 익히면, 타입 정의 자체만으로도 충분히 분명합니다.
는 와 꽤 비슷해 보이지만, 와 달리 는 다형 타입입니다. _타입 형성 규칙_을 보면 알 수 있습니다.
Maybe는 다형적입니다. 즉, 하나만 있는 것이 아니라 타입 a마다 하나씩 많은 가 있습니다. 예를 들어 타입을 예로 들어 봅시다. 가 타입이므로, (이 규칙에 따라) 역시 타입입니다.
다형 타입은 타입들의 우주에서 자기 자신으로 가는 화살입니다. (즉 의 kind는 입니다.) 반면 는 그냥 입니다.
이제 타입을 채울 차례입니다.
첫 줄은 불리언에서 본 것과 비슷합니다.
이것은 모든 타입에 대해 라는 값이 있다고 말합니다. (이것이 의 뜻입니다. “모든”이라는 뜻이지요.)
물론 모든 가 똑같기만 하다면 여러 개 있을 이유가 없겠지요. 그래서 두 번째 줄이 나옵니다.
생성자 는 타입 에서 타입 로 가는 화살을 나타냅니다. 예를 들어 에서 로 가는 화살입니다.
이 타입은 오류를 다루는 데, 즉 _부분 함수_를 정의하는 데 사용됩니다. 출발점의 모든 값에 대해 화살이 존재하지 않는 함수를 정의하고 싶다고 합시다. 그렇다면 이런 함수는 정의할 수 없다는 뜻일까요?
아닙니다. 도착 타입을 로 감싸기만 하면 보통 함수가 됩니다.
마무리를 위해, maybe 타입을 분해/제거하는 함수 하나를 정의합시다. 즉, 그 안의 기반 타입을 다른 것으로 바꾸는 함수를 이용해 다른 무언가로 변환하는 것입니다.
이 함수는, 함수 와 타입 의 값이 주어졌을 때, 타입 에서 임의의 타입 로 가는 화살을 정의한다는 점에 주목하세요.
처음 수학을 배울 때는 압도적으로 느껴질 수 있습니다. 이렇게 거대하고, 심지어 무한한 지식의 몸체를 도대체 어떻게 배워야 할지 모를 수 있으니까요. 그런데 답은 의외로 단순합니다. 처음에는 0가지를 알고 시작합니다. 그런 다음 이론 1개를 배웁니다. 축하합니다. 첫 번째 이론을 배웠고, 이제 총 1개의 이론을 알게 되었습니다. 그 다음 이론을 하나 더 배우면 총 2개의 이론을 알게 됩니다. 또 하나, 또 하나 배우다 보면, 충분한 시간과 노력을 들여 결국 모든 이론을 배울 수도 있을 것입니다.
이 논리는 수학 이론뿐 아니라 “셀 수 있는” 모든 것에 적용됩니다. 이것이 자연수의 수학적 정의의 기초이기 때문이며, 19세기에 이탈리아 수학자 Giuseppe Peano가 유명하게 정리했습니다.
혹은 Haskell 사람들은 이렇게 말합니다.
화살을 따라가 봅시다.
첫 줄은 자연수 타입이 일반적인 비다형 타입, 또는 “단형” 타입임을 나타냅니다.
첫 번째 규칙도 단순합니다.
이 규칙은 zero라고 부르는 값 하나를 만들 수 있게 해 줍니다.
즉, 이것은 페아노의 첫 번째 공리를 거의 말 그대로 반복한 것입니다.
- 는 자연수이다.
두 번째 규칙은 더 흥미롭습니다.
이것은 “Successor”(또는 우리가 흔히 +1이라고 부르는 것)라는 생성자가 있다고 말합니다. 즉, 이것은 다음과 같은 것의 대응물입니다.
- 가 자연수이면, 는 자연수이다.
는 자연수 타입에서 자기 자신으로 가는 화살입니다. 즉, 자연수 하나가 주어지면 또 다른 자연수를 만듭니다.
하지만 지금 자연수 타입의 항(값)은 단 하나, 뿐입니다. 화살을 그려서 또 하나를 만들면, (어떤 문맥에서는 라고도 알려진) 값이 생깁니다.
이제 값이 하나 더 생겼으므로, 화살도 하나 더 그려야 합니다. 이번 결과는 , 즉 2입니다.
이런 식으로, 끝없이, 값들의 사슬을 계속 만들어 갑니다.
흠, 이 표기는 좀 투박하네요. 이런 값을 더 잘 나타낼 방법이 있으면 좋겠는데… 아, 있군요.
이것이 바로 귀납적 타입(또는 재귀적 타입이라고도 할 수 있습니다)을 정의하는 방법입니다.
잠깐, 제거 규칙도 있었죠. 저는 늘 제거 규칙을 잊습니다. 여기 있습니다.
이것은 예를 들어 우리의 Nat를 일반 Haskell Nat로 변환할 수 있게 해 줍니다.
foldNat (Succ (Succ Zero)) 0 (+ 1) -- 2
자연수를 다른 타입으로 바꾸는 다른 모든 표준 함수도 이 제거 규칙을 사용해 정의할 수 있습니다.
타입의 풍경은 합성 타입 없이는 정말… 평평한 곳이 되었을 것입니다. 이것들은 다른 타입의 여러 값을 하나로 묶을 수 있게 해 주는 타입들입니다.
궁극의 합성 타입은 리스트입니다. 특히 연결 리스트 는 정말 아름답습니다.
하나씩 풀어 봅시다.
타입 형성 규칙은 가 ( 처럼) 합성 타입이라고 말합니다.
즉 타입이 하나만 있는 것이 아니라, 같은 여러 타입이 있다는 뜻입니다. (리스트의 리스트(의 리스트)를 생각하면 무한히 많습니다.) 이것들은 보통 “자연수의 리스트”, “불리언의 리스트” 등으로 읽습니다.
이제 생성자들을 봅시다. 첫 번째는 정적인 값 하나를 정의하는데, 각 리스트마다 하나씩 있으며 빈 리스트를 나타냅니다.
이 값을 라고 부르겠습니다. (기본 Haskell 리스트는 [] 기호를 씁니다.)
이제 더 흥미로운 부분으로 갑시다. 는 두 번째 항 도입 규칙인데, ( 는 construct의 줄임말입니다) 값 를 리스트에 추가하고 그 리스트를 돌려주는 연산으로 볼 수 있습니다.
첫눈에 보면 는 앞서 본 귀납 생성자와 꽤 비슷해 보입니다. 실제로 처럼, 도 무한히 많은 항을 만들어내는 귀납적/재귀적 생성자입니다.
하지만 시그니처가 인 와는 달리, 는 시그니처를 가집니다. 즉 타입 의 모든 값마다 리스트 생성자가 하나씩 있습니다. 를 다른 화살을 가리키는 화살로 시각화할 수 있습니다.
어째서 다른 화살에서 나오는 화살을 가질 수 있을까요? 아마 여기서 다시 상기할 때가 된 것 같습니다. 람다 계산에서는 타입 사이의 화살도 타입입니다.
그러니 이 화살들을 그려 봅시다. 기초 값 에서 시작합니다.
말했듯이, 이 타입은 귀납적입니다. 즉, 그리는 모든 화살이 더 많은 화살을 생성합니다. (여기서는 그중 일부만, 즉 주황색 공에서 나오는 것들만 그립니다.)
그 결과 생기는 타입의 값들은… 음, 다른 값들의 _리스트_입니다.
이제 항 제거 규칙을 써 봅시다.
이 규칙은 리스트를 다루는 데 가장 유용한 함수이기도 합니다.
Task 1: 에서 로 가는 특정한 대응이 하나 있는데, 너무도 유용해서 어떤 Lisp 방언들은 아예 타입이 없고 이 대응에만 의존합니다. 그려 보세요.
Task 2: Haskell에서 이 대응(List와 Bool 사이)을 정의해 보세요. 하나는 처음부터 함수를 직접 써서 정의하고, 두 번은 foldList 함수를 써서 정의해 보세요.
f :: (Bool -> a -> Bool)
f = undefined
foldList f False
Task 3: 타입 를 소개합니다. 여기서 는 싱글턴 타입, 즉 (값이 하나뿐인 타입)입니다. 공간이 허락하는 데까지 의 값들을 그려 보세요.
Task 4: 타입 는 사실 여기서 살펴본 다른 어떤 타입과 동형입니다. 무엇인지 찾아보세요.
이제 두 가지 타입을 아주 빠르게 더 소개하겠습니다. (흠… 왠지 저것들은 전에 본 적이 있는 것 같군요.)
타입 는 흥미로운 타입입니다.
이것은 두 타입 와 에 의해 매개변수화되는 타입이며, 두 개의 생성자/항 도입 규칙을 가집니다. 하나는 라는 생성자로, 값을 받아들이고, 다른 하나는 라는 생성자로 값을 받아들입니다. 아래는 Either의 정의입니다. (항 제거 규칙은 제외합니다.)
다음으로 소개할 타입은 타입입니다. 이것 역시 와 에 의해 매개변수화되지만, 그 각 값은 값과 값을 둘 다 포함합니다.
여기서는 다른 방식을 취해 보겠습니다. 정의 대신 곧바로 타입 제거 규칙을 제시하겠습니다.
Task 5: Tuple의 생성자를 작성하세요. Either의 fold 함수를 작성하세요.
타입 는 그것의 도입 규칙에 의해 유일하게 정의됩니다. 즉, 제거 규칙은 도입 규칙으로부터 유도할 수 있습니다.
반면 는 제거 규칙에 의해 정의됩니다. 즉, 도입 규칙은 그것들로부터 유도할 수 있습니다.
처럼 도입 규칙으로 정의되는 타입을 _양의 타입_이라고 합니다. 제거 규칙으로 정의되는 타입은 _음의 타입_입니다. 지금까지 본 타입들 가운데 ( 을 제외하면) 모두 양의 타입입니다.
양의 타입과 음의 타입은 서로 쌍대입니다.
양의/음의 타입은 범주론의 극한/쌍극한 개념에 대응하지만, 그것은 나중에 더 배울 것입니다.
Task 6: 말고도 아주 중요한 음의 타입이 하나 더 있는데, 우리는 이미 이 장에서(그리고 여러 다른 곳에서도) 그것을 다루었습니다.
이 절에서는 거의 아무것도 없는 상태, 오직 타입만 있는 상태에서 시작했습니다. 그리고 아주 빠르게 많은 것을 정의했습니다.
프로그래머들이 사용하는 타입들 중 아직 빠진 것도 있다는 것을 알 수 있지만, 그런 것들도 이미 정의한 타입들과 거의 같은 방식으로 정의할 수 있습니다. 예를 들어 는 그냥 기초 타입이고, 는 그냥 입니다.
앞 절에서 우리는 아주 많은 것을 아주 빠르게 정의했습니다. 하지만 Haskell의 일반화 대수적 데이터 타입(GADT)에 기대고 있었고, 함수만으로도 같은 일을 할 수 있다는 것이 자명하지는 않습니다. 하지만 할 수 있습니다. 모든 타입을 함수로 부호화하는 메커니즘이 존재하는데, 이것을 람다 계산의 창시자 Alonzo Church의 이름을 따서 _Church encoding_이라고 합니다.
우리가 이렇게 정의한 불리언 타입을 생각해 봅시다.
같은 것을 함수만으로 표현한 버전이 있습니다.
여기서 는 모든 에 대해 타입 의 값을 두 개 받아서 그중 하나를 돌려주는 함수의 축약형입니다. 이 정의 아래에서 는 첫 번째 를 돌려주는 함수이고, 는 두 번째 것을 돌려주는 함수라는 것을 알 수 있습니다.
이것들이 정말 불리언처럼 작동할 수 있는지 못 믿겠다고요? 여기 함수의 구현이 있습니다.
구현은 자명합니다. 데이터 타입 자체가 일을 하고 있기 때문입니다. 이것이 이른바 데이터 타입의 “Church 인코딩”의 주요 원리 가운데 하나입니다. 데이터 타입이 항 제거 규칙을 인코딩합니다.
이것을 어떻게 쓰는지 보겠습니다.
ifElse true "True" "False" -- "True"
ifElse false "True" "False" -- "False"
불리언 타입은 물론 기초 타입입니다. 그러니 더 복잡한 타입인 를 생각해 봅시다.
는 더 복잡한데, 생성자 로 다른 값을 내부에 담을 수 있기 때문입니다. 여기서 우리는 Church 인코딩의 또 다른 중요한 원리를 배웁니다. 값을 담기 위해 커리된 함수를 사용하는 것입니다.
이쯤 되면 타입의 Church 인코딩이 “보통” 타입과 같은 생성자들을 가진다는 것을 이미 보셨을 것입니다. 차이는 그것들을 매개변수로 받아들인다는 점뿐입니다.
만약 처럼 생겼지만 값이 하나만 있는 타입(예를 들어 타입 같은 것)이 있다면…
그 Church 인코딩은 이렇게 될 것입니다…
(이것은 실제로 타입의 Church 인코딩입니다.)
그 다음 이 타입을 생성자 도 갖도록 확장하면…
인코딩도 이렇게 확장됩니다…
그래서 Church 인코딩된 타입의 시그니처는, 그것을 제거하는 데 쓰이는 함수의 시그니처와 거의 같습니다.
그리고 함수 자체는 자명합니다. 일반적으로 타입의 Church 인코딩은 기본적으로 커리된 함수입니다. 즉, “접기” 함수와 같은 인자를 받아 같은 결과를 만들어내는 함수입니다.
Church 인코딩의 일반 원리는, 타입은 그 타입으로 _무엇을 할 수 있는가_에 의해 완전히 특징지어진다는 것입니다. 따라서 나중에 로 제거할 타입 생성자를 제공하는 대신, 곧장 로 가는 것입니다.
Task 7: 자연수 타입의 Church-encoded 버전을 작성하세요.
지금까지 우리는 Lambda Calculus가 어떻게 작동하는지 보았습니다. 이제 그것이 형식적으로 어떻게 정의되는지를 볼 차례입니다. 답은, 다른 모든 타입 시스템과 마찬가지로, _타이핑 규칙_으로 정의된다는 것입니다. 그럼 타이핑 규칙이란 무엇일까요? 음, 기본적으로 그것들도 역시 화살입니다. (놀라셨나요?)
그렇습니다. Haskell의 타이핑 규칙은 वास्तव로 화살이지만, 그것들은 Haskell과는 다른 언어, _자연 연역_이라 불리는 언어로 정의됩니다. 자연 연역은 Haskell과 비슷하지만, 전제와 결론을 가로선으로 나누는 문법을 씁니다. 예를 들어… 대신… 라고 쓰는 식입니다.
그 외에는 자연 연역과 Haskell 사이에 큰 차이는 없습니다. 예를 들어 불리언 타입을 보겠습니다. Haskell에서는 이렇게 정의했지요.
이것을 자연 연역으로 정의해서, 대부분의 프로그래밍 언어처럼 타입 시스템 자체의 “원시” 타입 가운데 하나가 되게 하려면 이렇게 생겼을 것입니다.
이는 Bool이라는 타입이 존재한다는 뜻입니다. (정확히 말하면 이것은 타이핑 규칙이 아니라 “카인딩” 규칙이기 때문에 double-colon을 씁니다.)
와 는 불리언입니다.
아, 깜빡했네요. 자연 연역에서는 전제 없는 결론을 갖는 것이 허용됩니다.
Task 8: 자연 연역을 사용해 불리언의 제거 규칙을 정의하세요.
이게 너무 단순한가요? 그럼 여기에 타이핑 문맥 (또는 타이핑 환경)이라는 개념을 더해 봅시다.
이렇습니다. 타입과 변수는 어딘가에 저장되어 있어야 합니다. 따라서 여러 값들(예를 들어 , , 등)과 여러 타입들(예를 들어 , , 등)이 주어졌을 때, 문맥은 모든 변수와 그 타입들의 _집합_입니다. (앗, 또 집합이라고 해버렸네요.) 예를 들어 같은 것이지요.
보통 문맥은 라는 문자로 나타내고, 그 문맥으로부터 따라 나온다는 뜻으로 기호를 씁니다. (아, 또 다른 화살이군요.) 예를 들어 는 문맥 안에 타입 이 있는 변수가 있다는 뜻입니다.
따라서 문맥을 고려하면 위 정의는 다음과 같이 됩니다.
즉, 문맥에 타입 가 포함되어 있습니다.
즉, 문맥에 타입 의 값 가 포함되어 있습니다.
즉, 문맥에 타입 의 값 가 포함되어 있습니다.
이렇게 해서 우리는 불리언 타입을 곧바로 문맥의 일부로 정의합니다.
이제 이것을 바탕으로 람다 계산의 공리들을 적어 보겠습니다. 그 안에는 값 수준 화살(함수)의 타입 정의 외에는 거의 아무것도 없습니다.
정의해야 할 타이핑 규칙이 몇 가지 있습니다. 가장 먼저 자명한 규칙인 _Var_가 있는데, 이것은 다음을 말합니다. 앞서 가 타입 라고 말했다면, 의 타입은 입니다.
이제 화살 자체의 타입을 정의해 봅시다.
먼저 타입 형성 규칙(또는 카인딩 규칙)부터 시작합니다.
그리고 두 개의 타이핑 규칙이 있습니다. 하나는 람다 항의 _항 도입_인데, 이것을 추상화(abstraction, 또는 Abs)라고 부릅니다.
(즉, 타입 의 값을 주었을 때 타입 의 값을 얻는 방법이 있다면, 함수 가 있다는 뜻입니다.)
그리고 람다의 항 제거도 있습니다. 즉 함수 적용(application, App)입니다.
이 규칙들이 어떻게 작동하는지 이해하기 위해, 함수를 예로 들어 봅시다. 이 함수에 대한 추상화 규칙은 다음과 같을 것입니다.
그리고 적용 규칙은 다음과 같습니다.
이 규칙들만 있으면 값 수준 화살을 정의하기에 충분합니다.
지금까지 본 규칙들은 다형 람다 계산을 정의하는 것은 아니지만, 그보다 더 단순한 타입 시스템을 정의합니다. 이름도 적절하게 _단순 타입 람다 계산_입니다.
단순 타입 람다 계산 (STLC)는 단 하나의 타입 생성자, 즉 함수(lambda)만을 가지는 타입 시스템으로, 항 도입과 제거를 위한 타이핑 규칙 Abs 와 App 을 가진다. 또한 Var 타이핑 규칙도 가진다.
단순 타입 람다 계산은 다형 람다 계산과 거의 같지만, 단 하나 다릅니다. _다형적이지 않다_는 점입니다. 즉 같은 다형 타입을 정의할 수 없습니다.
우리가 할 수 있는 최선은 타입의 별도 버전들을 정의하는 것, 예를 들어 오직 에 대해서만 동작하는 버전을 정의하는 것입니다.
그리고 에 대한 것도요.
게다가 STLC에서는 다형 타입에 대해 동작하는 _함수_도 정의할 수 없으므로, 타입뿐 아니라 그것을 사용하는 모든 함수까지도 다시 정의해야 합니다.
이 문제를 해결하고, _단순 타입_에서 다형 람다 계산(System F)으로 올라가기 위해, 우리는 타입 수준 화살을 정의합니다.
하지만 사실 그 전에 Kind부터 이야기해야 합니다…
표현식 “”에서 “”는 값의 타입을 나타냅니다. 그렇다면 표현식 “”에서 는 무엇일까요? 그것을 _타입_이라고 말할 수는 없습니다. 그러면 우리 등 뒤에 러셀이 그 이름의 역설과 함께 슬그머니 나타날 테니까요. 람다 계산에서는 이를 다음과 같이 해결합니다.
즉, 타입 시스템과 타이핑 규칙 외에도 _kind 시스템_과 _카인딩 규칙_이 있다는 뜻입니다. 하지만 제발 이 책을 창밖으로 던지지는 마세요. STLC의 kinding 시스템은 꽤 쉽게 정의됩니다. kind는 하나뿐이며, 그것을 라고 부릅니다. (때로는 로 표기하기도 합니다.)
그 다음 타입 정의 규칙은 이렇게 정의됩니다. (즉 모든 것은 kind 를 가집니다.)
그리고 다형 람다 계산의 경우는 다음 절에서 보겠습니다.
우리는 STLC를 시작하면서 자명한 Var 타이핑 규칙으로 값 수준 _변수_를 정의했습니다.
다형 람다 계산에서는 _타입 수준 변수_도 있으며, 이것들은 비슷한 TVar 카인딩 규칙으로 정의됩니다.
이제 화살 자체의 타입을 정의해 봅시다.
다형 람다 계산에서는, STLC에서와 마찬가지로 값을 다른 값으로 바꾸는 값 수준 화살이 있고…
또 타입을 다른 타입으로 바꾸는 타입 수준 화살도 있습니다. 이것들은 다음 kinding 규칙으로 정의됩니다.
예를 들어 타입 에 대해, 이 규칙은 다음을 말합니다.
다형성의 더 흥미롭고 더 어려운 부분은, 값 수준 화살이 다형 타입과 함께 작동하도록 확장하는 것입니다. 즉 값뿐 아니라 타입도 인자로 받는 함수를 갖는 것입니다.
예를 들어 STLC의 문맥에서, 지난 절에서 정의한 타입(문자열에 대해서만 동작하는 타입)을 사용한다면, 다음과 같은 타입 시그니처를 가진 함수를 정의할 수 있습니다.
다형 람다 계산의 기능을 사용하면, TAbs 규칙으로 타입을 추상화하여 다음과 같은 다형 함수를 만들 수 있습니다.
그 다음 TApp 으로 타입 매개변수를 이 추상 함수에 적용해 원래 함수를 얻습니다.
(이것은 실제 Haskell 문법은 아닙니다. Haskell은 타입 적용을 자동으로 하기 때문에, 값만 주면 언어가 타입을 추론합니다.)
아래는 다형 함수 자체의 타이핑 규칙입니다.
타입 추상화(type abstraction, 또는 TAbs)
그리고 타입 적용(TApp)
이것으로 System F의 정의를 마칩니다.
다형 람다 계산 (System F)는 단 하나의 타입 생성자, 즉 다형 람다만을 가지는 타입 시스템이며, 항의 도입과 제거를 위한 타이핑 규칙 Abs 와 App, 타입의 도입과 제거를 위한 kinding 규칙 TAbs 와 TApp 을 가진다. 또한 Var 타이핑 규칙과 TVar kinding 규칙도 가진다.
이제 이것이 우리의 주된 주제와 어떻게 연결되는지 볼 준비가 되었습니다.
우리는 이미 타입 이론과 범주론 사이에 몇 가지 평행 관계를 그려 보았지만, 단순한 유사성 이상이 있습니다. 적절한 각도에서 보면 타입 시스템 자체가 어떤 종류의 범주입니다. 게다가 우리는 이미 그것이 무엇인지도 알고 있습니다!
기초부터 시작해 봅시다.
모든 타입은 객체입니다.
그리고 모든 값 수준 화살(함수)은 사상입니다.
그리고 이제 그렇게 자명하지 않은 것 하나, 값입니다.
우리는 범주론이 화살에 관한 것이라고 말했습니다. 그런데 여기서는 겉보기에는 그 방향에서 벗어나서, 자연수 타입 같은 예에서 다시 값과 내부 그림을 그리기 시작했습니다.
하지만 모순은 없습니다. 우리는 타입 이론에서 “값은 오직 화살의 출발점과 도착점이 되는 것들뿐이다”라고 말했습니다. 자연수의 경우 그것은 화살과 화살입니다.
이것은 _값이 실제로는 화살을 표현하는 또 다른 방식일 뿐_이라는 뜻입니다.
예를 들어 자연수 타입은 외부적으로 이렇게 표현될 수 있습니다.
여기서 우리는 2장에서 배운 집합/타입 원소에 대한 간단한 정리로 다시 돌아갑니다.
임의의 집합의 각 원소는 어떤 함수와 동형이다. (여기서 는 싱글턴 집합을 뜻한다.)
따라서 어떤 타입 에 대해 에서 로 가는 화살은, 그것을 집합으로 볼 때 의 _값_과 동등합니다.
즉 우리가 라고 부르는 에서의 _화살_은 값 와 동형입니다.
외에도 화살 가 하나 더 있습니다. 그럼 이 둘을 합치면 어떻게 될까요? 또 다른 화살, 즉 의 후속자인 를 얻게 됩니다.
이것을 다시 하면 를 얻습니다.
이전 정의와 같은 방식으로 전개된다는 것을 알 수 있습니다. 값으로 돌아간 것이 아니라, 오히려 한 바퀴를 완전히 돌아 값이란 화살을 더 편하게 그리는 방법일 뿐이라는 사실을 발견한 것입니다. (혹은 다시 발견한 것입니다. 집합 범주의 기초 이론에서 이미 알고 있었으니까요.)
좋습니다. 타입을 객체로, 화살 _그리고 값_을 사상으로 보면 전체 타입 이론/타입 시스템을 범주로 볼 수 있다는 것은 알았습니다. 그런데 어떤 범주일까요? 이해하려면 Lambda Calculus의 특별한 성질을 다시 봐야 합니다. 거기에는 Lambda 타입, 즉 함수 타입이 있다는 것을 압니다. 따라서 함수 타입을 가진 범주가 필요합니다. 이것을 정의하려면 종단 객체( 객체)와 곱도 필요하므로, 그런 성질을 가진 범주를 찾아야 합니다. 놀랍게도, 우리는 이미 어떤 범주가 이런 성질들을 가지는지 알고 있습니다. 지난 장에서 논리를 다룰 때 살펴보았습니다.
단순 타입 람다 계산은 데카르트 닫힌 범주로 볼 수 있다. tuple과 either 타입은 “and”와 “or” 연산이고, Unit과 Empty 타입은 “True”와 “False” 값이며, Lambda 타입은 지수 객체이다.
깊이 다루지는 않겠지만, 무타입 람다 계산이라는 것도 있다는 점은 언급할 가치가 있다고 생각합니다. 이것은 타입이 단 하나, 즉 함수뿐인 언어이며, 모든 함수가 다른 모든 함수를 인자로 받습니다.
그렇다면 무타입 람다 계산은 우리의 그림에서 어디에 들어갈까요? 아주 잘 들어맞습니다. 이것은 데카르트 닫힌 모노이드(줄여서 C-모노이드)에 대응합니다. 객체가 하나뿐인 데카르트 닫힌 범주입니다.
우리는 값 수준 화살이 _사상_에 대응한다고 했습니다.
그렇다면 타입 수준 화살(즉 다형 타입)은 무엇에 대응할까요?
이것은 다음 장에서 계속 보겠습니다!
마무리하기 전에 다음을 생각해 봅시다. 왜 Lambda Calculus와 직관주의 논리는 거의 같은 종류의 범주, 즉 데카르트 닫힌 범주에 대응할까요?
이를 이해하기 위해, 지난 장에서 공부한 논리와 범주 사이의 대응으로 돌아가 봅시다.
직관주의 논리의 논리 체계는 바이데카르트 닫힌 범주로 볼 수 있다. “and”와 “or” 연산은 곱/쌍곱이고, “True”와 “False” 값은 시초/종단 객체이며, 함의 연산은 지수 객체이다.
이것은 지금 우리가 타입에 대해 가진 정의와 거의 정확히 같습니다. (유일한 차이는 Lambda Calculus는 쌍곱과 시초 객체 없이도 동작할 수 있어서 데카르트 닫힌 범주인 반면, 직관주의 논리는 그것들이 필요해서 _바이_데카르트라는 점입니다.)
즉 직관주의 논리와 Lambda Calculus의 유사성은 둘 다 “범주적”이라는 데서 끝나지 않습니다. 그것들은 사실상 하나이고 같은 것입니다.
| Intuitionistic logic | Simply-typed Lambda calculus | Cartesian closed category |
|---|---|---|
| Proposition | Type | Object |
| Implication | Arrow | Morphism |
| Primary proposition | Value of type A | Morphism 1 → A (global element) |
| Implication object (A → B) | Lambda type (A → B) | Exponential object B^A |
| And (A ∧ B) | Tuple (A × B) | Product A × B |
| Or (A ∨ B) | Either (A + B) | Coproduct A + B |
| True (⊤) | Unit type | Terminal object (1) |
| False (⊥) | Empty type | Initial object (0) |
| Negation A → ⊥ | Function A → Empty | Morphism A → 0 |
요컨대, 지난 장에서는 직관주의 논리와 데카르트 닫힌 범주 사이의 대응(커리-하워드-람베크 대응으로 알려진 것)에 대해 이야기했고, 이제 우리는 그 대응에 세 번째 가지를 추가하고 있습니다. 바로 Lambda Calculus입니다.
기본 타입들의 정의를 실행 가능한 Haskell로 제시할지, 아니면 수식으로 제시할지(즉 고정폭 글꼴이거나 좀 더 현대적인 형태로 제시할지) 오래 고민했습니다. 결국 수식이 더 낫다고 결정했지만, 실제로 그것들은 모두 Haskell입니다. 다만 몇 가지 단서가 있습니다.
먼저, 우리는 빈 상태에서 시작하고 싶습니다. Haskell에서는 보통 암묵적으로 import되는 표준 라이브러리(“Prelude”)를 제거해서 그렇게 할 수 있습니다.
{-# LANGUAGE NoImplicitPrelude #-}
그리고 타입 정의를 조금 더 명시적으로 쓸 수 있게 해 주는 확장도 하나 더 사용합니다.
{-# LANGUAGE GADTs, NoImplicitPrelude #-}
사실 그게 거의 전부입니다. 그리고 기호 대신 forall을 쓰는 것 정도요.
{-# LANGUAGE GADTs, NoImplicitPrelude #-}
import qualified Prelude as P
data Bool where
True :: Bool
False :: Bool
deriving (P.Show)
ifElse :: forall a. Bool -> a -> a -> a
ifElse True a b = a
ifElse False a b = b
data Either a b where
Left :: forall a b. a -> Either a b
Right :: forall a b. b -> Either a b
deriving (P.Show)
foldEither :: forall a b c. (a -> c) -> (b -> c) -> Either a b -> c
foldEither fa fb (Left val) = fa val
foldEither fa fb (Right val) = fb val
data Tuple a b where
Tuple :: forall a b. a -> b -> Tuple a b
deriving (P.Show)
first :: Tuple a b -> a
first (Tuple a b) = a
second :: Tuple a b -> b
second (Tuple a b) = b
data Maybe a where
Nothing :: forall a. Maybe a
Just :: forall a. a -> Maybe a
deriving (P.Show)
foldMaybe :: forall a b. b -> (a -> b) -> Maybe a -> b
foldMaybe n _ Nothing = n
foldMaybe _ f (Just x) = f x
data List a where
Nil :: forall a. List a
Cons :: forall a. a -> List a -> List a
deriving (P.Show)
foldList :: (b -> a -> b) -> b -> List a -> b
foldList f z Nil = z
foldList f z (Cons x xs) = foldList f (f z x) xs
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
deriving (P.Show)
foldNat :: Nat -> a -> (a -> a) -> a
foldNat Zero z s = z
foldNat (Succ a) z s = s (foldNat a z s)
plus :: Nat -> Nat -> Nat
plus Zero n = n
plus (Succ m) n = Succ (plus m n)
not :: Bool -> Bool
not False = True
not True = False
main = do
P.print (ifElse True 1 2) --1
P.print (ifElse False 1 2) --2
P.print (foldNat (Succ (Succ Zero)) 0 (P.+ 1)) -- 2
Task 1: List에서 Boolean으로 가는 어떤 대응이 하나 있는데, 아주 직관적입니다. 너무 직관적이어서 어떤 Lisp 방언들은 아예 Boolean 타입이 없고 이 대응에만 의존합니다. 이 대응이 무엇인지 맞혀 보세요.
Task 2: Haskell에서 이 대응(List와 Bool 사이)을 정의하세요. 하나는 처음부터 함수를 직접 써서 정의하고, 두 번은 foldList 함수를 사용해 정의하세요.
Task 3: 타입 List Unit를 소개합니다. 여기서 Unit은 (값이 하나뿐인 타입으로 알려진) 싱글턴 타입입니다. 공간이 허락하는 데까지 List Unit의 값들을 그려 보세요.
좋습니다, 여기 있습니다. (화살이 아니라 최종 결과만 그리겠습니다.)
Task 4: List Unit 타입은 사실 여기서 살펴본 다른 어떤 타입과 동형입니다. 무엇인지 찾아보세요.
이것은 자연수 타입(Nat)과 동형입니다. List와 Nat는 둘 다 귀납 타입이며, 둘의 유일한 차이는 List의 귀납 생성자 Cons는 타입에 의해 매개변수화된다는 점, 즉 타입의 각 값마다 생성자가 하나씩 있다는 점인 반면, Nat에는 Succ 생성자가 하나뿐이라는 점입니다. 따라서 Unit처럼 값이 하나뿐인 타입의 리스트는 Nat와 동형입니다.
Task 5: Tuple의 생성자를 작성하세요. Either의 fold 함수를 작성하세요.
먼저 tuple의 생성자입니다. 아주 직접적입니다. a와 b를 출력하는 함수를 가지려면, 생성자에 a와 b를 _입력_할 수 있어야 합니다.
data Tuple a b where
Tuple :: forall a b. a -> b -> Tuple a b
Either의 fold 함수도 직접적입니다. 처음 보면 그렇게 안 보일 수는 있지만요. 이름이 말해 주듯이 Either a b는 a이거나 b이므로, Either a b -> c로 바꾸려면 (a -> c)와 (b -> c)를 제공해야 합니다.
foldEither :: forall a b c. (a -> c) -> (b -> c) -> Either a b -> c
foldEither fa fb (Left val) = fa val
foldEither fa fb (Right val) = fb val
Task 6: Tuple 말고도 아주 중요한 음의 타입이 하나 더 있는데, 우리는 이 장에서(그리고 여러 다른 곳에서도) 그것을 다룰 것입니다.
그것은 함수 타입입니다. 함수는 “평가될 수 있는 객체”라고 생각할 수 있으므로, Tuple처럼 항 제거 규칙에 의해 특징지어집니다. 함수 a -> b는 (a 값과 함께) b 값으로 줄일 수 있습니다.
Task 7: 자연수 타입의 Church-encoded 버전을 작성하세요.
여기 있습니다.
Task 8: 자연 연역을 사용해 불리언의 제거 규칙을 정의하세요.
타이핑 규칙으로 표현한 제거 규칙(함수)은 이것입니다.
불리언 와 어떤 타입 의 두 값이 주어지면, 타입 의 값을 만들 수 있습니다.