What is the term for types that are not type variables?

Question

In a language, some types are actually type variables. I am aware of three kinds of type variables:

1. Generic Parameter Types: In the declaration of Foo<T>, the T is a type that is a variable.
2. Associated Types: In languages like Scala, Swift, and Rust, a trait/protocol can have an associated type trait Foo { type T; }. Again, in the declaration of Foo, the T is a type that is a variable.
3. Self Types: In Swift and Rust, the type Self is a type variable.

What is an umbrella term for all types that are not type variables?

OR

What is an umbrella term for reference and value types that are not type variables?

(I need a short way to refer to these in my compiler and language spec.)

EDIT:

It appears many people misunderstood my question in a way I hadn't anticipated. I was trying to keep the explanation of type variables short because it wasn't the core of the question. It is just background information. However, that led to the confusion.

When I said "in the declaration of," I meant in the scope of the declaration of that thing. Let me try to clarify.

1. Generic Parameter Types:

public abstract class Foo<T>
{
    // Here T is a type, but not a specific one. It is a type variable.
    public abstract fn test() -> T; 
}

2. Associated Types

public trait Foo
{
    public abstract type T;
    // Here T is a type, but not a specific one. It is a type variable.
    public abstract fn test() -> T;
}

3. Self Types

public abstract class Foo
{
    // Here Self is a type, but not a specific one. It is a type variable.
    public abstract fn test() -> Self; 
}

My language is an OO language in the style of Swift, C#, Java, or Scala and has all three of Generic Parameter Types, Associated Types, and Self Types. It also has abstract classes.

An example of how I want to use this term:

In the compiler, I have a class hierarchy that represents types. Simplifying some, there is a class Type with a tree of subclasses including ones like OptionalType (i.e. x?), NeverType (i.e. the bottom type), SimpleType (i.e. primitive types), ValueType (i.e. like the types declared with struct in C#), ReferenceType, and GenericParameterType. There is a part of the heriarchy where the "type variables" split off. They have a lot in common and have a base class TypeVariableType 🤢. They can have constraints on the type but they have no actual properties. The other types, the non-type-variables also have a lot in common. I want a superclass for them. I need to name that superclass.

One answer brought up the term "ground type". That isn't what I am describing here. If test() above returned List<T>, that would be a non-type-variable type in my schema. That is because List<> is a reference type.

I am expecting this term to also be helpful in the language spec.

Answer 1

A concrete type may fit your description. It’s any type that’s not “abstract”, where the types of abstraction possible depend on the type system. For example:

• It’s not a type variable, if type constructors can be parameterised by such variables.

• It’s not a universally quantified type, if there’s first-class polymorphism.

• It’s not a reducible expression, if there’s any type-level computation or dependent typing.

  This is also called a normal form, if you want to avoid the term “concrete” in a context where you might already be using it for something else, such as subtyping.

A type can still be concrete in this sense even if it’s not ground or named. For example, say (x, y) is the type of a tuple of x and y, which are unsolved metavariables that stand for some concrete types, say T1 and T2. This is in weak head normal form, but not ground as long as x or y are unknown, yet we know it will be solved to a concrete type (T1, T2), which is concrete even though it doesn’t necessarily have a distinct name like Pair_T1_T2.

Answer 2

I can tell you what we did in the C# spec, and it is a cautionary tale; see if you can do better than we did.

• Generic types that have type arguments supplied are "constructed" types and also "bound" types.
• Generic types whose type arguments are not specified at all are "unbound". (This is rare; it only really happens in the context of the typeof operator and maybe a few other corners.)
• A non-generic type is both "bound" and "unbound", grrr. (That makes certain other sections of the spec easier to write.)
• All types are exactly one of "open" and "closed".
• Type parameters are open types.
• Arrays of open type are open types.
• Constructed types with at least one open type argument are open.
• Types that are not open are closed.

There was no jargon defined for "type that is not a type parameter" because we didn't need it when writing the spec. We did need "type that has no usage of a type parameter", and that's "closed".

Answer 3

You're actually asking about at least three different concepts, for which the concepts of “being” or “containing” a variable are different.

In a type definition (examples 1 and 2), what you're defining (Foo) is never a variable. Any parameter of the type is denoted by a variable. The number of parameters of a type definition is typically called its arity (“arity” is the number of parameters something has, whether it's a type, a function, etc.) This terminology is used, for example, in .NET, ML (§4.1). So a type definition with no parameters can be said to have arity 0, also called a nullary type. More generally, the “shape” of the parameters of a type is sometimes called a kind (which can be more complex than an integer if the language has, for example, higher-order kinds or named parameters for types). A type with no parameters is a type whose kind is the “base” kind. This terminology is used in Haskell, where the kind of nullary types is written $*$.

In a type expression (example 3), I can't think of a word that means that a type expression is not a variable, for example including int * T and list(T) while excluding T. A type expression that does not have any free variable is a ground type, following the general terminology used in term rewriting. For example, int * bool and list(int) are ground types, whereas int * T and list(T) are not. Note that in some languages, a type expression can include bound variables; $\forall \alpha, (\mathtt{list}(\alpha) \to \mathtt{int})$ is a ground type while $\mathtt{list}(\alpha) \to \mathtt{int}$ is not. A type expression with no variables appearing anywhere would have to be a quantifier-free ground type.

In your revised question, it looks like you're interested in the top-level aspect of the type: the node at the root of the parse tree of the type expressed in its canonical form. For example * (or Tuple or whatever your language calls it) for something like int * T, list for list(int), int for int, T for a type variable, forall for a quantifier $(\forall \alpha, \ldots)$, etc. The node at the root is usually called the head. If the head isn't a variable, it's probably a constructor. int is a nullary constructor, list and Optional are unary constructors, Tuple is a constructor of variable arity, etc. Each struct is a constructor (struct itself isn't a constructor, it's a way to define new constructors). NeverType may or may not be a constructor, depending on how you model it (a type constructor with subtype declarations, or a separate form of types that can unify with anything).

Answer 4

In a language, some types are actually type variables.

Which language? I would simply say that a type is a type, and a type variable is a variable that refers to a type, not a kind of type itself.

Usually, one talks about generic functions, whose types may involve one or more type variables. Your examples using List would be better described as a parameterized type, with List<Int>, List<Char>, List<T>, etc, being examples of the type being "indexed" with either concrete types or type variables.

An associated type isn't really a kind of type, but a kind of type-valued attribute.

Self is not a type at all, just a kind of "reference" to some other type. In the case of your Foo.fn example, fn's return value is whatever type is used to invoke it, either Foo or a subclass of Foo.

Answer 5

I'd just call them paravariables. Why do you need anything more complicated?

I suppose if you need to name that set as a syntactic element, which is completely reasonable, you could just call them nonvariables, because they are the complement of the set of variables.

I'm sure there's a reason for this concern, but it's one of many things I don't understand.