Skip to main content
another interpretation: the head of the type expression
Source Link

You're actually asking about at least twothree 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).

You're actually asking about at least two 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.

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

Source Link

You're actually asking about at least two 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.