Modified 2018-06-22 by Andrea Censi
Introduction to type theory.
Knowledge of set theory.
Modified 2018-06-22 by Andrea Censi
Types are similar to sets in that they are collections that include some objects and exclude others. On a first glance, you can interpret $0 : \text{nat}$ as $0 \in \mathbb{N}$, reading the colon as membership in sets without any ill effect. But types and sets are the basic concepts belonging to two different formal systems, type theory and set theory, respectively. It is not essential to appreciate the difference in the scope of this course but for the curious readers, this section on Wikipedia can serve as a brief summary.
Modified 2018-06-22 by Andrea Censi
Given two types $A$ and $B$, we can construct the type $A \times B$, which we call their cartesian product. (Compare this with the similar concept of cartesian product of sets which is defined in terms of its elements and not a primitive.)
Modified 2018-06-22 by Andrea Censi
As we will be using ROS, which models a robotic system as a network of communicating programs. In order to understand each other, all the communicating programs talk to each other in well-defined message types. Message types in ROS are product types composed of primitive types and other message types.
Please read section 2 on ROS/msg page and answer: what are some primitive types in ROS? what are the fields and their types in message type Header
?
Additionally, ROS/common_msgs page provides a list of pre-defined message types commonly used in robotics, such as Image (note how Header
, a non-primitive type, is included in the definition) and Pose2D. As you have likely guessed, an RGB camera publishes Image
messages, and a routing planning program might subscribe to the duckiebot’s current position in duckietown, as represented in a Pose2D
message and calculates the appropriate wheel actions.
Modified 2018-06-22 by Andrea Censi
Historically, the flexibility of naive set theory allows for some paradoxical sets such as a set that contains all sets that does not contain itself. Does this set contains itself? This is known as Russell’s paradox which demonstrated that naive set theory is inconsistent. In response, Russell and colleagues developed type theory which demands all terms to be typed, i.e., to have a type, and used a hierarchy of types to avoid Russell’s paradox. Later, a subclass of type theories known as intuitionistic type theories internalized many key ideas in constructive mathematics and became a foundation for programming languages where computability is a major concern.
On a side note, this is not to say sets cannot serve as a formal foundation of mathematics. Russell’s paradox only shows that naive set theory is inconsistent. In fact, most working mathematicians today believe that the axiomatized Zermelo-Fraenkel set theory (together with the axiom of choice, usually abbreviated as ZFC) can serve as a “consistent” foundation of all mathematics.
Modified 2018-06-22 by Andrea Censi
Type theory is a fascinating subject in itself and recently, Homotopy Type Theory (HoTT) captured a lot of research interest. For more on the subject consult HoTT website. The first chapter of the HoTT book also provides a reasonable introduction to type theory. For more practical applications of these abstract ideas, you may be intrigued by the field of formal verification, where software is verified by mathematical proofs against the formal specification, automatically.
Maintainer: Falcon Dai
No questions found. You can ask a question on the website.