5

What is a type in type theory? I tried to find a rigorous definition without luck. And that makes me wonder.. maybe there isn't any rigorous definition?

My aim is to see how homotopy type theory provides a foundation for mathematics. An attempt is given here. Despite the nice resources given there, however, I found that my problem was more basic than knowing what a homotopy type theory is. Rather, it's about type theory: I'm in search of a rigorous definition of type theory.

Now, since this question is close to the fundamentals.. I reckon that I might have to specify what I really need. First of, I know how the basics of type theory works. I know that a type is roughly a collection of things, called terms, whatever these means. I know there might be rules to tell if a given term is of a given type. I know there are types derived from predefined types.. etc. If you ask me to follow the rules and play the game, I think I won't have a problem. What bothers me is that I don't really know what a type is, whenever addressed.

So, really, what is a type? What is a term? What is a function? Are they fundamentally undefined?

My feeling is.. it's necessary to introduce the rules of the game we're playing if one has to more rigorously refine type. And to do that, deductive system and lambda calculus seem to be a must. To define a function, it seems that certain realistic or imaginary machine should be involded.. for example Turing machine. And are there other systems to be introduced, before defining rigorously what a type is? Also, a natural question then arises: can all these systems be rigorously defined?

Remark

I have to admit at the end that I might not fully understand what I'm asking. I know I'm in search of a full and rigorous definition of type.. but you might ask what I mean by "rigorous"? Well.. I don't know. How can I define "rigorous"? How can I define "define"? What is "what"? And what is "what is what"? ..? It might sound like I'm making fun of words, but I'm serious.

EDIT: Zhen Lin asked a great question in the comment, which helped me express my expectation through set theory.

@ZhenLin I'm much comfortable with set theory because I sort of know what are undefined. We start with a set of undefined symbols (characters) and make up strings. There are some symbols that are "special": " ", "(", ")", "$\exists$", "$\forall$, "$\wedge$, "$\to$... etc. There is a list of pre-defined rules, that tell us how to reduce one to another. There is a list of pre-defined axioms that tell us where we could start. There is a list of translation rules that translate what's in it to English. And then we obtain meanings from that..

Related

Student
  • 1,822
  • 3
    Let me turn this around. Do you feel comfortable with set theory? What is a set in set theory? How do you define it rigorously? If you are able to show us what level of answer you expect then perhaps we can give you an answer you might be happy with. – Zhen Lin Oct 14 '20 at 03:06
  • See B.Russel, PoM (1903), “Appendix B: The Doctrine of Types”: "if $x$ belongs to the range of significance of $\phi(x)$, then there is a class of objects, the type of $x$, all of which must also belong to the range of significance of $\phi(x)$". Thus, types are homogeneous groups of objects (terms) for which certain assertions make sense. – Mauro ALLEGRANZA Oct 14 '20 at 06:12
  • @ZhenLin I'm much comfortable with set theory because I sort of know what are undefined. We start with a set of undefined symbols (characters) and make up strings. There are some symbols that are "special": " ", "(", ")", "$\exists$", "$\forall$, "$\wedge$, "$\to$... etc. There is a list of pre-defined rules, that tell us how to reduce one to another. There is a list of pre-defined axioms that tell us where we could start. There is a list of translation rules that translate what's in it to English. And then we obtain meanings from that.. – Student Oct 14 '20 at 07:35
  • I'm totally fine with undefined terms.. I just hope that people treat it formally, and admit it loudly. There are many motivations for types out there.. but I haven't seen any that tells clearly what are undefined and what are not. – Student Oct 14 '20 at 07:39
  • 1
    Types and terms are undefined concepts. There are very many more special symbols than in set theory. Does that clarify things? – Zhen Lin Oct 14 '20 at 07:43
  • @ZhenLin a lot! Thank you! Has it been written up somewhere? I want to make sure what are undefined and what exactly are the rules of "the game". – Student Oct 14 '20 at 08:18
  • As others on MO have referred you to before, I suggest the appendices of the HoTT book. – Zhen Lin Oct 14 '20 at 08:40
  • Ok.. now I should write up why I think it isn't enough... Or maybe I will write up a version that I am happy with. In any case, thanks for your great help :) – Student Oct 14 '20 at 08:50
  • It feels to me like you're trying to have it both ways: a rigorous – to me, that means formalist – definition of term/type and an intuitive conceptual understanding of term/type. This requires two different answers. – Zhen Lin Oct 14 '20 at 09:11
  • @ZhenLin no.. I don't want an intuitive understanding of term/type. I want a formal definition, and that must include undefined things. I hope the undefined things can be pointed out loudly. – Student Oct 14 '20 at 09:55
  • Term and type are the only undefined notions in formal type theory. – Zhen Lin Oct 14 '20 at 10:05
  • That's assuming you have imported other systems, like the lambda calculus, right? In those systems, there seem to be other undefined notions as well. There are also a set of "rules of game". I'd hope all of these, starting from the very beginning, can be pointed out loudly. – Student Oct 14 '20 at 10:12
  • No, there are only types and terms in the ontology of type theory. A lambda calculus is a special kind of type theory. – Zhen Lin Oct 14 '20 at 10:18
  • @ZhenLin If I understand correctly, one still needs to define a type constructor, reduction rules (for each type), type inference rules.. etc. And really what's really a function? – Student Oct 14 '20 at 10:44
  • Type constructors, reduction rules, inference rules etc. do not exist in the ontology of type theory. They are not things you reason about in type theory; they are things you use. As for "function": this the conventional name for a term of function type. – Zhen Lin Oct 14 '20 at 11:07
  • Regarding you added part to the question, you are confusing symbols of the language of set theory (they are "defined" in the theory of first-order languages and logic) and objects that the theory deals with: obviously sets. – Mauro ALLEGRANZA Oct 14 '20 at 13:27
  • @MauroALLEGRANZA yes, I think that's where it caused confusion. So set theory depends on the definition of the language of first-order logic. In this vein, what does type theory depend on? – Student Oct 14 '20 at 16:33
  • Type theory is a formal system at the same level as first-order (or higher-order etc.) logic. If you look at a formal definition of first-order logic, particularly one based on sequent calculus, you will see many of the same devices as in type theory. – Zhen Lin Oct 14 '20 at 23:33

2 Answers2

1

Not "rigorous" but a "motivation"...

See Rob Nederpelt & Herman Geuvers, Type Theory and Formal Proof : An Introduction (Cambridge University Press, 2014), page 33:

In order to get a firmer hold on the desired behaviour of functions, we will introduce types in the present chapter. This is a natural thing to do: functions are usually thought of as acting on objects belonging to a certain collection, e.g. the collection of the natural numbers or the collection of points on a line. Therefore, it is quite customary to talk about a function on a domain, for example the function ‘square’ on the natural numbers.

Hence, the addition of types gives certain restrictions on the input values permitted: a function defined on domain $\mathbb N$ may only take natural numbers as input values, even when it would be quite clear what the output value would be for some ‘illegal’ input value. For example, ‘square’ on $\mathbb N$ permits us to calculate three-squared, but excludes by definition the squaring of three-and-a-half. We could, however, define ‘another’ squaring function on a larger domain, e.g. $\mathbb Q$ or $\mathbb R$, in order to make it applicable to three-and-a-half. On the other hand, such an extension of the domain is often impossible: the function ‘square root’ on the naturals may not be extended to a function ‘square root’ on the integers, since the square root of a negative number is non-existent in the normal conception of what it means to be a root (even when complex numbers are permitted as an answer, the square root of $−1$ does not exist, since both $i$ and $−i$ could serve as an answer).

And see page 34:

we discuss the intended meaning of the types. This is simple:

− type variables are abstract representations of basic types such as nat for natural numbers, list for lists, etcetera.

− arrow types represent function types, such as nat → real (the set of all functions from naturals to reals) or (nat → integer) → (integer → nat) (the set of all functions with input a function from naturals to integers and output a function from integers to naturals).

In a nutshell, it is an abstract representation of a mathematical universe made of objects of different sorts (numbers, lists) and function on them.

Mauro ALLEGRANZA
  • 94,169
1

Your question is very typical for a small class of individuals. Unfortunately, reduction to "first principles" is something you need to look for in the papers reprinted in sourcebooks, modern commentary written mostly by philosophers, and the arduous task of sifting through bibliographies. If you do so, you will find that different authors will use the same words differently. You will then be faced with deciding upon reconciliations that work for you personally.

With that said, almost all foundational literature begins with "motivation." Rarely does the technical development return to what serves as motivation to recover the heuristic under the formal. In my personal opinion, the HOTT book is utterly flawed for this reason. If you claim a foundation, its explanation does not belong in appendixes.

In so far as formalist foundations are associated with Hilbert, it essentially invokes the paraphrase of natural language fragments. There is no meaningful notion of definition. Its relationship to "language signatures" is closely bound to the study of symbolic algebras pursued in the tradition of British mathematics (de Morgan and Peacock). And, this had been motivated by the desire to do for logic what Newton had done for analytical geometry.

De Morgan speaks of "peculiar symbols," "meanings," and "rules of operation." Formalism is bound to peculiar symbols and rules of operation without meanings. But, de Morgan observes that the sign of equality is a exception. Substitutivity in a calculus requires a warrant.

This leads to the difference between Frege's logicism and Russell's logicism. With respect to intentionality, Frege's logic had been non-classical. Russell's interpretation of definite descriptions as a form of quantifier recovers classical ambivalence. But, this effectively undermines the generally understood role of definition with respect to first principles.

Russell's account of definite descriptions introduces the notion of "self-identity" into the jargon of logic and its defense of the law of identity. It also accounts for Russell's stipulation that "term" is to be identified with "individual." A term can clearly be stipulated to mean something else. But, this lies at the heart of first-order logic. Russell's recovery of classical bivalence depends upon the fact that collections are composed of individuals.

One influence on Russell had been Peano's distinction between membership and inclusion. Earlier authors had not made this distinction. It lies at the heart of extensionality and semantics.

However, although Russell had been committed to a logicist interpretation for the sign of equality, he considered other views. He has a chapter on "quantity and magnitude" in "Principles of Mathematics" in which he considers alternatives. His "relative equality" does not assume the necessity of reflexive equality statements, although they are provable. In a parenthetical remark that follows, he says that reflexive equality statements maybe assumed as a consequence to a "type" stipulation (If A be a number, then A=A).

Backtracking this even further, Aristotle's analysis of logic speaks of genera, species, in individuals. All of it involves "names." Individuals are associated with proper names and are referred to as "primary substances." Other names are "secondary substances." These would be comparable with "types."

You can get from Russell to HOTT by reading Martin-Lof.

Russell's account of foundations is bound to his logical atomism. One need not take that view. Category theory does not. Lawvere makes an oblique comment about how philosophy detoured away from mathematics because of how the logicists deprecated inclusion. Since HOTT uses a categorical notion of set, this is relevant to your question.

mls
  • 21