함수형 프로그래밍의 도 1장 - 빈 서판

2022-04-23

Bartosz Milewski의 함수형 프로그래밍의 도 The Dao of Functional Programming 1장 “빈 서판Clean Slate”을 읽고 요약했습니다.

도입

프로그래밍은 타입과 함수에서 시작합니다. 타입이나 함수에 대한 기존 지식은 모두 잊으세요. 오히려 방해가 될 수 있습니다. 컴퓨터나 구체적인 구현에 대해 생각하지 마세요. 프로그래밍의 본질과 무관합니다.

1.1. 타입과 함수Types and Functions

타입 이론type theory에서 타입type이라고 부르는 개념을 범주론category theory에서는 대상object이라고 부르며, 논리학logics에서는 명제proposition라고 부릅니다.

하나 이상의 타입이 존재할 수 있으므로 타입에 Int, Bool 등의 이름을 붙여주곤 하지만, 타입 그 자체에는 아무런 의미도 없습니다. 타입의 의미는 타입들 사이의 관계에 의해 부여됩니다.

타입과 타입 사이의 관계는 화살표에 의해 표현되는데, 타입 이론에서는 화살표를 함수function라고 부르고, 범주론에서는 사상morphism이라고 부르며, 논리학에서는 수반entailment 또는 함축implication이라고 부릅니다.

a \rightarrow b

위 수식은 다음과 같이 해석할 수 있습니다.

타입 이론: 타입 a를 받아서 타입 b를 반환하는 함수가 존재한다.
범주론: 대상 a에서 대상 b를 연결하는 사상이 존재한다.
논리학: a가 참이면 b도 참이다. 즉 a는 b를 함축한는 증명이 존재한다.

두 타입 사이에 여러 함수가 존재할 수 있으므로, 필요하면 함수에도 이름을 붙일 수 있습니다.

a \overset{f}{\rightarrow} b

위 수식은 다음과 같이 해석할 수 있습니다.

타입 이론: 타입 a를 받아서 타입 b를 반환하는 함수 f가 존재한다.
범주론: 대상 a에서 대상 b를 연결하는 사상 f가 존재한다.
논리학: a가 참이면 b도 참임을 보이는 증명 f가 존재한다.

타입 이론, 람다 대수lambda calculus, 논리학, 범주론 사이의 대응 관계는 커리-하워드-램벡 대응Curry-Howard-Lambek correspondence이라고 부릅니다.

1.2. 음과 양Yin and Yang

한 대상으로부터 범주 내의 다른 모든 대상으로 향하는 사상이 존재할 경우, 그 대상을 시작 대상initial object이라고 부릅니다. 수학에서는 보통 0으로 표현하며, 논리학에서는 거짓false이라고 부르고 기호로는 $\bot$ 으로 표현하며, 해스켈 언어에서는 Void 타입으로 부릅니다.

범주 내의 다른 모든 대상으로부터 한 대상으로 향하는 사상이 정확히 하나씩만 존재할 경우, 그 대상을 끝 대상terminal object이라고 부릅니다. 수학에서는 보통 1로 표현하며, 논리학에서는 참true이라고 부르고 기호로는 $\top$ 으로 표현하며, 해스켈 언어에서는 ()으로 나타내며 유닛Unit이라고 부릅니다.

initial -> {a;b;c} -> terminal;
initial -> initial;
a -> a:ne;
b -> b;
c:sw -> c;
terminal -> terminal;

1.3. 원소들Elements

집합 안을 들여다보면 원소들이 있는 것과 달리, 범주론의 대상은 직접 들여다볼 수 없습니다. 다만 대상으로 향하는 사상들을 통해 그 대상의 구조를 살펴볼 수 있을 뿐입니다. 시작 대상으로 향하는 사상은 존재하지 않기 때문에(자기 자신을 향하는 화살표는 제외), 시작 대상에는 구조가 없다고 말합니다.

모든 대상으로부터 끝 대상으로 향하는 사상이 정확히 하나씩만 존재하기 때문에 끝 대상은 가장 단순한 구조를 가집니다. 즉, 다른 대상들이 볼 때 끝 대상은 그저 “존재”한다는 구조만을 가지고 있습니다.

끝 대상은 가장 단순한 구조를 가지기 때문에, 끝 대상에서 출발하여 다른 대상으로 향하는 사상을 이용하면 다른 대상들의 구조를 살펴볼 수 있습니다.

만약 끝 대상에서 어떤 대상 $a$ 로 향하는 사상이 둘 또는 그 이상 존재한다면, 이는 대상 $a$ 를 볼 수 있는 여러 방법이 존재한다는 것을 의미하고, 이는 곧 대상 $a$ 에 어떠한 구조가 존재한다는 뜻입니다.

끝 대상(1)에서 어떤 대상 $a$ 로 향하는 사상 $x$ 가 있다면, $x$ 를 $a$ 의 전역 원소global element 또는 그냥 원소라고 부릅니다.

1 \overset{x}{\rightarrow} a

타입 이론에서는 $x: A$ 라고 쓰며 $x$ 의 타입은 $A$ 라는 의미입니다. 해스켈에서는 아래와 같이 콜론 두 개를 써서 표현합니다.

x :: A

논리학에서는 $x$ 가 $A$ 의 증명이라고 불립니다. 왜냐하면 $\top \rightarrow A$ 는 “만약 True 가 참이라면 A도 참이다”라는 뜻이기 때문입니다.

시작 대상, 즉 Void는 원소가 없습니다. 끝 대상에서 시작 대상을 찔러볼 수 있는 방법(즉, 끝 대상에서 시작 대상으로 향하는 사상)이 없기 때문입니다.

끝 대상, 즉 ()은 단일한 원소를 가집니다. 끝 대상을 찔러볼 수 있는 방법(즉, 끝 대상에서 끝 대상으로 향하는 사상)이 하나 뿐이기 때문입니다.

initial -> {a; terminal};
initial -> initial;
a -> {a; terminal};
terminal -> {a; terminal} [color="#33FF33"];

1.4. 화살표들을 담고 있는 대상The Object of Arrows

지금까지는 대상을 향하는 사상들을 이용하여 대상의 구조를 설명했습니다. 화살표 자체를 어떤 대상의 요소로 간주할 수도 있을까요? 즉, 화살표들을 담고 있는 대상에 대해서 생각해볼 수 있을까요?

프로그래밍에 대입해서 생각해보면, 지금까지는 함수 인자의 타입과 함수 반환값의 타입에 대해 생각했다면, 이제는 함수 자체의 타입에 대해 생각해볼 차례입니다.

예를 들어 타입 a를 받아서 타입 b를 반환하는 함수 f의 타입은 다음과 같습니다.

f :: a -> b

위 코드는 아래와 같이 분해할 수 있습니다.

대상 $a$
대상 $b$
대상 $a$ 와 $b$ 를 연결하는 사상 $f$
사상 $f$ 를 원소로 가지고 있는 대상 $a \rightarrow b$

프로그래밍 언어에서 쓰는 표기법들을 종종 3과 4의 차이를 잘 드러내지 못합니다. 범주론에서는 4를 아래와 같이 표현합니다.

1 \overset{f}{\rightarrow} b^a

논리학에서는 $A \rightarrow B$ 가 함축을 의미합니다. 즉 “A이면 B이다”를 뜻합니다. 위 식에서 $B^A$ 가 이 명제에 대응합니다. 이 명제는 참일 수도 있고, 거짓일 수도 있습니다. 이 명제가 참이라는 근거들이 $B^A$ 의 원소들입니다. $B^A$ 의 원소를 찾았다면 이 명제가 참이라는 점이 증명된 것입니다.

전체 목차를 보려면 함수형 프로그래밍의 도를 읽어주세요.