Type Theory
Type theory is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software.
Type theories are also called higher-order logics, since they allow quantification not only over individual variables (as in first-order logic), but also over function, predicate, and even higher-order variables. Type theories characteristically assign types to entities, distinguishing, for example, between numbers, sets of numbers, functions from numbers to sets of numbers, and sets of such functions. These distinctions allow one to discuss the conceptually rich world of sets and functions without encountering the paradoxes of naive set theory.
Idea
All entities have type, including functions. If $\alpha$ and $\beta$ are types, the type of functions from elements of type $\beta$ to elements of type $\alpha$ is written as $\beta \rightarrow \alpha$.
Functions that take more than one arguments can be represented in terms of functions of one argument which returns a function type.
각 term과 type을 표현할 때 $a: A$로 나타내는데, 이는 term a의 type이 A임을 의미한다.
Why Type?
Programming language에서 type은 각 term의 expected behavior와 연결된다. 따라서 해당 term 혹은 subterm의 type에 따라 value가 달라지거나, 아예 term의 validity가 달라질 수도 있다.
Type checker는 이를 통해 program의 semantics에 대한 어느 정도의 검증을 가능하게 한다. 그러나 type checker를 통한 검증은 sound하지 않다. Type checker를 통과해도 program semantics가 올바르지 않은 경우(Runtime Error)를 우리는 너무 잘 알고 있다. 반면, type checker는 대게 complete하기 때문에, type checker를 통과하지 못하는 프로그램은 실행하지 않아도 의미적으로 올바르지 않음을 알 수 있다.
Dependent Type
Dependent Type은 어떤 term의 값에 의존적인 type으로, Type $A: \mathcal U$에 대하여 각 term $a: A$마다 type $B(a): \mathcal U$를 대응시키는 type이다. $\mathcal U$는 type universe를 나타낸다. 이 때 $a$의 값에 따라 변하는 dependent type $B: A \rightarrow \mathcal U$이다.
Dependent Product Type
Return type이 argument에 대한 dependent type인 function의 type을 dependent product type이라고 한다. 어떤 type $A$와 dependent type $B: A \rightarrow \mathcal U$에 대하여 $\prod_{x:A}{B(x)}$로 나타낸다.
특히 constructive logic에서는 명제가 type이기 때문에 $\forall x \in A, B(x)$와 같은 명제가 dependent product type에 해당한다.
Type Universe
Type system에서 type 또한 term이기 때문에 type도 type을 가지게 된다. 이처럼 type의 type을 type universe라고 하며 $\mathcal U$로 나타낸다.
그러나 $\mathcal U: \mathcal U$이게 되면 Russel Paradox 등의 문제가 생기기 때문에 type universe는 여러 universe로 귀납적으로 정의되며, 한 universe의 type이 다음 universe이다.
- $\forall A, \forall x: A$, x is not a type, $A: \mathcal U(0)$
- $\mathcal U(i): \mathcal U(i+1)$