요즘 여기가 좀 조용했죠! 글 쓰는 시간의 거의 전부를 Logic for Programmers에 쏟느라 머릿속이 온통 책으로 가득합니다. 믿으세요, Sphinx 빌드 후 LaTeX 커스터마이징에 대한 2000단어짜리 넋두리는 읽고 싶지 않으실 겁니다. 하지만 지난 한 주를 역사라는 토끼굴에서 보내며 찾아낸 것을 꼭 공유하고 싶어졌습니다.

계기는 Algebraic [Data] Types are not Scary, Actually라는 글이었습니다. 그 글에서는 AlgDT¹를 더 자세히 다루지만, 간단히 요약하면 다음과 같습니다:

• 곱 타입은 (Int, Bool)이나 Dog(name: str, owner: Person, age: Int 같은 것입니다. 각 필드마다 값을 하나씩 갖습니다. 거의 모든 현대 언어에는 곱 타입이 있으며, 보통 “structs”나 “records”, “value object” 등으로 부릅니다.

• 합 타입은 “태그된 합집합(tagged union)”으로, Int + Nothing이나 Result + ErrorType, Address + Number + Email 같은 것입니다. 여러 선택지 중 하나를 고르는 타입입니다. “태그”가 있다는 건 겹치는 선택지를 제거하지 않는다는 뜻입니다. Bool + Bool은 네 가지 값을 가질 수 있는데, 관용적으로 Left True, Right True, Left False, Right False라 부릅니다. 함수형 프로그래밍과 Rust 같은 일부를 제외하면, 합 타입은 현대 프로그래밍 언어에서는 비교적 드뭅니다.

이 이름들은 어디서 왔을까요? 흔한 설명은 원소의 개수, 즉 카디널리티에서 왔다는 것입니다. 타입 T의 카디널리티를 #T라 하면 #(S + T) == #S + #T이고 #(S, T) == #S * #T가 성립합니다. 잘 와닿지 않는다면 Bool + Weekday와 (Bool, Weekday)로 직접 세어 보세요.

하지만 오히려 타입의 합과 곱이 숫자의 합과 곱처럼 행동하기 때문에 그런 이름이 붙었다고 볼 수도 있습니다! 꽤 알려진 이야기라고 생각하지만 AlgDT 입문 글에서는 자주 등장하지 않습니다. 예를 들어, 수에서 덧셈은 결합법칙을 만족합니다. 즉 a + (b + c) == (a + b) + c입니다. 이를 통해 Int + (String + Null)이 (Int + String) + Null과 동형(isomorphic)(≅)이라는 것을 알 수 있습니다. 두 타입 사이에서 유용한 정보를 잃지 않고 값을 변환할 수 있다는 뜻입니다.

더 흥미로운 예는 AlgDT가 분배법칙 a*(b + c) == a*b + a*c를 따른다는 점입니다. Account(name: str, contact: (Email + Phone)) 타입의 값이 있다면, 이를 EmailAccount(name, email) + PhoneAccount(name, number) 타입의 값으로 변환할 수 있습니다. 꽤 멋지지 않나요!

그래서 궁금해졌습니다. AlgDT의 어떤 성질 때문에 “합”과 “곱”이라는 이름이 붙게 됐고, 어떤 성질들은 나중에 발견된 것일까요? 이 궁금증을 따라가다 보니 글이 대수적 데이터 타입의 초기 역사에 대한 탐구로 커져 버렸습니다.

기원을 찾아서

보통 용어의 기원을 찾는 건 악몽 같은 일이지만, 이건 일반적인 학계의 난센스라서 관련된 내용은 어딘가 논문에 다 남아 있습니다. 제가 즐겨 쓰는 두 가지 연구 방법은 다음과 같습니다:

1. 용어를 확실히 사용하는 논문을 읽고, 그 논문이 인용한 문헌을 읽고, 다시 그 문헌이 인용한 논문을 읽는 식으로 거슬러 올라가기
2. ACM Digital Library에서 용어를 검색해 가장 오래된 논문부터 하나씩 읽어 나가기²

대개는 두 방법을 섞는 게 가장 효과적입니다. 그렇게 해서 결국 도달한 것이 1961년에 출간된 존 매카시(리스프의 창시자)의 “A Basis for a Mathematical Theory of Computation”입니다. 제가 아는 한, 어떤 형태로든 AlgDT를 처음으로 다룬 문헌입니다.

매카시 논문

우선, 이 논문은 (컴퓨터 과학적 의미의) “타입”이나 “대수”라는 말을 전혀 사용하지 않으며, 사실 컴퓨터 과학 자체를 다루지도 않습니다. 다만 “주어진 기본 공간들을 이용해 새로운 데이터 공간을 정의하는 방법”을 다루는데, 그 중 하나가 “원소가 T(참)와 F(거짓)뿐인 진릿값들의 Π” 즉 ‘불리언’입니다. 하지만 매카시는 ALGOL 60 위원회 소속이었으니 타입 개념을 분명히 알고 있었을 것이고, 그래서 여기서는 의도적으로 “타입”이라는 단어를 피한 것으로 보입니다.

논문 전체는 프로그램 함수의 단순한 수학적 모델과 그 성질에 관한 것입니다. 2.6절에서는 기존 데이터 공간으로부터 새로운 데이터 공간을 생성하는 두 가지 방법을 정의합니다:

1. 두 집합 A와 B의 데카르트 곱 A × B는 a ∈ A이고 b ∈ B인 모든 순서쌍 (a · b)의 집합이다. A와 B가 유한 집합이고 n(A)와 n(B)가 각각 A와 B의 원소 개수라면 n(A × B) = n(A) · n(B)이다.

놀랍지 않게도, 곱 타입은 데카르트 곱에서 이름을 따왔습니다. 레코드 Dog(name: str, owner: Person, age: Int)는 데카르트 곱 Str × Person × Int에 태그를 붙인 버전입니다. 여기서 우리 식으로 표현하면 #(A, B) == #A * #B라는 점도 확인할 수 있습니다.

1. 집합 A와 B의 직접 합집합 A ⊕ B는 각각 A 및 B와 일대일 대응되는, 서로 겹치지 않는 두 집합의 합집합이다. A와 B가 유한하면, A와 B가 겹치더라도 [강조는 필자] n(A ⊕ B) = n(A) + n(B)이다. A ⊕ B의 원소는 자신이 속한 집합을 아래 첨자로 표시해 a_A 또는 b_B와 같이 쓸 수 있다.

제가 아는 한 “direct union”이라는 용어는 매카시가 만든 것이지만, 이는 서로소 합집합과 정확히 일치합니다. 매카시는 나중에 이 둘을 “직합(direct sum)과 데카르트 곱”이라고 부릅니다. 그는 이들을 “합 타입과 곱 타입”이라고 이름 붙이지는 않았지만, 대응되는 서로소 합집합과 데카르트 곱 집합 연산에서 이름이 유래했다고 보는 것이 타당해 보입니다. 저는 그 연산들의 이름의 역사는 파고들지 않겠지만, 아마 산술의 합과 곱에 빗대어 이름 붙여졌을 것이라 짐작합니다.

직합과 데카르트 곱을 정의한 직후³ 매카시는 데이터 공간 사이의 동형을 정의합니다:

우리는 집합 A × (B × C) and (A × B) × C를 동일한 것으로 간주하지 않지만, 이들 사이에는 표준적인 일대일 사상이 존재한다 … 우리는 이 집합들이 표준적으로 동형임을 표현하기 위해 (A × B) × C ≅ A × (B × C)라고 쓸 것이다.

그는 분배법칙 A × (B ⊕ C) ≅ A × B ⊕ A × C를 비롯해 여러 동형 관계를 보여 주는데, 제가 앞서 멋지다고 했던 바로 그 성질입니다. “대수적 데이터 타입”의 모든 성질은 아직 그렇게 불리지는 않았을지라도 처음부터 알려져 있었던 셈입니다.

거기서부터 퍼져나간 걸까?

이를 조사하던 중 “Some Observations Concerning Large Programming Efforts”(1964)라는 흥미로운 글을 발견했습니다. 저자는 애자일 선언문이 나오기 거의 50년 전에 애자일 선언문과 다름없는 내용을 제시했습니다! 아무도 이 글을 인용하지 않았고 저자는 다른 논문을 전혀 내지 않았습니다.

제가 하고 싶은 말은, 남들이 당신이 그런 아이디어를 가졌다는 걸 듣지 못한다면 맨 처음 아이디어를 낸 사람이 되는 건 중요하지 않다는 것입니다.

그러니 대수적 타입의 발전 과정을 계속 추적해 보겠습니다. 1964년 매카시는 Definition of new data types in ALGOL x를 발표했습니다.⁴ 여기서 그는 차기 ALGOL 버전에 “cartesian”과 “union”이라는 두 가지 새로운 타입을 추가하자고 제안합니다. 주목할 점은 여기서 비로소 합과 곱 모두에 문자열 태그가 붙는 “태그가 있는” 대수적 타입이 등장한다는 것입니다. ALGOL 68은 나중에 둘 다 구현하겠지만 언어 역사에서는 흥미로운 막다른 골목으로 남았고, 현대 프로그래밍 언어에는 거의 영향을 주지 못했습니다.

여기서부터 역사는 복잡해집니다. 다음 단계를 찾던 중 매카시를 인용한 두 영향력 있는 논문을 발견했습니다. 토니 호어의 Notes on Data Structuring(1970)과 로드 벌스톨의 Proving properties of programs by structural induction(1968)입니다. 이 둘은 각각 명령형 언어와 함수형 언어의 갈래에 해당하므로 따로 다루겠습니다.

호어 논문

호어는 합 타입과 곱 타입의 아이디어를 독자적으로 떠올린 것으로 보입니다. “A contribution to the development of ALGOL”(1966)에서 그는 “클래스(classes)”로 태그된 레코드와, 서로소 클래스들을 하나의 상위 타입으로 묶는 union 키워드를 제안합니다. 다만 레코드나 합집합의 대수적 성질은 언급하지 않습니다. “Notes on Data Structuring”에 이르러 그의 용어는 매카시와 일치하게 바뀝니다:

우리가 관심을 갖는 타입들은 이미 수학자들에게 친숙한 것들이다. 즉, 데카르트 곱(Cartesian Products), 구분된 합집합(Discriminated Unions), 집합(Sets), 함수(Functions), 수열(Sequences), 그리고 재귀적 구조(Recursive Structures)가 그것이다.

그의 “데카르트 곱”과 “구분된 합집합” 모두 태그가 붙어 있어 오늘날 우리가 사용하는 대수적 타입과 같은 형태입니다. 그는 주로 데이터 저장에 관심을 두고 있어 대수적 성질을 나열하지는 않지만, 이러한 타입들을 어떻게 가장 효율적으로 저장할지에 대한 논의의 일환으로 카디널리티를 언급합니다.

이 논문은 합 타입이 컴파일 타임에 오류를 잡는 수단으로 논의된 최초의 사례일 수도 있습니다:

프로그래머가 구분된 합집합 값을 그것이 유래하지 않은 타입으로 변환하려고 시도하면, 이는 무의미한 결과를 초래할 수 있는 심각한 프로그래밍 오류이다. 이 오류는 그러한 변환이 명시적으로나 암시적으로 호출될 때마다 태그 필드를 검사하는 런타임 검사를 통해서만 잡을 수 있다. 이러한 검사는 시간이 많이 걸리고, 실패했을 때 매우 불편하다. 따라서 우리는 실행 중인 프로그램에서는 이 오류가 절대 발생하지 않음을 보장하는 표기법을 찾고자 한다. 그리고 그 보장은 런타임 값을 전혀 알지 못한 채 텍스트만 검사함으로써 주어진다. 이러한 보장은 자동 컴파일러가 있다면 컴파일러가 제공할 수 있을 것이다.

또한 누군가 합 타입을 “discriminated union”이라 부른 최초의 사례도 이 논문에서 찾을 수 있습니다.⁵ 이후 바버라 리스코프는 CLU의 oneof 합 타입을 설명할 때 “discriminated union”이라는 표현을 사용하고, 니클라우스 비르트는 파스칼이 합 타입을 갖지 않는 이유를 설명하면서 같은 용어를 씁니다. 그래서 저는 명령형 진영이 합 타입을 처음 접한 것은 호어의 강의였고, 호어 자신은 (완전히 독자적이지는 않지만) 매카시의 영향을 받았다고 추측합니다.⁶

이 시점 이후 합 타입은 명령형 프로그래밍에서 사라집니다. 20세기 후반의 명령형 언어들은 파스칼과 C의 영향이 지배적이었습니다. 파스칼에는 합 타입이 없었는데, 비르트가 태그 없는 합집합보다 덜 유연하다고 생각했기 때문입니다. C에 합 타입이 없는 이유는 아마도 IBM의 PL/I의 타입 시스템을 채택했기 때문일 것입니다. 1964년에 처음 출시된 PL/I에는 곱 타입(이들은 structs라 불렀습니다)은 있었지만 태그 없는 합집합만 있었습니다. 최근의 명령형 언어들은 오히려 함수형 프로그래밍 세계에서 합 타입을 가져왔는데, 이제 다시 “Proving properties of programs by structural induction”으로 돌아가 보겠습니다.

벌스톨 논문

벌스톨은 연구하기가 믿을 수 없을 정도로 까다로운 인물입니다. 그의 부고에는 엄청난 수의 논문과 영향력 있는 제자들이 나열되어 있어, 그가 함수형 프로그래밍 초기에 엄청난 역할을 했음이 분명합니다. 하지만 그 논문들 중 온라인에 있는 것은 극히 적어, 쉽게 조사할 수 있는 부분에는 큰 공백이 있습니다. 여기서는 제가 파악한 범위 내에서 그의 역사를 최대한 정리해 보겠습니다.

이 논문은 리스트나 트리 같은 재귀 타입의 성질을 증명하는 것에 관한 것입니다. 그는 리스트를 이렇게 정의합니다:

각 생성 연산이 새로운 타입을 도입하고, 이러한 타입들의 분리(disjunction) 역시 타입이 되어야 한다고 제안한다(대략 Landin 1964를 따름)

a cons는 원자(atom)와 리스트를 갖고, a nil은 구성 요소를 갖지 않으며, a list는 cons 또는 nil이다.

벌스톨은 자신의 표기법을 P. J. 랜딘의 “The Mechanical Evaluation of Expressions”(1964)에서 가져왔다고 말합니다. 랜딘의 용법은 합 타입과는 완전히 같아 보이지는 않습니다. 타입들이 겹치는 값을 가질 경우 이를 구분할 메커니즘이 있는지 명확하지 않습니다. 오히려 벌스톨이 랜딘의 재귀적 정의 작성 방식을 “따르고” 있는 것처럼 보입니다. 몇 번 읽어봐도 판단하기 어렵고, 제가 틀렸을 수도 있습니다.

벌스톨은 어쨌든 합 타입을 가지고 있었는데, 이는 트리 정의에서 드러납니다. 트리는 “노드 또는 팁 또는 niltree”이지만, 팁은 아이템 자체가 아니라 아이템을 “갖습니다”. 그리고 나중에는 이런 의사코드가 등장합니다:

cases t:
    niltree(): nil()
    tip(i): i::nil()
    node(t1, i1, i2): concat(flatten(t1), flatten(t2))

벌스톨 역시 자신의 아이디어가 “존 매카시의 연구에 기반한다”며 그의 수학적 이론 논문을 인용합니다. 벌스톨이 매카시의 직접 합집합 개념에서 영감을 받았을 가능성은 충분히 있습니다.

2025년 기준으로 이 논문은 500회 이상 인용되었습니다. 벌스톨은 나중에 더 큰 기여를 하게 되지만 그건 1980년의 일이므로 먼저 ML을 다루어야 합니다.

밀너 논문

지금까지 대수적 데이터 타입의 정의와 “데카르트 곱”이라는 표현의 일반적인 사용은 살펴봤지만, “합 타입”과 “곱 타입”이라는 용어 자체는 아직 등장하지 않았습니다. 제가 아는 한, 그 용어는 로빈 밀너의 ML에서 비롯되었으며, “A Theory of Type Polymorphism in Programming”(1977)을 통해 널리 알려졌습니다:

완전히 결정된 타입(즉, 단형(mono types))은 기본 타입(int, bool 등)들의 집합으로부터 이항 중위 연산자인 x(데카르트 곱), +(서로소 합집합) 및 ->(함수 타입)와 단항 후위 연산자인 list에 의해 구성된다.

이 논문에서 주목할 점이 몇 가지 있습니다. 첫째, 물론 “서로소 합집합”으로 타입을 구성한다고 설명하며 + 기호를 사용한다는 점입니다. 둘째, 호어나 매카시와 달리 “서로소 합집합”을 정당화하거나 정의하지 않는다는 점입니다. 이 시점에서는 밀너의 독자들에게 이미 상식이었을지도 모릅니다. 마지막으로, 이 논문은 합과 곱이 이미 최소 2년 전부터 ML에 구현되어 있었다고 주장합니다.

가장 오래된 ML 버전들의 완전한 명세는 가지고 있지 않지만, ML이 원래 위해 설계된 LCF 증명기의 공개된 소스 코드는 가지고 있습니다. 이는 files.ml에 있습니다:

let instintype insttylist ty = inst ty whererec inst ty =
    fst(revassoc ty insttylist)
    ?(failwith phylumoftype ty
   ??``consttype vartype`` ty
   ??``funtype`` mkfuntype((inst # inst)(destfuntype ty))
   ??``sumtype`` mksumtype((inst # inst)(destsumtype ty))
   ??``prodtype`` mkprodtype((inst # inst)(destprodtype ty))
     )  ;;

자, 여기 있습니다: “sum”과 “product” 타입! 다만 이들은 태그가 없습니다. 리야오 샤(Li-yao Xia)의 글 Where does the name “algebraic data type” come from?에서는 “초기 버전에는 데이터 타입이 없었다(에든버러 LCF의 첫 번째 버전 참조)”고 언급하는데, 이는 태그가 있는 대수적 타입을 의미하는 것으로 이해합니다. ML에는 구성된 타입에 이름을 붙이는 abstype 키워드가 있었습니다. EmailOrAddress를 Str + Str로 정의할 수는 있었지만 왼쪽의 Str을 “email”이라고 부를 수는 없었습니다.

“A Theory of Type Polymorphism”은 매카시 논문도, 호어나 벌스톨의 논문도 인용하지 않으므로 밀너가 이들에게 영향을 받았는지 아니면 AlgDT를 독자적으로 개발했는지는 분명하지 않습니다. 후속 논문인 “A Metalanguage for Interactive Proof in LCF”(1978)에서 세 사람 모두에게 감사를 표한다는 점이 그 영향을 짐작하게 하는 tentative한 증거입니다:

우리는 우리 연구의 이론적 기반의 상당 부분을 제공해 준 데이나 스콧(Dana Scott)에게, 스탠퍼드에서 이 프로젝트의 전신이 되는 연구를 격려해 준 존 매카시에게, 그 프로젝트에 크게 기여한 리처드 웨이로치(Richard Weyhrauch)에게, ML의 추상 타입 개념에 도움을 준 토니 호어와 제리 슈워츠(Jerry Schwarz)에게, 실험을 통해 최종 설계 단계에 도움을 준 에이브라 콘(Avra Cohn)에게, 그리고 에든버러의 동료인 로드 벌스톨과 많은 동료들에게 깨우침을 주는 토론에 대해 빚을 지고 있다.

좋습니다, 이제 남은 언어는 세 개뿐입니다.

Hope, VAX ML, and Miranda

이 무렵 벌스톨은 소프트웨어 명세에 범주론을 적용하고 있었고, 이는 결국 HOPE 개발로 이어졌습니다. “HOPE: An experimental applicative language”(1980)는 태그된 합집합을 함수형 프로그래밍에 처음 도입한 사례로 기록되지만, 태그된 곱은 아직 아닙니다:

‘tree-of-numbers’ 타입을 정의하기 위해 우리는 이렇게 쓸 수 있다

data numtree == empty ++ tip(num) ++ node(numtree#numtree)

(기호 #는 타입의 데카르트 곱을 나타낸다.)

여기에 더해, 이 논문은 몇 가지 중요한 아이디어를 소개합니다. 첫 번째는 컴파일러가 합 타입의 모든 서로소 선택지가 처리되었는지를 철저히 검사할 수 있다는 점입니다:

각 데이터 타입은 서로 다른 생성자 함수를 갖는 서로소 하위 타입들의 집합을 가질 것이다. 예컨대 리스트는 cons나 nil로 만들어진다. 이러한 생성자에 대해 경우를 나누어 분석하기가 쉬워야 하며, 그 분석이 완전한지를 컴파일러가 검사하기 쉬워야 한다. 이렇게 하면 빈 리스트에 대한 검사를 빠뜨리는 등의 실수를 피할 수 있다.

여기에 더해, 이 논문은 패턴 매칭을 통해 합 타입의 사용을 극적으로 단순화할 수 있다고 제안합니다. 이는 구조적 패턴 매칭이 언어에 처음 등장한 사례는 아니지만(프롤로그가 먼저였습니다), 함수형 프로그래밍에서는 처음입니다.

HOPE와 거의 같은 시기에, 벌스톨의 제자의 제자인 루카 카델리⁷는 ML을 VAX와 Unix로 포팅하면서 레코드 타입과 배리언트 타입을 추가하는 작업을 하고 있었습니다. 제가 아는 한, 이는 태그된 합과 태그된 곱이 모두 함수형 프로그래밍 언어에 존재하게 된 최초의 사례입니다.

이러한 모든 아이디어는 나중에 Standard ML에 통합되어, 오늘날 사람들이 대수적 타입의 핵심 기능으로 여기는 것들 — 태그, 컴파일러 기반의 완전성 검사, 그리고 패턴 매칭 — 을 확립했습니다.

마지막으로, 다시 샤의 글을 인용하면, “Miranda: A non-strict functional language with polymorphic types”(1985)가 실제로 “Algebraic Data Type”이라는 용어를 사용한 최초의 논문입니다. 더 자세한 내용은 샤의 글을 읽어 보시길 강력히 추천합니다.

매우 불안정한 요약

• 매카시는 자신의 논문에서 대수적 데이터 타입의 개념과 성질을 처음 제안했지만, 그렇게 부르지는 않았다.
• 이는 토니 호어와 로드 벌스톨에게 최소한 어느 정도 영향을 주었고, 그들은 각자 영향력 있는 논문을 썼다.
• AlgDT는 ALGOL 68, CLU, ML에서 구현되었다. 밀너가 매카시의 이론을 알고 있었는지는 불분명하지만, 알았을 가능성이 더 높다고 본다.
• 파스칼과 C 때문에 합 타입은 명령형 프로그래밍에서 자리를 잡지 못했다.
• 벌스톨과 루카 카델리는 AlgDT의 주요 기능들을 채워 넣어, 이를 타입이 있는 함수형 프로그래밍의 초석으로 자리매김했다.

이것이 제가 가진 시간과 자원으로 할 수 있는 최선이었습니다. 오류를 발견하시면 알려 주세요!

이 글이 마음에 드셨다면 제 뉴스레터에 가입해 주세요! 매주 새로운 에세이를 보내드립니다.

저는 기업을 대상으로 형식 기법을 교육하여 소프트웨어 개발을 더 빠르고, 저렴하고, 안전하게 만듭니다. 더 자세한 내용은 여기에서 확인하세요.