This introduction does not aim at providing full understanding of type theory, but is more focused on giving a brief yet extensive overview of the basis that might be of interest to any new or even experienced programmer. Kumi makes extensive use of some concepts that will be detailed in the following sections. In the current state, the Kumi library focuses on handling product types.
Type theory is the academic study of type systems used to formalize how types are constructed and composed. While Set Theory categorizes elements into sets, Type Theory categorizes data (propositions) and the transformations (proofs) applied to them.
In this view:
The Curry-Howard Correspondence formalizes the direct link between logical reasoning and type-level reasoning. Every concept in logic has a direct counter part in type theory. The following table recapitulates the different operation that can be necessary to understand.
| Logic Name | Logic Notation | Type Notation | Type Name | C++ Example |
|---|---|---|---|---|
| True | \( \top \) | \( \top \) | Unit Type | std::monostate |
| False | \( \bot \) | \( \bot \) | Empty Type | void (as a non-return type) |
| Implication | \( A \to B \) | \( A \to B \) | Function | std::function<B(A)> |
| Not | \( \neg A \) | \( A \to 0 \) | Function to empty type | [[noreturn]] void foo |
| And | \( A \land B \) | \( A \times B \) | Product type | std::tuple<A,B> |
| Or | \( A \lor B \) | \( A + B \) | Sum type | std::variant<A,B> |
In order to be able to build more complex type, it is necessary to first define Atomic Terms. In common type theory, these can be of three different types. There are the natural numbers, often denotated nat, then there are boolean values notated bool and formal variables. Formal variables are simply variables reffered to by a symbol.
Then in order to be able to manipulate these types, there is the concept of functions terms. This is simply a function in the programming sens. Given a parameter of a type \( \sigma \) and a return type \( \tau \) the associated function is noted \( \sigma \rightarrow \tau \). The addition of two real numbers can then written as : add : nat \( \rightarrow \) (nat \( \rightarrow \) nat)
Finally, there are lambda terms, it is associated to concept of anonymous functions/lambdas functions in programming, these should sound familiar. They simply represent a way to define new function terms.
In the context of Set Theory, the Cardinality of a set is simply the number of element it contains. When translating it to Type Theory, the cardinality of a type refers to the total number of unique values (or states) an instance of that type can possibly represent.
By treating types as set of potential values, we can use standard arithmetic to predict the complexity of our data structures. A type like bool as a cardinality of 2, the set of it's values is \( {true, false} \)
Understanding cardinality allows us to see types not just as labels, but as mathematical objects where the size of the state space dictates how much information a variable can have.
In the next page, we will see some more specific types that are used as a base for more complex operations.
Reference Wikipedia: Type Theory
