Robert Constable, in his article “Computational Type Theory” (Constable 2009):

Computational type theory [CTT] answers questions such as: What is a type? What is a natural number? How do we compute with types? How are types related to sets? How are data types for numbers, lists, trees, graphs, etc. related to the corresponding notions in mathematics? Do paradoxes arise in formulating a theory of types as they do in formulating a theory of sets?

The first question is decisive for CTT’s answers to the all the rest, and it is the focus of this section. We would like to articulate what a type is from the perspective of “type theory” in general, but we begin by looking at CTT in particular.

In formulating his account of types (for a popular audience), Constable drives the question “what is a type?” back to the question “what is a term?”:

What is a type? To answer this question, we must first be more precise about computation; we will see that the notion of a type is ultimately grounded in computation, specifically in concrete linguistic expressions because computation in the physical world is ultimately symbolic. We are only interested in computation that is physically realizable by explicit, verifiable human actions and by machines that humans understand. Thus to explain types, we first need to explain terms and how to compute with them.

(Constable 2009)

Let us fix some set of terms (symbols), \(T\), and an operational semantics, telling us how to compute certain elements \(t_1, ..., t_n \in T\) from other elements \(t'_1, ..., t'_n \in T\), via the relation \(\to\), such that \(t' \to t\) reads “\(t'\) reduces to \(t\)”. We say a term in \(T\) is “irreducible” if it is only reducible to itself: \(t \to t\). Such a term is called “canonical”. That this sets up a (partial) ordering over a set of signs.¹

We might expect that more complex signs reduce to simpler ones, and this is often the case, but we haven’t actually placed any constraint that enforces this kind converge upon atomic elements. The canonical signs serve as points of rest, in our system, but there is no requirement enrcing in the sense that they cannot be further reduced to simpler components.

Having established such a system of signs, we define types over the canonical elements by delimiting collections of terms that belong together, and stipulating how to determine if any two terms in such a collection are to taken as equal:

To define a type we specify a collection of canonical terms which are the canonical elements of the type, and we define an equality relation declaring when two canonical terms denote the same abstract object. The equality relation creates abstract objects out of terms.

(Constable 2009)

Note that these types presuppose the construction of ideal (abstract) objects, on the basis of positing equality between concrete objects: “The equality relation creates abstract objects out of terms.”. Existence precedes essence, and essence is “created” through acts of gathering (terms that belong together) and equalization (of terms that are taken to be the same).

The roots of type theories, computational or otherwise, extend back through the history of philosophy, at least to Aristotle (Constable 2009).

In Types as Theories, Goguen denies that “type theory” advances a general theory of types, in arguing instead that it presents a theory based on a specific, limited notion of “type”:

In the “types as predicates” variant of the “types as sets” approach, types are taken to be predicates, which therefore denote sets (or some variant thereof, such as domains). However, many advocates of this view are more proof theoretically inclined, and hence might resist such denotations. Perhaps the best known work along this line is Martin-Löf’s “type theory”, which also provides dependent types, as implemented in Pebble and other languages. (Note that “type theory” is not a general theory of types, but rather a specific intuitionistic logic which provides one specific notion of type).

(Programming and Goguen 1991)

Goguen counters the “types as predicates” view with another interpretation, which he calls “types as theories” or “types as algebras”:

The essential insight of the “types as algebras” notion is that the operations associated with data are at least as important as the values. Thus, the this approach generalized from [types as] sets to algebras, which are just sets with some given operations.

(Programming and Goguen 1991)

Let’s lean on the proof-theory side of types-as-propositions and recall (what I believe to be) a key insight of Gentzen’s approach:

To every logical symbol … belongs precisely one inference figure which ’introduces’ the symbol - as the terminal symbol of a formula - and one which ’eliminates’ it. … The introductions represent, as it were, the ’definitions’ of the symbols concerned, and the eliminations are no more than, in the final analysis, than the consequences of these definitions. This fact may be expressed as follows: In eliminating a symbol, we may use the formula with whose terminal symbol we are dealing only ’in the sense afforded by the introduction of that symbol’.

(edited by M. E. Szabo 1969)

That is, the meaning of the logical connectives (i.e., the correspondents of the principle types in the various type theories) is given by their introduction and elimination rules. From the Curry perspective on typing, I think we can say that the intro/elim rules are (partial) operations on the sets of derivations in the lambda calculus (since a set of derivations is a set of programs, which is a set of proofs, which is the meaning of a proposition according to the perspective of proof-theoretic semantics). If this is correct, I think we have a perspective from which we can say that the meaning of the types in our systems are indeed given by the operations belonging to each type (i.e., the particular sets of operations which carve out patterns of permitted connections within the sets of derivations of the lambda calculus).

As alternative to equality as determinations of “type” could we base types on the two relationships of material incompatibility and consequence, as per Robert Brandom?

A # B

A is incompatible with B

A |~ B

B is a material consequence of A