Can type constructors be considered as types in functional programming languages?

Question

I am approaching the Haskell programming language, and I have a background of Scala and Java developer.

I was reading the theory behind type constructors, but I cannot understand if they can be considered types. I mean, in Scala, you use the keywords class or trait to define type constructors. Think about List[T], or Option[T]. Also in Haskell, you use the same keyword data, that is used for defining new types.

So, are type constructors also types?

Answer 1

Let's look at an analogy: functions. In some branches of mathematics, functions are called value constructors, because that's what they do: you put one or more values in, and they construct a new value out of those.

Type constructors are exactly the same thing, except on the type level: you put one or more types in, and they construct a new type out of those. They are, in some sense, functions on the type level.

Now, to our analogy: what is the analog of the question you are asking? Well, it is this: "Can value constructors (i.e. functions) be considered as values in functional programming languages?"

And the answer is: it depends on the programming language. Now, for functional programming languages, the answer is "Yes" for almost all (if not all) of them. It depends on your definition of what a "functional programming language" is. Some people define a functional programming language as a programming language which has functions as values, so the answer will be trivially "Yes" by definition. But, some people define a functional programming language as a programming language which does not allow side-effects, and in such a language, it is not necessarily true that functions are values.

The most famous example may be John Backus' FP, from his seminal paper Can Programming Be Liberated from the von Neumann Style? – a functional style and its algebra of programs. In FP, there is a hierarchy of "function-like" things. Functions can only deal with values, and functions themselves are not values. However, there is a concept of "functionals" which are "function constructors", i.e. they can take functions (and also values) as input and/or produce functions as output, but they cannot take functionals as input and/or produce them as output.

So, FP is arguably a functional programming language, but it does not have functions as values.

Note: functions as values is also called "first-class functions" and functions that take functions as input or return them as output are called "higher-order functions".

If we look at some types:

1   :: Int
[1] :: List Int
add :: Int → Int
map :: (a → b, List a) → b

You can see that we can easily say: any value whose type has an arrow in it, is a function. Any value whose type has more than one arrow in it, is a higher-order function.

Again, the same applies to type constructors, since they are really the same thing except on the type level. In some languages, type constructors can be types, in some they can't. For example, in Java and C♯, type constructors are not types. You cannot have a List<List> in C♯, for example. You can write down the type List<List> in Java, but that is misleading, since the two Lists mean different things: the first List is the type constructor, the second List is the raw type, so this is in fact not using a type constructor as a type.

What is the equivalent to our types example above?

Int     :: Type
List    :: Type ⇒ Type
→       :: (Type, Type) ⇒ Type
Functor :: (Type ⇒ Type) ⇒ Type

(Note, how we always have Type? Indeed, we are only dealing with types, so we normally don't write Type but instead simply write *, pronounced "Type"):

Int     :: *
List    :: * ⇒ *
→       :: (*, *) ⇒ *
Functor :: (* ⇒ *) ⇒ *

So, Int is a proper type, List is a type constructor that takes one type and produces a type, → (the function type constructor) takes two types and returns a type (assuming only unary functions, e.g. using currying or passing tuples), and Functor is a type constructor, which itself takes a type constructor and returns a type.

Theses "type-types" are called kinds. Like with functions, anything with an arrow is a type constructor, and anything with more than one arrow is a higher-kinded type constructor.

And like with functions, some languages allow higher-kinded type constructors and some don't. The two languages you mention in your question, Scala and Haskell do, but as mentioned above, Java and C♯ don't.

However, there is a complication when we look at your question:

So, are type constructors also types?

Not really, no. At least not in any language I know about. See, while you can have higher-kinded type constructors that take type constructors as input and/or return them as output, you cannot have an expression or a value or a variable or a parameter which has a type constructor as its type. You cannot have a function that takes a List or returns a List. You cannot have a variable of type Monad. But, you can have a variable of type Int.

So, clearly, there is a difference between types and type constructors.

Answer 2

Well, types and type constructors have a calculus of their own and they each have kinds. If you use :k (Maybe Int) in ghci for example, you'll get *, now this is a proper type and it (usually) has inhabitants. In this case Nothing, Just 42, etc. * now has a more descriptive alias Type.

Now you can look at the kind of the constructor that is Maybe, and :k Maybe will give you * -> *. With the alias, this is Type -> Type which is what you expect. It takes a Type and constructs a Type. Now if you see types as set of values, one good question is what set of values do Maybe has? Well, none because it is not really a type. You might attempt something like Just but that has type a -> Maybe a with kind Type, rather than Maybe with kind Type -> Type.

Answer 3

At least in Haskell, there is a hierarchy that can roughly be described as follows.

Terms are things that exist at run-time, values like 1, 'a', and (+), for example.

Each term has a type, like Int or Char or Int -> Int -> Int.

Each type has a kind, and all types have the same kind, namely *.

A type constructor like [], though, has kind * -> *, so it is not a type. Instead, it is a mapping from a type to a type.

---

There are other kinds as well, including (in addition to * and * -> *, with an example of each):

• * -> * -> * (Either)
• (* -> *) -> * -> * (ReaderT, a monad transformer)
• Constraint (Num Int)
• * -> Constraint (Num; this is the kind of a type class)