러셀의 역설을 해결하는 타입 이론, 그리고 범주론과의 연결
러셀의 역설(Russell's paradox)은 집합론의 문제점을 드러내며, 타입 이론(Type Theory)의 등장을 촉발함
타입 이론은 집합론의 대안으로, 타입(Type)과 항(Term)의 개념을 통해 역설을 회피함
다양한 타입(Boolean, Maybe, List 등)의 정의와 람다 계산법(Lambda Calculus)과의 관계를 설명함
타입 시스템을 범주론(Category Theory)의 관점에서 해석하고, 단순 타입 람다 계산법이 데카르트 닫힌 범주임을 밝힘
러셀의 역설(Russell's Paradox)과 타입 이론(Type Theory)의 등장 배경
본문에서는 러셀의 역설(Russell's paradox)이 집합론의 문제점을 드러내며, 타입 이론(Type Theory)의 필요성을 제기하는 배경을 설명한다. 특히, 자기 자신을 포함하는 집합의 개념에서 발생하는 모순을 지적하며, ZFC 집합론(ZFC set theory)과 같은 해결책이 존재하지만, 단순성을 잃는다는 단점을 언급한다. 이러한 문제점을 해결하기 위해 러셀은 집합 대신 타입(Type) 개념을 도입하여 역설을 회피하는 방법을 제시한다.
타입 이론(Type Theory)의 핵심 개념: 타입(Type)과 항(Term)
타입 이론(Type Theory)은 집합론과 달리, 항(Term)이 타입(Type)에 종속되는 구조를 가진다. 즉, 하나의 항은 오직 하나의 타입에만 속할 수 있다. 이러한 제약 조건은 러셀의 역설(Russell's paradox)을 근본적으로 해결하는 데 기여한다. 본문에서는 이러한 타입 이론의 기본 원리를 설명하고, 타입과 항의 관계를 명확히 제시하며, 집합론과의 차이점을 강조한다. 특히, $a:A$ 표기법을 통해 항이 타입에 속함을 나타낸다.
다양한 타입(Type) 정의와 람다 계산법(Lambda Calculus)과의 관계
본문에서는 Unit, Lambda, Boolean, Maybe, Inductive, Composite 등 다양한 타입(Type)의 정의를 소개하고, 각 타입의 생성 규칙(Term Introduction), 소멸 규칙(Term Elimination)을 설명한다. 특히, 람다 계산법(Lambda Calculus)을 활용하여 타입(Type)을 정의하는 방법을 제시하며, Church encoding을 통해 람다 계산법으로 타입(Type)을 표현하는 원리를 설명한다. 이러한 과정을 통해 타입 이론과 람다 계산법의 깊은 연관성을 보여준다.
타입 시스템(Type System)을 범주론(Category Theory)으로 해석
본문에서는 타입 시스템(Type System)을 범주론(Category Theory)의 관점에서 해석한다. 타입(Type)을 객체(Object)로, 값 수준의 화살표(Value-level arrow)를 사상(Morphism)으로 간주하여 타입 이론을 범주론적 언어로 표현한다. 특히, 단순 타입 람다 계산법(Simply-typed Lambda Calculus)이 데카르트 닫힌 범주(Cartesian Closed Category)임을 밝히며, 튜플(Tuple)과 Either 타입을 'and'와 'or' 연산으로, Unit과 Empty 타입을 'True'와 'False' 값으로, 람다 타입을 지수 객체로 대응시킨다.
