Types + Properties = Software: designing with types by Mark Seemann
Design types so that illegal states are unrepresentable.
This article is the first in a series of articles that demonstrate how to develop software using types and properties. In this article, you'll see an example of how to design with algebraic data types, and in future articles, you'll see how to specify properties that must hold for the system. This example uses F#, but you can design similar types in Haskell.
The source code for this article series is available on GitHub.
Tennis #
The example used in this series of articles is the Tennis Kata. Although a tennis match consists of multiple sets that again are played as several games, in the kata, you only have to implement the scoring system for a single game:
- Each player can have either of these points in one game: Love, 15, 30, 40.
- If you have 40 and you win the ball, you win the game. There are, however, special rules.
- If both have 40, the players are deuce.
- If the game is in deuce, the winner of a ball will have advantage and game ball.
- If the player with advantage wins the ball, (s)he wins the game.
- If the player without advantage wins, they are back at deuce.
You can take on this problem in many different ways, but in this article, you'll see how F#'s type system can be used to make illegal states unrepresentable. Perhaps you think this is overkill for such a simple problem, but think of the Tennis Kata as a stand-in for a more complex domain problem.
Players #
In tennis, there are two players, which we can easily model with a discriminated union:
type Player = PlayerOne | PlayerTwo
When designing with types, I often experiment with values in FSI (the F# REPL) to figure out if they make sense. For such a simple type as Player, that's not strictly necessary, but I'll show you anyway, take illustrate the point:
> PlayerOne;; val it : Player = PlayerOne > PlayerTwo;; val it : Player = PlayerTwo > PlayerZero;; PlayerZero;; ^^^^^^^^^^ error FS0039: The value or constructor 'PlayerZero' is not defined > PlayerThree;; PlayerThree;; ^^^^^^^^^^^ error FS0039: The value or constructor 'PlayerThree' is not defined
As you can see, both PlayerOne and PlayerTwo are values inferred to be of the type Player, whereas both PlayerZero and PlayerThree are illegal expressions.
Not only is it possible to represent all valid values, but illegal values are unrepresentable. Success.
Naive point attempt with a type alias #
If you're unfamiliar with designing with types, you may briefly consider using a type alias to model players' points:
type Point = int
This easily enables you to model some of the legal point values:
> let p : Point = 15;; val p : Point = 15 > let p : Point = 30;; val p : Point = 30
It looks good so far, but how do you model love? It's not really an integer.
Still, both players start with love, so it's intuitive to try to model love as 0:
> let p : Point = 0;; val p : Point = 0
It's a hack, but it works.
Are illegal values unrepresentable? Hardly:
> let p : Point = 42;; val p : Point = 42 > let p : Point = -1337;; val p : Point = -1337
With a type alias, it's possible to assign every value that the 'real' type supports. For a 32-bit integer, this means that we have four legal representations (0, 15, 30, 40), and 4,294,967,291 illegal representations of a tennis point. Clearly this doesn't meet the goal of making illegal states unrepresentable.
Second point attempt with a discriminated Union #
If you think about the problem for a while, you're likely to come to the realisation that love, 15, 30, and 40 aren't numbers, but rather labels. No arithmetic is performed on them. It's easy to constrain the domain of points with a discriminated union:
type Point = Love | Fifteen | Thirty | Forty
You can play around with values of this Point type in FSI if you will, but there should be no surprises.
A Point value isn't a score, though. A score is a representation of a state in the game, with (amongh other options) a point to each player. You can model this with a record:
type PointsData = { PlayerOnePoint : Point; PlayerTwoPoint : Point }
You can experiment with this type in FSI, like you can with the other types:
> { PlayerOnePoint = Love; PlayerTwoPoint = Love };;
val it : PointsData = {PlayerOnePoint = Love;
PlayerTwoPoint = Love;}
> { PlayerOnePoint = Love; PlayerTwoPoint = Thirty };;
val it : PointsData = {PlayerOnePoint = Love;
PlayerTwoPoint = Thirty;}
> { PlayerOnePoint = Thirty; PlayerTwoPoint = Forty };;
val it : PointsData = {PlayerOnePoint = Thirty;
PlayerTwoPoint = Forty;}
That looks promising. What happens if players are evenly matched?
> { PlayerOnePoint = Forty; PlayerTwoPoint = Forty };;
val it : PointsData = {PlayerOnePoint = Forty;
PlayerTwoPoint = Forty;}
That works as well, but it shouldn't!
Forty-forty isn't a valid tennis score; it's called deuce.
Does it matter? you may ask. Couldn't we 'just' say that forty-forty 'means' deuce and get on with it?
You could. You should try. I've tried doing this (I've done the Tennis Kata several times, in various languages), and it turns out that it's possible, but it makes the code more complicated. One of the reasons is that deuce is more than a synonym for forty-forty. The score can also be deuce after advantage to one of the players. You can, for example, have a score progression like this:
- ...
- Forty-thirty
- Deuce
- Advantage to player one
- Deuce
- Advantage to player two
- Deuce
- ...
Additionally, if you're into Domain-Driven Design, you prefer using the ubiquitous language of the domain. When the tennis domain language says that it's not called forty-forty, but deuce, the code should reflect that.
Final attempt at a point type #
Fortunately, you don't have to throw away everything you've done so far. The love-love, fifteen-love, etc. values that you can represent with the above PointsData type are all valid. Only when you approach the boundary value of forty do problems appear.
A solution is to remove the offending Forty case from Point. The updated definition of Point is this:
type Point = Love | Fifteen | Thirty
You can still represent the 'early' scores using PointsData:
> { PlayerOnePoint = Love; PlayerTwoPoint = Love };;
val it : PointsData = {PlayerOnePoint = Love;
PlayerTwoPoint = Love;}
> { PlayerOnePoint = Love; PlayerTwoPoint = Thirty };;
val it : PointsData = {PlayerOnePoint = Love;
PlayerTwoPoint = Thirty;}
Additionally, the illegal forty-forty state is now unrepresentable:
> { PlayerOnePoint = Forty; PlayerTwoPoint = Forty };;
{ PlayerOnePoint = Forty; PlayerTwoPoint = Forty };;
-------------------^^^^^
error FS0039: The value or constructor 'Forty' is not defined
This is much better, apart from the elephant in the room: you also lost the ability to model valid states where only one of the players have forty points:
> { PlayerOnePoint = Thirty; PlayerTwoPoint = Forty };;
{ PlayerOnePoint = Thirty; PlayerTwoPoint = Forty };;
--------------------------------------------^^^^^
error FS0039: The value or constructor 'Forty' is not defined
Did we just throw the baby out with the bathwater?
Not really, because we weren't close to being done anyway. While we were making progress on modelling the score as a pair of Point values, remaining work includes modelling deuce, advantage and winning the game.
Life begins at forty #
At this point, it may be helpful to recap what we have:
type Player = PlayerOne | PlayerTwo type Point = Love | Fifteen | Thirty type PointsData = { PlayerOnePoint : Point; PlayerTwoPoint : Point }
While this enables you to keep track of the score when both players have less than forty points, the following phases of a game still remain:
- One of the players have forty points.
- Deuce.
- Advantage to one of the players.
- One of the players won the game.
type FortyData = { Player : Player; OtherPlayerPoint : Point }
This is a record that specifically keeps track of the situation where one of the players have forty points. The Player element keeps track of which player has forty points, and the OtherPlayerPoint element keeps track of the other player's score. For instance, this value indicates that PlayerTwo has forty points, and PlayerOne has thirty:
> { Player = PlayerTwo; OtherPlayerPoint = Thirty };;
val it : FortyData = {Player = PlayerTwo;
OtherPlayerPoint = Thirty;}
This is a legal score. Other values of this type exist, but none of them are illegal.
Score #
Now you have two distinct types, PointsData and FortyData, that keep track of the score at two different phases of a tennis game. You still need to model the remaining three phases, and somehow turn all of these into a single type. This is an undertaking that can be surprisingly complicated in C# or Java, but is trivial to do with a discriminated union:
type Score = | Points of PointsData | Forty of FortyData | Deuce | Advantage of Player | Game of Player
This Score type states that a score is a value in one of these five cases. As an example, the game starts with both players at (not necessarily in) love:
> Points { PlayerOnePoint = Love; PlayerTwoPoint = Love };;
val it : Score = Points {PlayerOnePoint = Love;
PlayerTwoPoint = Love;}
If, for example, PlayerOne has forty points, and PlayerTwo has thirty points, you can create this value:
> Forty { Player = PlayerOne; OtherPlayerPoint = Thirty };;
val it : Score = Forty {Player = PlayerOne;
OtherPlayerPoint = Thirty;}
Notice how both values are of the same type (Score), even though they don't share the same data structure. Other example of valid values are:
> Deuce;; val it : Score = Deuce > Advantage PlayerTwo;; val it : Score = Advantage PlayerTwo > Game PlayerOne;; val it : Score = Game PlayerOne
This model of the tennis score system enables you to express all legal values, while making illegal states unrepresentable.
It's impossible to express that the score is seven-eleven:
> Points { PlayerOnePoint = Seven; PlayerTwoPoint = Eleven };;
Points { PlayerOnePoint = Seven; PlayerTwoPoint = Eleven };;
--------------------------^^^^^
error FS0039: The value or constructor 'Seven' is not defined
It's impossible to state that the score is fifteen-thirty-fifteen:
> Points { PlayerOnePoint = Fifteen; PlayerTwoPoint = Thirty; PlayerThreePoint = Fifteen };;
Points { PlayerOnePoint = Fifteen; PlayerTwoPoint = Thirty; PlayerThreePoint = Fifteen };;
------------------------------------------------------------^^^^^^^^^^^^^^^^
error FS1129: The type 'PointsData' does not contain a field 'PlayerThreePoint'
It's impossible to express that both players have forty points:
> Points { PlayerOnePoint = Forty; PlayerTwoPoint = Forty };;
Points { PlayerOnePoint = Forty; PlayerTwoPoint = Forty };;
--------------------------^^^^^
error FS0001: This expression was expected to have type
Point
but here has type
FortyData -> Score
> Forty { Player = PlayerOne; OtherPlayerPoint = Forty };;
Forty { Player = PlayerOne; OtherPlayerPoint = Forty };;
-----------------------------------------------^^^^^
error FS0001: This expression was expected to have type
Point
but here has type
FortyData -> Score
In the above example, I even attempted to express forty-forty in two different ways, but none of them work.
Summary #
You now have a model of the domain that enables you to express valid values, but that makes illegal states unrepresentable. This is half the battle won, without any moving parts. These types govern what can be stated in the domain, but they don't provide any rules for how values can transition from one state to another.
This is a task you can take on with Property-Based Testing. Since all values of these types are valid, it's easy to express the properties of a tennis game score. In the next article, you'll see how to start that work.
If you're interested in learning more about designing with types, you can watch my Type-Driven Development with F# Pluralsight course.
