Skip to main content
  1. Posts/

What List is when it's not a type

·6 mins
Rafael Fernandez
Author
Rafael Fernandez
Mathematics, programming, and life stuff

Int is a type. String is a type. List[Int] is a type. List is not a type.

That sentence usually irritates people the first time they see it. It sounds like a trick. It sounds like one of those lines someone drops in a talk just to seem more profound than necessary. Because, honestly, List is everywhere. You use it all the time. How could it possibly not be a type?

But write this in the Scala REPL and look at what happens:

val x: List = ???
// error: List takes type parameters

What is happening here is less exotic than it sounds. List on its own is unfinished. It is missing information. It needs a type argument before it becomes something you can use as a type. List is, in a very practical sense, a machine for making types. Give it Int and you get List[Int]. Give it String and you get List[String]. Without that argument, the machine is there, but it has not produced a complete type yet.

This kind of thing has a name: a type constructor.

what-list-is-when-it-is-not-a-type-img-7.svg

The level above types
#

To understand type constructors, it helps to step back for a second and ask what a type actually does. A type classifies values. Int classifies the value 42. String classifies "hello". List[Int] classifies List(1, 2, 3). Types live one level above values.

Type constructors live one level above types. They do not classify values. They classify, or more accurately transform, types. List takes a type and produces a type. Option takes a type and produces a type. Either takes two types and produces a type.

And this level above types has its own vocabulary: kinds. The shortest way to say it is this: a kind is to a type what a type is to a value.

A proper type like Int or String has kind * (read: “star” or, if you want a less ceremonial phrasing, “complete type”). It is a type that can classify values directly.

A type constructor like List has kind * -> *. It takes one type of kind * and produces another type of kind *. The arrow notation mirrors ordinary function notation, and that resemblance is not accidental: Int -> String is a function from values to values, while * -> * is a “function” from types to types.

Either has kind * -> * -> *. It needs two type arguments before it becomes a proper type. Map works the same way.

Why this actually matters
#

Most of the time, you never think about kinds, and that is fine. Scala infers them, and the compiler complains loudly when something does not fit. But there is a point where kinds stop being a theoretical curiosity and become unavoidable: when you want to write code that abstracts not over concrete types, but over whole families of types.

Functor is the classic example. A functor is, roughly speaking, something you can map over. List, Option, and Either[String, _] all fall into that category. And sooner or later, you want an abstraction that works for all of them:

trait Functor[F[_]] {
  def map[A, B](fa: F[A])(f: A => B): F[B]
}

Look at F[_]. This is Scala’s way of saying: “F is a type constructor that expects one type argument.” You are no longer abstracting over a concrete type like Int. You are abstracting over something like List or Option. Functor[F[_]] has kind (* -> *) -> *: it takes a type constructor of kind * -> * and produces a proper type.

That is what higher-kinded type means: a type parameterized by a type constructor rather than a proper type. The name sounds heavier than the idea. In practice, it just means you have moved up one level of abstraction.

Seeing it in criteria4s
#

If you have been reading the criteria4s series, you have already seen higher-kinded types in real code, even if you did not have a name for them yet.

Show is a binary type constructor:

trait Show[-V, D <: CriteriaTag] {
  def show(v: V): String
}

Show by itself is not a complete type. Show[Int, SQL] is. Show has kind * -> * -> *.

BuilderBinary is higher-kinded:

trait BuilderBinary[H[_ <: CriteriaTag]] {
  def build[T <: CriteriaTag](F: (String, String) => String): H[T]
}

H[_ <: CriteriaTag] says: H is a type constructor that takes one type argument, with the condition that the argument must be a subtype of CriteriaTag. When you write BuilderBinary[EQ], you are passing the type constructor EQ as the argument for H. EQ by itself is not a complete type: EQ[SQL] is a type, EQ[MongoDB] is a type, but EQ alone is a type constructor of kind * -> *, restricted to CriteriaTag subtypes.

BuilderBinary[H[_ <: CriteriaTag]] has kind ((* -> *) -> *) -> *: it takes a type constructor and produces a proper type. That is the (* -> *) part wrapped in another layer.

It sounds more intimidating than it really is. In practice, you read it like this: BuilderBinary knows how to build instances for any predicate type class, as long as that type class is parameterized by a dialect. The type system is describing something very general, but the underlying idea is still simple: we are abstracting one level higher.

How Scala 3 writes this
#

At this point, Scala 3 syntax starts looking less like a puzzle. [F[_]] means “F is a type constructor with one type parameter.” And yes, you can add constraints:

// F takes one type parameter, unconstrained
def example[F[_]](...)

// F takes one type parameter that must extend CriteriaTag
def example[F[_ <: CriteriaTag]](...)

// F takes two type parameters
def example[F[_, _]](...)

You will also see F[_] in context bounds or in type aliases when someone wants to name a particular family of type constructors. The _ is a placeholder: “there is a type parameter here, but I do not need to name it right now.”

The short version
#

  • A proper type (Int, List[Int]) has kind *. It classifies values.
  • A type constructor (List, Option) has kind * -> *. It takes a type and produces a type.
  • A higher-kinded type is a type parameterized by a type constructor, written F[_] in Scala 3.
  • Kinds classify types, in the same way types classify values.

You do not need to think about kinds every day. But when you run into F[_] in a trait definition, or when the compiler says type constructor expected but type found, it stops sounding like an esoteric error. Now you know what it is trying to tell you. And, with a bit of luck, also why List is sometimes not a type.