대수적 자료형(Algebraic data types)

참·거짓 두 값을 갖는 타입 Bool이 있습니다. Bool 두 개의 쌍 (Bool, Bool)은 (참, 참), (참, 거짓), (거짓, 참), (거짓, 거짓)의 네 값을 갖습니다. 요일(7개)과 Bool의 쌍은 14개입니다. 쌍의 타입을 곱 타입⁠(product type)⁠ $A \times B$라 부르는 까닭이 여기에 있습니다. 값의 개수가 곱해집니다. 한편 'A의 값 하나 또는 B의 값 하나'를 담는 타입은 합 타입⁠(sum type)⁠ $A + B$입니다. 값마다 어느 쪽에서 왔는지 꼬리표(inl, inr)가 붙어서, A와 B가 둘 다 Bool이어도 inl 참과 inr 참은 다른 값입니다. 그래서 개수가 더해집니다. 원소⁠(element)⁠가 없는 타입 0과 원소가 하나뿐인 타입 1까지 두면, 타입들은 0, 1, +, ×를 가진 수처럼 셈이 됩니다. 이렇게 합과 곱으로 짓는 타입을 대수적 자료형⁠(algebraic data type)⁠이라 합니다.

'셈이 된다'는 말은 정확히 이런 뜻입니다. $A \times B$와 $B \times A$는 같은 타입이 아니지만, 쌍의 순서를 바꾸는 함수⁠(function)⁠가 서로 되돌리는 짝으로 있어서 값들이 빠짐없이 하나씩 짝지어집니다(전단사⁠(bijective)⁠). 이런 관계를 동형($\cong$)이라 합니다. 동형⁠(isomorphism)⁠을 같음으로 보면 수의 법칙이 그대로 성립합니다. $A \times (B + C) \cong A \times B + A \times C$(분배 법칙), $1 \times A \cong A$, $0 + A \cong A$, $0 \times A \cong 0$. 각 법칙은 두 방향의 변환 프로그램으로 확인됩니다. 분배 법칙이라면 (a, inl b)를 inl (a, b)로 보내는 식입니다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠으로 읽으면 이 동형들은 논리의 동치이기도 합니다. A ∧ (B ∨ C)와 (A ∧ B) ∨ (A ∧ C)가 서로를 함축한다는 것입니다.

타입 , $|A| =$ , $|B| =$ :

함수 타입은 거듭제곱입니다. $A \to B$의 값은 A의 원소 |A|개 각각에 B의 원소 하나를 정해 주는 방법이니, $|B|^{|A|}$가지입니다. Bool → Bool은 $2^2 = 4$개로, 항등 함수, 부정, 늘 참, 늘 거짓입니다. 그림의 함수 칸이 출력들을 늘어놓은 모양인 것도 이 때문입니다. 함수 하나는 출력들의 |A|짝, 곧 $B \times B \times \cdots \times B$의 원소와 같습니다. A → 2는 A의 원소를 참과 거짓으로 가르는 방법이니 A의 부분집합⁠(subset)⁠과 하나씩 짝지어지고, 그래서 멱집합⁠(power set)⁠의 크기가 $2^{|A|}$입니다. 지수 법칙도 프로그램입니다. $c^{ab} = (c^b)^a$는 $(A \times B \to C) \cong (A \to B \to C)$, 곧 두 인자를 한꺼번에 받는 함수와 하나씩 받는 함수를 바꾸는 커링입니다. $c^{a+b} = c^a c^b$는 '합에서 나가는 함수는 두 경우를 각각 처리하는 함수의 쌍'이라는 경우 나누기이고, $(bc)^a = b^a c^a$는 '쌍을 돌려주는 함수는 함수의 쌍'입니다.

그림에서 |A| = 0으로 두어 보세요. A → B의 값은 정확히 하나(빈 함수)이고, B → A는 |B| ≥ 1이면 하나도 없습니다. $m^0 = 1$과 $0^n = 0$(n ≥ 1)이 그대로 보입니다. 논리로 읽으면 앞의 것은 '거짓에서는 무엇이든 나온다', 뒤의 것은 '참에서 거짓은 나오지 않는다'입니다. $0^0 = 1$인 까닭도 여기서 분명해집니다. 빈 타입⁠(empty type)⁠에서 빈 타입으로 가는 함수는 빈 함수 하나입니다. 이 셈은 타입이 유한하고 함수가 모두 끝까지 계산된다고 가정하며, 함수를 입력–출력 표로 봅니다. 코드는 달라도 같은 표를 내는 두 프로그램은 한 함수로 셉니다. 끝나지 않는 계산이 섞이는 실제 언어에서는 '값이 없음'도 값처럼 끼어들어 개수가 달라집니다.

되부르는 타입도 셈이 됩니다. A의 리스트는 비어 있거나, 원소 하나와 나머지 리스트의 쌍입니다. 식으로 쓰면 $L = 1 + A \times L$입니다. 수처럼 풀면 $L = \dfrac{1}{1 - A} = 1 + A + A^2 + A^3 + \cdots$, 곧 '빈 리스트, 또는 원소 하나, 또는 둘, 또는 셋, …'이라는 등비급수가 됩니다. 뺄셈과 나눗셈은 타입에 뜻이 없지만, 전개한 급수⁠(series)⁠는 뜻이 있습니다. $A^n$의 계수는 원소가 n개인 리스트의 모양 수(여기서는 1)이고, 이 급수는 모양의 수를 세는 생성함수⁠(generating function)⁠로서 엄밀하게 다룰 수 있습니다. 이진 나무는 잎⁠(leaf)⁠이거나 두 나무를 이은 마디이니 $T = 1 + x\,T^2$(x는 마디 하나)이고, 풀면 $T = \frac{1 - \sqrt{1 - 4x}}{2x}$, 계수는 1, 1, 2, 5, 14, 42, …의 카탈랑 수⁠(Catalan number)⁠입니다. 마디가 n개인 이진 나무의 모양 수가 정확히 이 수입니다. 마디 수를 세지 않고 모양만 보려고 x를 떼면 $T = 1 + T^2$, 곧 '나무는 잎이거나 나무 두 개의 쌍'입니다. 이것을 복소수⁠(complex number)⁠의 이차방정식 $T^2 - T + 1 = 0$으로 풀면 $T = e^{\pm i\pi/3}$, 곧 $T^6 = 1$인 1의 거듭제곱근⁠(roots of unity)⁠이 되어 $T^7 = T$가 나옵니다. 뺄셈도 없는 타입에서 복소수를 거친 계산은 믿을 근거가 없어 보이지만, 1995년 앤드리어스 블라스는 '나무 일곱 개의 묶음'과 '나무 하나'를 하나씩 짝짓는 명시적인 대응을 실제로 찾았습니다($T^7 \cong T$). 그렇다고 같은 계산의 중간 단계 $T^6 \cong 1$까지 참인 것은 아닙니다. 나무는 무한히 많으니 여섯 개의 묶음도 무한히 많습니다. 복소수 계산에서 나온 등식이 언제 실제 동형으로 옮겨지는지는 조건이 필요하고, 2000년대 초 마르셀로 피오레와 톰 라인스터가 그 조건을 밝혔습니다.

미분에도 자료 구조의 뜻이 있습니다. 세 원소의 묶음 $A^3 = A \times A \times A$에서 한 자리에 구멍을 뚫는다고 합시다. 구멍의 자리 셋 가운데 하나를 고르고, 나머지 두 자리의 값을 적으면 되니 구멍 뚫린 묶음의 타입은 $3 \times A^2$입니다. 이것은 $\frac{d}{dA}A^3 = 3A^2$과 같습니다. 곱의 미분법 $(FG)' = F'G + FG'$도 '구멍은 왼쪽 부분에 있거나 오른쪽 부분에 있다'로 읽힙니다. 리스트에 적용하면 $L' = \frac{1}{(1-A)^2} = L \times L$입니다. 구멍 하나 뚫린 리스트는 구멍 앞의 리스트와 뒤의 리스트의 쌍이라는 뜻입니다. 1997년 제라르 위에가 제안한 지퍼(zipper)가 바로 이 모양입니다. 구멍의 맥락에 구멍 자리의 값을 더한 $A \times L \times L$를 들고 다니면, 편집기의 커서처럼 자료 구조 안의 한 자리를 가리키면서 이웃으로 한 칸 옮기는 일을 상수 시간에 할 수 있습니다. 왼쪽 맥락을 구멍에 가까운 것부터 적어 두면, 한 칸 옮길 때 리스트의 맨 앞 원소 하나만 옮기면 되기 때문입니다. 코너 맥브라이드는 2001년, 규칙적인 타입의 미분이 언제나 구멍 하나 뚫린 맥락의 타입이라는 것을 정리했습니다. 멱급수를 항별로 미분하는 것(테일러 급수⁠, Taylor series⁠)과 같은 셈법이 자료 구조에서도 통하는 것입니다. 조합론⁠(combinatorics)⁠에서는 앙드레 조얄의 종(species) 이론(1981)이 같은 생각을 먼저 다듬었습니다.

◀ 구멍을 왼쪽으로 구멍을 오른쪽으로 ▶

합 타입은 프로그램을 안전하게 만듭니다. 합 타입의 값을 쓰려면 경우를 나눠야 하고, 컴파일러⁠(compiler)⁠는 빠진 경우가 없는지 검사할 수 있습니다. 값이 없을 수도 있다는 것을 $1 + A$(Maybe, Option)로 적으면, '없음'의 경우를 처리하지 않은 코드는 실행 전에 걸러집니다. 토니 호어는 1965년 언어 ALGOL W에서 아무 참조나 '없음'(null)이 될 수 있게 했는데, 2009년 이 결정을 '10억 달러짜리 실수'라 불렀습니다. 합 타입이 있는 언어에서는 이 '없음'이 타입에 드러납니다.

흔한 혼동 둘을 짚어 둡니다. 첫째, 대수적 자료형(algebraic data type)과 추상 자료형(abstract data type)은 약자가 같지만 다른 개념입니다. 뒤의 것은 내부 표현을 감추고 연산만 드러내는 설계 방식입니다. 둘째, 개수가 같다고 같은 타입은 아닙니다. Bool과 $1 + 1$은 동형이고, 동형인 타입은 한쪽에 대해 증명한 것을 변환을 거쳐 다른 쪽으로 옮길 수 있을 뿐입니다. '동형인 타입은 같다'를 공리⁠(axiom)⁠로 받아들이는 것이 호모토피 타입 이론⁠(homotopy type theory)⁠의 일가성 공리입니다. 더 정확히는 '두 타입이 같다는 증명'과 '두 타입 사이의 동형'이 정확히 하나씩 맞물린다는 공리입니다. 한 걸음 물러서 보면, 리스트는 '$X \mapsto 1 + A \times X$'라는 타입 짓기 규칙의 가장 작은 해이고, 리스트 위의 되부름(fold)은 그 해가 갖는 보편 성질⁠(universal property)⁠에서 나옵니다. 이 규칙이 함자⁠(functor)⁠의 예이며, 이 관점이 범주론⁠(category theory)⁠으로 이어집니다.

이어지는 곳. 합과 곱을 개수 대신 논리로 읽는 법, 곧 '그리고'는 쌍이고 '또는'은 꼬리표 붙은 값이라는 것은 커리–하워드 대응의 표에 있습니다. 개수의 법칙은 무한 집합⁠(set)⁠에서도 통하는 집합의 크기⁠(cardinality)⁠의 셈과 같은 모양이며, $2^{|A|}$는 칸토어의 대각선 논법⁠(Cantor's diagonal argument)⁠이 멱집합이 늘 더 크다고 말할 때의 그 수입니다. 리스트와 나무의 개수를 세는 급수는 생성함수로, 나무의 개수는 카탈랑 수로 이어지고, 미분이 구멍을 뚫는다는 것은 미분과 테일러 급수의 셈을 자료 구조에서 다시 보는 일입니다. 되부르는 타입은 재귀⁠(recursion)⁠로 처리하고, 그 되부름이 반드시 끝난다는 보장은 수학적 귀납법⁠(mathematical induction)⁠과 같은 원리에서 나옵니다. 타입 변수를 넣어 '모든 A에 대해 A의 리스트'를 한 번에 다루는 것이 다형성⁠(polymorphism)⁠입니다. 되부르는 타입이 방정식 $L\cong 1 + A\times L$의 가장 작은 해, 곧 시작 대수이고 그 위의 구조적 재귀가 하나뿐인 fold라는 것은 그 페이지에서, 곱과 합이 두 자리 모두에서 공변⁠(covariant)⁠이라 읽기 전용 자료가 대개 공변이라는 것은 하위 타입⁠(subtype)⁠과 변성⁠(variance)⁠에서 이어집니다.