새로운 시작

프로그래밍은 타입과 함수로 시작한다. 타입과 함수에 대한 선입견은 모두 버려라. 그것들은 마음을 어지럽힐 뿐이다.

프로그래밍이 하드웨어로 어떻게 구현되었을지는 생각하지 마라. 컴퓨터는 여러 계산 모델 중 하나일 뿐이다. 프로그래밍을 하드웨어와 연관지어 생각할 필요 없다. 계산은 머리로 할 수도 있고 펜과 종이로 할 수도 있다. 프로그래밍에 대한 생각은 물리적인 기저와 관련이 없다.

타입과 함수

도덕경에 이런 말이 나온다.

道可道 非常道

'말로써 설명할 수 있는 도는 영원한 도가 아니다'라는 뜻인데 타입에도 적용할 수 있다. 설명할 수 있는 타입은 타입이 아니다. 타입은 가장 기본적인 개념이며 따로 더 설명할 수 없다.

타입은 분야별로 부르는 이름이 다르다.

• 타입 이론 : 타입(type)
• 카테고리 이론 : 오브젝트(object)
• 논리학 : 명제(proposition)

타입은 하나 이상 존재하기 때문에 이름을 지어줘야 한다. 손가락으로 가리켜서 구분할 수 있지만 다른 사람들과 소통하려면 부를 수 있는 이름이 있어야 한다. $a, b, c$나 Bool, Double 등으로 부를 것이다. 이것들은 그냥 이름일 뿐이다.

하나의 타입 자체는 아무 의미가 없다. 다른 타입과 어떻게 연결되었는지가 타입을 특별하게 만든다. 연결은 애로우(arrows)로 설명한다. 애로우에는 시작 쪽의 타입이 있고 끝 쪽의 타입이 있다. 시작과 끝이 같을 수 있는데 이때 애로우는 다시 되돌아 온다.

타입 간의 애로우를 함수(function)라 한다. 오브젝트 간의 애로우를 사상(morphism)이라 한다. 명제 간의 애로우를 귀결(entailment)이라 한다. 이것들은 수학의 여러 분야에서 애로우를 부르는 단어일 뿐이다. 서로 바꿔 사용해도 된다.

두 타입 간에 애로우가 하나 이상 있을 수 있으므로 이름을 지어야 한다. 예를 들어 타입 $a$에서 타입 $b$로 가는 애로우를 $f$라 부를 수 있다.

이렇게 해석할 수도 있다. 함수 $f$는 인자로 타입 $a$를 받아서 그 결과로 타입 $b$를 제공한다.

아래 분야들의 관련성을 연구하는 분야를 커리-하워드-

음과 양

오브젝트는 오브젝트의 연결로 정의된다. 애로우는 두 오브젝트가 연결되었다는 사실의 증거이자 목격자이다. 어떤 때는 증거가 하나도 없을 수 있다. 오브젝트가 연결되지 않은 것이다. 어떤 때는 증거가 많을 수 있고 단 하나의 증거만 있을 수도 있다. 증거가 단 하나만 있는 경우 애로우가 유일(unique)하다고 한다.

유일하다는 것은 어떤 의미일까? 예를 들어 두 오브젝트 간의 애로우가 두 개 있다면 그 둘이 같음을 의미한다.

모든 오브젝트로 나가는 애로우가 각각 유일한 오브젝트를 시작(initial) 오브젝트라 한다.

시작 오브젝트의 반대는 모든 오브젝트로부터 들어오는 애로우가 각각 유일한 오브젝트로 끝(terminal) 오브젝트라 한다.

수학에서 시작 오브젝트는 보통 $0$으로 표기하고 끝 오브젝트는 $1$로 표기한다.

시작 오브젝트는 모든 것의 출발점이다. 하스켈에서는 타입 Void가 수학에서의 $0$이다. Void는 모든 것이 발생하는 혼돈을 상징한다. Void에서 모든 것으로 가는 애로우가 있기 때문에 Void에서 Void 자기 자신으로 가는 애로우도 있다.