Construction Types or Type Constructions?

Question

In any (simple) type theory there are base types (i.e. the type of individuals and the type of propositions) and type builders (i.e. $\rightarrow$, which takes two types $t,t'$ and yields the type of functions $t \rightarrow t'$).

For each type in such a type theory there is a rooted ordered tree with

• base types as labels of leaves and
• type builders as labels of non-leaf nodes
  ("by which type builder this node is built?")

that shows how the corresponding type (i.e. the root) is built from base types.

What is the "official" name of such a tree when the base types are ignored (i.e. the labels of the leaves)?

[Formally: Two types have the same ??? when their corresponding trees are isomorphic upto labelling of the leaves.]

(Something like "type constructor" or "type construction" or "construction type"?)

As long as there is only one base type, this question is not very interesting. And when there are several base types, but of quite different nature - like individuals and propositions - it's not very interesting, too.

But what I think of is a type theory with several base types of the same kind (or nature) — like chemical elements. This leads to another question:

(How) can/are "base types of the same kind" be captured in type theory?

---

(See also: context-free grammars, parse tree, syntax tree, atomism/reductionism.)

Answer 1

Basically what you're considering seems to me as the type-operations which you can obtain from the basic type builders.

As you have guessed this objects should be the type constructors.

About the second part of the question type theory in general don't preclude the possibility of types of being terms of some other type. The idea is to consider a special type kind whose terms are called types which can be terms which inhabit them.

This construction is possible in type theories which allows it, for instance in univalent foundations there's a hierarchy of types whose terms are types.

Answer 2

I don't know about "official", but from what I understand you speak of a special kind of type contexts, where the "holes"---that is, the type placeholders in the context---are to be filled exclusively by base types (I'm borrowing the term context from some old experience of mine in algebraic semantics, where contexts make sense for trees in general).

To illustrate what I have in mind, consider a type system $\mathcal{T}$ built with arrows over, say, $\mathbb{N}$. I also need a symbol for the hole, the type placeholder; so I introduce a special type variable, say $\omega$, to stand for an unspecified base type---this is so to speak a base pseudo-type. I can then define the type contexts over $\mathcal{T}$ inductively by (i) $\omega$ is a type context, and (ii) if $\rho$ and $\sigma$ are types or contexts then $\rho \rightarrow \sigma$ is also a type context. Examples would be $\omega$, $(\mathbb{N} \rightarrow \omega) \rightarrow \mathbb{N}$, $\mathbb{N} \rightarrow (\omega \rightarrow \omega)$, $(\omega \rightarrow \omega) \rightarrow \omega$ et cetera.

Note that you would possibly need more base pseudo-types than one, if you have different proper base types and you want to reserve the right to fill in different base types to different placeholders.

Note also (aha, now that I read your original post again, I understand that this is most likely what you mean) that if you want that only the type constructors are specified---here, the arrow constructor---and leave all proper leaves out of the picture, you can accomodate the inductive definition above by allowing no proper types in the inductive step. Again, I don't know about "official", but the term skeleton comes to mind.

As to the second question about "kinds" (and again borrowing from algebraic semantics), you might try introducing different sorts of base types (the term to look up would be many-sorted algebras): if you want to play with, say, two kinds of types, $k$ and $l$, then I intuitively understand that $k = \{ \alpha_1, \ldots, \alpha_m \}$ and $l = \{ \beta_1, \ldots, \beta_n \}$; that is, all $\alpha_i$'s and $\beta_j$'s are base types of the kind $k$ and $l$ respectively. Surely, an inductive understanding of the special type contexts that you have in mind above, can be had in this generalized setting as well. EDIT: In this case of course your type constructors should be metatyped by kinds. My chemistry is unfortunately rusted to dirt these days, but (in danger of making a fool of myself) say that you can form some "bond" $b$ between "elements" of the kind $k$, $l$, and $k$ again, but not of the kind $k$, $l$, $l$; then you should specify your bond's "arity" by $b : k \times l \times k$. Something along these lines anyway.

Hope this algebraic-semantics take helps.