What are the differences and relations between a type constructor and a type operator?

Question

What are the definitions of a type constructor and a type operator? What are their differences and relations? I think a type operator is a function whose parameters are n types and return is a type. A type constructor also means the same thing. I use them exchangeably. But some reply used type constructor when my question (I forgot where) used type operator. In Types and Programming Languages by Pierce, the index says

type constructors, see type operators

Ch 29 says informally that

these type-level functions, collectively called type operators, more formally.

Is it correct that type operators/constructors are used only and exactly to create algebraic types, and algebraic types are created only and exactly by type operators/constructors?

Is Ref in Ref T a type operator/constructor? Is Ref T an algebraic type?

Thanks.

Answer 1

These sorts of terms in type theory are not always used completely consistently. However, type operators are generally type-level functions: that is, they take as arguments some number of types and return a single type. Type constructors are a specific kind of type operator for which the return type is free in the sense that it is a new type on its arguments.

Generally speaking, if you have a type operator $T: \star \to \star$ and for any type $A : \star$, you have a type $T(A) : \star$, which is not prima facie equal to anything else, then it is called a type constructor.

For example, $\times$, $+$ and $\to$ are all type constructors. Type-level application is not, because the application of $(\lambda X . X + X)\ Y$ is reducible to $Y$, i.e. the application of the type operator is equal to some other type.

In your example, $\mathrm{Ref} : \star \to \star$ would be considered a type constructor. If by "algebraic type" you mean "algebraic data type", then $\mathrm{Ref}(T)$ is not an algebraic data type, because it's part of the type system rather than formed as a composite type out of products and sums.