Illustrated guide to Types, Sets and Values

Originally published on Medium in 2019. This version uses Scala 3.

Scala version used: 3.9.0
Latest revision: Sep 23, 2026

This document is a graphical exploration of the relationship between Types, Sets and Values.

The goal is to help develop an intuition about types by representing them graphically in a very concrete way: as labels or post-its attached to expressions.

Audience: Beginner.

We'll be talking about two different notions of functions:

i) Mathematical functions. They are abstract, and can be defined between two arbitrary Sets. They "live" in our heads, so to speak.

We'll use the notation A → B in this case.

ii) Scala functions and methods. We'll use A => B in this case.

The two notions are not the same: a Scala function corresponds to a mathematical function only when it is pure, and there are many mathematical functions that are not expressible as Scala functions.

1. Preliminaries

1.1 Types as labels

We'll start by declaring types to be just labels (think of tags / post-its, etc) assigned to expressions.

1.2 Types and values

Let's call $\mathbb{T}$ the set of all types, $\mathbb{V}$ the set of all values, and consider the function $V$ that maps each type to its set of possible values:

Note: $\mathcal{P}(\mathbb{V})$ is the power set of $\mathbb{V}$ (the set of all its subsets).

As you can see, the function $V$ allows us to distinguish values of different characteristics from each other.

In a dynamic language such as Python on the other hand, all values have a single label assigned to them, which we can call Dynamic.

You might be thinking that even in Python there are different kinds of values: numbers, lists, dicts, etc.

This is true: they have different representations in memory, and the interpreter checks the difference when it runs the code. But nothing checks it before the program runs: Python will happily start to evaluate 1 / "one", and only then throw an exception.

>>> 1 / "one"
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for /: 'int' and 'str'

(Optional type checkers such as mypy add static types to Python, but the language itself doesn't need them.)

What about people writing or reading the program? Well, we try to be aware of such a difference, with varying degrees of success.

So when we talk about types, we are talking about a static property that the typechecker can verify without running the code, not the specifics of the in-memory binary representation of values at runtime.

Further reading: the function $V$ is more than a teaching device. In the literature it is the interpretation of types, usually written $\llbracket A \rrbracket$, and it is a standard tool to prove that a type system is sound.

• John C. Reynolds, The Meaning of Types: From Intrinsic to Extrinsic Semantics (2000). Compares the view of this post, where values come first and a type is a property that a value can have ("extrinsic"), with the view where each term has exactly one type ("intrinsic").
• Robin Milner, A Theory of Type Polymorphism in Programming (1978). Interprets each type as a subset of a domain of values, and uses this to prove that "well-typed programs cannot go wrong".
• Amin Timany, Robbert Krebbers, Derek Dreyer and Lars Birkedal, A Logical Approach to Type Soundness (2024). The modern form of the same idea: $V(A)$ is the value interpretation $\mathcal{V}\llbracket A \rrbracket$ of a logical relation. Scala Step-by-Step (2020) uses it to prove the soundness of DOT, a core calculus of Scala.
• Giuseppe Castagna and Alain Frisch, A Gentle Introduction to Semantic Subtyping (2005). Defines $A \mathrel{<:} B$ as $V(A) \subseteq V(B)$, with union and intersection types as the set operations of section 5.

The simple picture has limits. For example, polymorphic types have no naive set-theoretic model: see Reynolds, Polymorphism is not Set-Theoretic (1984).

1.3 Some examples of types and corresponding set of values

In this list, some types are "atomic" or "simple", while others are derived from other types by combining them in different ways.

This is going to be one of our main themes: we'll systematically explore different ways to combine types and analyze the resulting set of values.

Another important theme is that in order to keep things simple we'll basically ignore the meaning of values of a given type. Values will be represented as mere featureless points in a set.

2. Simple types

First things first: how do we even create new types?

Consider the following definitions:

// `sealed` + nobody extending it in this file = no values of type T can be created.
sealed trait T

// a singleton object
object O

// an enumeration with exactly three values
enum X:
  case A, B, C

case class Point(x: Int, y: Int)

At this point we have introduced 4 new types (labels) into our program:

Point is a case class, so two values Point(1, 2) are equal: each pair (x, y) gives exactly one value.

(Here and in the rest of the article we ignore null. For every class and trait type, Scala also accepts null as a value: val t: T = null compiles. Scala 3's explicit nulls remove null from these types.)

3. Families of types: Functions in 𝕋

A trait declaration such as

trait F[A]

defines a (math) function from types to types:

We can apply this function to a type, and the result will be another, brand new type.

(In Lean, as we saw in Lean for Scala programmers, a type function is just an ordinary function of type Type → Type.)

We'll represent type functions as incomplete labels (or labels with holes). Once the missing label is provided we get a proper label.

In the diagrams, a proper type is a square and a type function is a frame with square holes. The shadows show which parts stand up and which parts are missing: a square fits exactly into a hole, and when all the holes are full we have a proper type.

Using List as an example:

// Declaration (simplified; the standard library's List is more complex):
trait List[A]

// Usage:
val l: List[Int] = ???

The top rectangle represents $\{\mathbb{T} \to \mathbb{T}\}$, the set of all (simple) type functions, of which List is a member.

To be clear: List is not a Scala function. But it is a mathematical function.

// More examples:
trait Future[A]

// Usage:
val ll: List[List[Int]] = ???
val ts: Future[String]  = ???

// Invalid:
// List[List]
// Future[List]

// A type alias:
type DoubleList[A] = List[List[A]]
// Applying a type alias does not create a new type:
// DoubleList[Int] is the same type as List[List[Int]]

In the expressions above:

• List is not a type, it needs a type argument to become a type. It is a type constructor.
• List[Int] is a brand new type.
• List[List] is invalid, because the declared argument of List has to be a proper type.

Even though List[Int] and List[String] are different types, they are clearly related (and we can expect the corresponding values to also be related somehow). Thus type functions allow us to create families of related types:

Observe that this is just the image of List.

Another example:

One difference between type functions and regular (math) functions is that a type function declared with a trait or a class just "accumulates" its arguments: there is no automatic simplification. For example:

List[Either[(Int, A), Map[Int, String]]]

(hence the need for type aliases).

A type alias, on the other hand, does reduce: DoubleList[Int] is List[List[Int]]. And Scala 3's match types compute their result, like the Length example in Lean for Scala programmers.

3.1 Functions of multiple arguments

Otherwise identical to single-argument functions, except with more than one hole.

For example, the signature of Map is:

The signature of a type function is called its kind:

• Regular types have kind Type (i.e. $\mathbb{T}$). They are also called proper types.
• Map and Function1 have kind (Type, Type) => Type (i.e. $\mathbb{T} \times \mathbb{T} \to \mathbb{T}$).

3.2 More type functions

Before continuing let's examine different expressions that give rise to type functions:

Note: The square block ∎ is not valid Scala syntax!

It's just a way to represent the fact that a type is missing at that position, and if we fill the gap, then we will have a proper type.

Scala 3 has native syntax for anonymous type functions: type lambdas. The type function Map[Int, ∎] is written [A] =>> Map[Int, A]. (In Scala 2 you need the compiler plugin kind-projector, which writes it as Map[Int, *].)

3.3 (Type) function composition

As expected, type functions can be composed.

For example, applying List and then Future gives the composition Future ∘ List:

In Scala 3 we can write it as a type lambda:

type FutureOfList = [A] =>> Future[List[A]]

3.4 Identity function

As with any set, there is an identity function in the set of types $\mathbb{T}$. This can be expressed in Scala using a type alias like so:

type Id[A] = A

3.5 High order functions

We can also describe high order type functions that receive (simpler) type functions as arguments.

// Declaration:
trait H[F[_]]
//      ▲
//      |
//  The single argument F has to be a type function 𝕋 → 𝕋

// Usage:
val listH: H[List] = ???
// Once H is applied to List, the result is a proper type!

A high order type function has a "hole" with a very specific shape: only simpler type functions can be used as arguments. Once this argument is provided the result is a proper type.

Since H takes a function and returns a proper type, it has kind $(\mathbb{T} \to \mathbb{T}) \to \mathbb{T}$.

Here's an attempt to represent this graphically:

More examples:

// The argument F has to be a one-argument type function
trait Functor[F[_]]
trait Monad[F[_]]

// The argument F has to be a two-argument type function
trait Category[F[_, _]]

// Usage:
val intFunctor: Functor[[B] =>> Int => B] = ???
val functionCategory: Category[Function1] = ???

Taking the idea further, how about a function that accepts arguments of a shape/kind like Functor?

trait N[G[_[_]]]

• N takes one argument, named G.
• The argument G is a type function; it takes one anonymous argument of shape $\mathbb{T} \to \mathbb{T}$ (i.e. a type function such as List).
• Hence the signature (kind) of G is $(\mathbb{T} \to \mathbb{T}) \to \mathbb{T}$.
• And N has signature (kind) $((\mathbb{T} \to \mathbb{T}) \to \mathbb{T}) \to \mathbb{T}$.

// valid:
val nFunctor: N[Functor] = ???
val nMonad: N[Monad] = ???

// invalid, not the right shape:
// N[List]
// N[Int]

Graphically:

4. Subtypes and Sets

In Scala 3 the set of types $\mathbb{T}$ has the structure of a lattice under subtyping:

Every two types have a least upper bound, their union A | B, and a greatest lower bound, their intersection A & B (see section 5). Strictly speaking, this is true if we treat equivalent types, such as a type and its alias, as one type. In Scala 2, which has no union types, two types don't always have a least upper bound.

The above diagram of $\mathbb{T}$ does not show all subtype arrows; it only shows the "direct" or "minimal" arrows. But since subtyping is a transitive relation, if A <: B and B <: C then A <: C. (Matchable is new in Scala 3; it is related to pattern matching.)

Using our mapping $V$ between types and sets of values we get an analogous structure on $\mathcal{P}(\mathbb{V})$:

To A <: B we can associate the inclusion function $i: V(A) \hookrightarrow V(B)$ between the corresponding sets of values.

5. Set related operations

The correspondence between subtyping and subsets mentioned above naturally leads us to consider what other operations on types we can do based on operations on the corresponding sets of values.

Let's start by creating a little dictionary between sets and types.

5.1 Union of two types

The union of types A and B is the type A | B defined as

i.e. its values are the union of the values of A and B.

Properties:

• | is commutative and associative.
• A is a subtype of A | B (and similar for B)
• If A <: C and B <: C then A | B <: C

5.2 Intersection of two types

The intersection of types A and B is the type A & B defined as

i.e. its values are the intersection of the values of A and B.

Properties:

• If A <: X then A & B <: X
• If B <: X then A & B <: X
• In particular A & B <: A and A & B <: B
• If T <: A and T <: B then T <: A & B

which are rather natural if we think of their effect on the corresponding sets of values.

Intersection of types is defined in a structural way in the sense that values of A & B must have all the properties (members) of A and all the members of B.

Note: In Scala 2 the keyword with can be used for similar purposes. The main difference is that it is not commutative.

6. Subtypes and type functions

Let's discuss now the interaction between subtypes and type functions.

6.1 Domain and image of type functions

The domain of a type function F is the set of all types A ∈ 𝕋 for which F[A] is defined. The image of F is the set of all types of the form F[A] for some A.

In the examples we've seen so far our functions (such as List or Future) have been defined for all types, making the domain the whole set of types $\mathbb{T}$.

On the other hand, the image of List is a proper subset of $\mathbb{T}$:

What if we want to restrict the domain of a type function to be not the whole $\mathbb{T}$ but rather just a proper subset of it?

There are different ways to accomplish this, as we'll see in the following sections.

6.2 The set of subtypes of a given set

The simplest way to come up with a proper subset of types (and corresponding values) is to use subtyping.

Consider the set Sub(A) in $\mathbb{T}$ of all the subtypes of a given type A:

(This is sometimes described as $\downarrow A$.)

For example, given

trait Pet
class Fish extends Pet
class Dog  extends Pet

then Sub(Pet) contains Pet, Fish, Dog, Null and Nothing, but also types such as Fish & Dog or Pet & Serializable. In fact, it is infinite.

Graphically:

Analogously for supertypes.

6.3 Type constraint: Invariant type functions

Consider this definition:

trait F[A <: X]

F is a type function whose argument A is now restricted to be a subtype of X. In other words

(If X happens to be Any then we're back to the "no restrictions" case).

F as defined does not preserve the subtyping relationship: F[A] <: F[B] only when A and B are the same type, so the elements of its image have no subtyping relationship amongst each other.

6.4 Type constraint: Covariant type functions

If we add the + annotation then we're declaring that subtype relationships (arrows) will be carried over to the image of F:

trait F[+A <: X]

6.5 Type constraint: Contravariant type functions

The annotation - will reverse the subtype arrows:

trait F[-A <: X]

Note: Variance annotations +, - cannot be applied to an arbitrary function F[_]. They are only allowed on type functions whose implementation satisfies the variance rules (more information).

Subtyping gives an easy way to create sets of types and sets of values. The downside is that it's not very flexible, in the sense that we cannot add pre-existing types to a given hierarchy (i.e. we cannot retroactively make one type extend another).

The Type Class pattern provides a way to overcome that limitation. Before examining it we need to talk briefly about givens.

7. Givens

The given mechanism (called implicits in Scala 2) allows us to mark a value of a given type (say a: A) and elsewhere in our code summon this value (i.e. retrieve it, get a reference to it) by referring to the type A.

In practice this amounts to having a compile time function from types to values, called summon in Scala 3 (implicitly in Scala 2):

For example:

import scala.concurrent.ExecutionContext

given ec: ExecutionContext = ExecutionContext.global

// later:
summon[ExecutionContext] == ec

Given that in general there can be many values of a given type, in order for this mechanism to work: 1) the specific value a has to be selected beforehand by marking it as a given, and 2) where we summon it, exactly one given must be the best candidate. (If two givens are equally good candidates, the compiler reports an ambiguity.)

Another interesting aspect of this function is that even though its codomain is the whole set of values $\mathbb{V}$, the result is not arbitrary: it is always a value of the given type. In other words, summon is a dependent function: the type of its result depends on its argument. (Dependent functions are the topic of Lean for Scala programmers, Part 3.)

8. Type Classes

Quoting Scala with Cats:

A type class is an interface or API that represents some functionality we want to implement.

… [It] is represented by a trait with at least one type parameter.

It has three ingredients:

1) A Type Function: capture all the desired properties of a type A in a trait parameterized by A.

Example: Monoid

trait Monoid[A]:
  def empty: A
  def combine(a: A, b: A): A

// Monoid laws, for all a, b, c: A
// 1. Associativity:    combine(combine(a, b), c) == combine(a, combine(b, c))
// 2. Identity element: combine(empty, a) == a and combine(a, empty) == a
def monoidLaws[A](a: A, b: A, c: A)(using M: Monoid[A]): Boolean =
  M.combine(M.combine(a, b), c) == M.combine(a, M.combine(b, c)) &&
  M.combine(M.empty, a) == a &&
  M.combine(a, M.empty) == a

A property-based testing library such as ScalaCheck can check monoidLaws for many random values.

2) Instances: Make a given type a member of the type class by creating lawful given instances for required types:

given intMonoid: Monoid[Int] with
  def empty = 0
  def combine(a: Int, b: Int) = a + b

given stringMonoid: Monoid[String] with
  def empty = ""
  def combine(a: String, b: String) = a + b

// make sure each instance actually passes the Monoid laws!

"Make a given type a member" is not something that has a native construct in Scala. Instead, it is understood in the following sense:

We're going to overload the word Monoid to refer to the set of types for which a lawful given instance of Monoid[A] exists! (see diagram below).

"Lawful" means that our instance actually passes the tests asserting the Monoid laws.

So given the definitions above we can say that "Int is a Monoid", because there is a given instance of Monoid[Int] in scope.

Consider the following function (and diagram below):

(for example theMonoid[Int] == intMonoid)

• theMonoid maps a type A into a single value: the given instance for Monoid[A].
• theMonoid is only defined for types with a given instance of Monoid. Otherwise you get a compilation error.

This means that the "Monoid" type class is just the domain of theMonoid.

Note: Even though the type function Monoid can be applied to any type A (hence the domain is all of $\mathbb{T}$), we can't necessarily create a lawful instance for every such A.

For example, Monoid[Char] is a valid type, but as long as there is no lawful given instance of it in our code then we don't consider it to be a member of the "Monoid" Type Class.

3) Client code: program against this trait whenever the functionality is desired:

def combineAll[A](as: List[A])(using M: Monoid[A]): A =
  as.foldLeft(M.empty)(M.combine)

// usage:
combineAll(List(1, 2, 3)) == 6
combineAll(List("hello", " ", "world!")) == "hello world!"

combineAll is actually a family of functions (one for each type A):

We can see that if no instance of Monoid[X] (for a particular X) exists, then there's no way we can use combineAll[X].

Type classes give us the ultimate flexibility to define subsets of types with desired properties, since we can "add" members one by one as we did above.