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
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.