Type constructors and type constants (and type variables) : What's the difference?

Question

I am confused about the difference between type constructors, type constants, and type variables.

The Haskell 98 report says there are 4 types of type expressions:

1. Type variables
2. Type constructors
3. Type application
4. Parenthesized type

So then what's a type constant? The report says "Char, Int...are type constants" but I can't find a more detailed example. Even more confusing is how IO is first called a "unary type constructor," but then referred to as a "a constant, IO".

The reason I ask is because of this paper on Haskell's type system implementation. In it, it says this:

Haskell type expressions are either type variables or constants (each of which has an associated kind), or applications of one type to another: applying a type of kind k1 -> k2 to a type of kind k1 produces a type of kind k2

It's saying something different than the report. Is the second type of type expressions "constructors" or "constants"?

The paper also includes code showing the representation:

data Type  = TVar Tyvar | TCon Tycon | TAp  Type Type | TGen Int
             deriving Eq

data Tyvar = Tyvar Id Kind
           deriving Eq
data Tycon = Tycon Id Kind
           deriving Eq

Apparently Tycon stands for "type constructor," but then what does TCon represent? What about Tyvar and TVar? Why is there the need to seperate the T and Ty?

Answer 1

Last question

Apparently Tycon stands for "type constructor," but then what does TCon represent? What about Tyvar and TVar? Why is there the need to seperate the T and Ty?

first.

The 'T' in TCon, TVar etc. is just a marker that the concern is types and that they're constructors of the type Type. TCon takes a value of type Tycon and constructs a value of type Type from that etc. The constructor of Type isn't prefixed with Ty but rather only T to avoid confusion, the type could have been defined

data Type = Tyvar Tyvar | Tycon Tycon | ...

since value constructors and types live in different namespaces, but that would have opened up the road for far more confusion.

1 Type variables

are type expressions that can be substituted with other type expressions, their identifiers start with lower case letters (or they can be symbols not starting with ':').

2 Type constructors

are type expressions taking zero or more type expression arguments to construct a type of kind *, for example

• Int
• Char
• Double

are nullary type constructors, they take zero type expression arguments to construct a type of kind *, these are also type constants.

• Maybe
• IO
• []

are unary type constructors, they take one type expression (of kind * in these examples, but unary type constructors can take arguments of other kinds too).

• Either
• (,)

are binary type constructors,

• StateT

is a ternary type constructor, taking two arguments of kind * and one of kind * -> * (the kind of StateT is thus StateT :: * -> (* -> *) -> * -> *).

3 Type application

is a type expression of the form t1 t2. It is only well-formed if t2 has kind k2 and t1 has kind k2 -> k3 (analogous to function application). For example StateT s is a type application, the type expression StateT is applied to the type variable s.

4 Parenthesized type

is a type expression in parentheses, that may be necessary for precedence resolution or parsing, otherwise it's the same as the unparenthesized type expression, for example in

instance Monad (Either e) where ...

the parenthesized type expression (Either e) is the same as Either e, but the parentheses are necessary to distinguish it from an instance of a two-parameter class for the two type expressions Either and e. In the type

StateT s ((->) a) b

the parentheses around (->) a are for precendence. (Note, the type constructor (->) is a special case not covered by the general rule that type constructors begin with upper case letters, as [], (,), (,,) etc.)

Now, type constants. Those are just type expressions containing no type variables, but I don't think it's formally defined anywhere. So any type expression with only uppercase identifiers (including symbols starting with ':') and the special cases ([], (->), (,), ...) is a type constant.

• single token type expressions starting with an uppercase letter (':' for symbols) or the special cases are type constants
• a type expression consisting entirely of type constants is a type constant

Answer 2

Is the second type of type expressions "constructors" or "constants"?

There is no reason for being confused.

Look, we can say that 5 is a value constructor, because it constructs the value 5. And at the same time we can say that 5 is a constant.

Another example: in the Maybe type we have

data Maybe a = Just a | Nothing

Both Just and Nothing are value constructors. It is easy to understand that Nothing is also a constant. It may be harder to understand that Just is also a constant: it denotes a function that, given any value, constructs a value of type Maybe. If you find that hard to understand, imagine that there will be some machine code in the memory of a program using Just that actually performs the task of construction of Maybe values. This code does never change, hence it is constant, and Just is how we refer to this constant.

Now we understand what constant and constructor mean in the realm of values, we can extend this to the realm of types.

Answer 3

In type theory, "type constructor" typically refers to a type expression of higher kind. By extension, plain types are often included as a degenerate case.

In programming languages, "type constructor" is often used with a more specific meaning, referring to named type constructors that are defined by the context. Again, this can include plain types as the degenerate case with zero parameters.

The term "type constant" is somewhat less standard. In the Haskell definition, it seems to be used rather informally, and probably is meant to denote the subset of named type constructors that is pre-defined by the language (as opposed to user-defined type constructors, which are defined in terms of algebraic types and the pre-defined type constructors). Consequently, every constant is also a type constructor.

As for "T" vs "Ty", that just seems to be a naming convention in the piece of code you are looking at, intended to differentiate between language-level data constructors ("T") and language-level type constructors ("Ty"). The reason that it factors out the definition of Tycon and Tyvar into separate type definitions is probably that they are used separately by some pieces of the code.