The type system has a type system

In the companion post I introduced type constructors, kinds, and higher-kinded types through the lens of Scala 3 syntax. That post was practical: here is the concept, here is the code, here is why the compiler cares.

This post goes one level deeper. The concepts behind F[_] did not originate in programming. They come from category theory, and the correspondence between the two fields is not a loose analogy. It is structural. Type constructors are functors. Polymorphic functions are natural transformations. Kinds are a simply-typed lambda calculus. And parametric polymorphism gives you naturality conditions for free, without proving anything.

If you have read Syntax and Semantics 3 or the tagless final post, you already have the intuition. This post makes it precise.

The category we pretend exists

#

Before we talk about functors, we need a category. In programming, the standard candidate is Hask: the category where objects are types and morphisms are functions.

The category laws (associativity of composition, identity as neutral element) hold for pure functions. But there is a catch: Hask is not technically a category in the strict sense. Andrej Bauer showed in 2016 that the presence of bottom values (???, non-termination, null) breaks the identity law. In Haskell, seq can distinguish undefined from undefined . id, violating f . id = f.

The pragmatic response, which the entire functional programming community adopts, is to work in “Platonic Hask”: the total fragment where every computation terminates and no bottom values exist. In this fragment, the category laws hold, and the intuitions are correct. For the rest of this post, Hask means Platonic Hask.

Type constructors are endofunctors

#

A functor F: C -> D between two categories maps objects to objects and morphisms to morphisms, preserving identity and composition:

• Object mapping: For each object A in C, an object F(A) in D
• Morphism mapping: For each morphism f: A -> B, a morphism F(f): F(A) -> F(B)
• Laws: F(id) = id, and F(g . f) = F(g) . F(f)

When C and D are the same category, F is an endofunctor.

List is an endofunctor on Hask. The object mapping is the type constructor itself: List maps the type Int to the type List[Int]. The morphism mapping is map: given f: A => B, you get List[A] => List[B].

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

The functor laws translate directly:

// Identity: mapping identity does nothing
xs.map(identity) == xs

// Composition: mapping a composition equals composing the maps
xs.map(f andThen g) == xs.map(f).map(g)

The type class Functor[F[_]] is a certification that F is an endofunctor on Hask. The F[_] syntax requires F to have kind * -> *, which is exactly what “endofunctor on Hask” means: a mapping from types to types.

Polymorphic functions are natural transformations

#

A natural transformation alpha: F => G between two functors F, G: C -> C is a family of morphisms, one for each object A:

alpha_A : F(A) -> G(A)

satisfying the naturality condition: for every morphism f: A -> B,

G(f) . alpha_A  =  alpha_B . F(f)

Drawn as a commutative diagram:

        alpha_A
 F(A) ---------> G(A)
  |                |
  | F(f)           | G(f)
  |                |
  v                v
 F(B) ---------> G(B)
        alpha_B

Both paths from F(A) to G(B) must give the same result.

In Scala, headOption is a natural transformation from List to Option:

def headOption[A](xs: List[A]): Option[A] = xs.headOption

The naturality condition says:

// These must be equal for all f: A => B
list.map(f).headOption  ==  list.headOption.map(f)

It does not matter whether you first transform the elements and then extract the head, or first extract the head and then transform it. The natural transformation commutes with the functor’s map.

You can encode natural transformations explicitly in Scala 3:

// FunctionK: a natural transformation from F to G
trait ~>[F[_], G[_]]:
  def apply[A](fa: F[A]): G[A]

val headOpt: List ~> Option = new (List ~> Option):
  def apply[A](fa: List[A]): Option[A] = fa.headOption

Or using Scala 3’s polymorphic function types:

val headOpt: [A] => List[A] => Option[A] =
  [A] => (xs: List[A]) => xs.headOption

Parametricity gives you naturality for free

#

Here is the remarkable fact. In general category theory, you must prove the naturality condition for each natural transformation. In Hask, you do not. Parametric polymorphism proves it for you.

Philip Wadler showed in 1989 that the type signature of a parametrically polymorphic function, by itself, implies a theorem that any implementation must satisfy. His technique translates types into relations: the free theorem for a polymorphic function between functors is exactly its naturality condition.

For any function r: [A] => List[A] => List[A], the free theorem is:

r(list.map(f)) == r(list).map(f)

This holds because r cannot inspect or produce values of type A. All it can do is rearrange, drop, or duplicate list positions. Parametricity (the inability to examine a type parameter) forces the same structural behavior regardless of the element type, which is precisely what naturality requires.

The deep connection: in a language with parametric polymorphism, every polymorphic function between functors is automatically a natural transformation. You get naturality for free.

Kinds as a type-level lambda calculus

#

Mark P. Jones formalized this in his 1995 paper on constructor classes. The kind system is a simply-typed lambda calculus at the type level:

k ::= *           -- proper types (base type)
    | k1 -> k2    -- type constructors (function type)

This mirrors exactly the grammar of the simply-typed lambda calculus (STLC):

tau ::= Base       -- base type
      | tau -> tau  -- function type

Just as the STLC has term-level variables, abstraction, and application, the kind system has type-level variables, type abstraction (type lambdas in Scala 3), and type application (applying a type constructor to an argument).

Scala 3 makes type lambdas explicit:

// A type lambda: partially apply Either, fixing the left to String
type StringOr = [X] =>> Either[String, X]
// StringOr has kind * -> *

// This lets you use Either (which has kind * -> * -> *) where * -> * is expected
given Functor[StringOr] with
  extension [A](e: Either[String, A])
    def map[B](f: A => B): Either[String, B] = e.map(f)

The [X] =>> Either[String, X] is type-level lambda abstraction. StringOr[Int] is type-level application, producing Either[String, Int].

Kind polymorphism (Scala 3’s AnyKind, Haskell’s PolyKinds) goes further: it allows a type parameter to range over all kinds, not just *. This is useful for type-level tags and phantom types that should work at any kind.

The Yoneda lemma, briefly

#

The Yoneda lemma is one of the most important results in category theory. For a functor F: C -> Set and an object A in C:

Nat(Hom(A, -), F) ≅ F(A)

The set of natural transformations from the representable functor Hom(A, -) to F is isomorphic to the set F(A).

In Scala, this becomes the Yoneda encoding:

// Yoneda[F, A] ≅ F[A]
trait Yoneda[F[_], A]:
  def apply[B](f: A => B): F[B]

def toYoneda[F[_]: Functor, A](fa: F[A]): Yoneda[F, A] =
  new Yoneda[F, A]:
    def apply[B](f: A => B): F[B] = fa.map(f)

def fromYoneda[F[_], A](y: Yoneda[F, A]): F[A] =
  y.apply(identity)

The practical consequence: Yoneda[F, A] fuses chained map calls. When you chain y.map(f).map(g).map(h), the Yoneda encoding reduces this to a single y.map(f andThen g andThen h) automatically, because map on Yoneda is just function composition. No intermediate structures are created.

The dual construction, CoYoneda, gives you a free functor: it makes any type constructor (even one without a Functor instance) behave as a functor. This is the basis for many free monad implementations.

The correspondence table

#

References

#

• Mark P. Jones, “A system of constructor classes: overloading and implicit higher-order polymorphism”, Journal of Functional Programming 5(1), 1995. The paper that introduced kinds into Haskell’s type class system and made Functor, Monad, etc. possible as constructor classes.

• Philip Wadler, “Theorems for free!”, FPCA ‘89, 1989. Shows that the type signature of a parametrically polymorphic function implies a theorem (the “free theorem”) that any implementation must satisfy. For functions between functors, the free theorem is the naturality condition.

• Andrej Bauer, “Hask is not a category”, 2016. A rigorous argument that bottom values and seq break the category laws in Haskell. The pragmatic response is to work in “Platonic Hask” where all computations terminate.

• Bartosz Milewski, Category Theory for Programmers, 2018. Chapters on functors, natural transformations, and the Yoneda lemma, written for programmers with Haskell and C++ examples. An adapted Scala edition exists.

• Scala 3 documentation: Type Lambdas, Kind Polymorphism. The official reference for Scala 3’s kind system and type-level lambda syntax.