A common red herring in the type debate.

I regularly get involved in debates about static versus dynamic typing. This post isn't an attempt to persuade anyone that static types are better. One of the reasons that I so often find myself debating this topic is that it intrigues me. I get the impression that most of the software luminaries that I admire (e.g. Kent Beck, Robert C. Martin, Michael Feathers) seem to favour dynamically typed languages. What is it that smart people have figured out that I haven't?

The debate continues, and this article isn't going to stop it. It may, perhaps, put one misconception to rest. There are still good arguments on either side. It's not my goal to dispute any of the good arguments. It's my goal to counter a common bad argument.

Misconception: static typing as numbers on steroids #

I get the impression that many people think about static types as something that has to do with strings and numbers - particularly numbers. Introductions to programming languages often introduce strings first. That's natural, since the most common first example is Hello, world!. After that usually follows an introduction to basic arithmetic, and that often includes an explanation about types of numbers - at least the distinction between integers and floating-point numbers. At the time I'm writing this, the online C# tutorial is a typical example of this. Real World Haskell takes the same approach to introducing types.

It's a natural enough way to introduce static types, but it seems to leave some learners with the impression that static types are mostly useful to prevent them from calling a method with a floating-point number when an integer was expected. That's the vibe I'm getting from this article by Robert C. Martin.

When presented with the notion of a 'stronger' type system, people with that mindset seem to extrapolate what they already know about static types.

Three boxes, from left to right: no types, static primitive types, and static primitive types on steroids.

If you mostly think of static types as a way to distinguish between various primitive types (such as strings and a zoo of number types), I can't blame you for extrapolating that notion. This seems to happen often, and it leads to a lot of frustration.

People who want 'stronger numbers' try to:

  • Model natural numbers; i.e. to define a type that represents only positive integers
  • Model positive numbers; i.e. rational or real numbers greater than zero
  • Model non-negative numbers
  • Model numbers in a particular range; e.g. between 0 and 100
  • Model money in different currencies
Particularly, people run into all sorts of trouble when they try to accomplish such goals with Haskell. They've heard that Haskell has a powerful type system, and now they want to do those things.

Haskell does have a powerful type system, but it's a type system that builds on the concept of algebraic data types. (If you want to escape the jargon of that Wikipedia article, I recommend Tomas Petricek's lucid and straightforward explanation Power of mathematics: Reasoning about functional types.)

There are type systems that enable you to take the notion of numbers to the next level. This is called either refinement types or dependent types, contingent on what exactly it is that you want to do. Haskell doesn't support that out of the box. The most prominent dependently-typed programming language is probably Idris, which is still a research language. As far as I know, there's no 'production strength' languages that support refinement or dependent types, unless you consider Liquid Haskell to fit that description. Honestly, all this is at the fringe of my expertise.

I'll return to an example of this kind of frustration later, and also suggest a simple alternative. Before I do that, though, I'd like to outline what it is proponents of 'strong' type systems mean.

Make illegal states unrepresentable #

Languages like Haskell, OCaml, and F# have algebraic type systems. They still distinguish between various primitive types, but they take the notion of static types in a completely different direction. They introduce a new dimension of static type safety, so to speak.

Three boxes. At the bottom left: no types. To the right of that: static primitive types. To the top of the no-types box: algebraic data types

It's a completely different way to think about static types. The advantage isn't that it prevents you from using a floating point where an integer was required. The advantage is that it enables you to model domain logic in a way that flushes out all sorts of edge cases at compile time.

I've previously described a real-world example of domain modelling with types, so I'm not going to repeat that effort here. Most business processes can be described as a progression of states. With algebraic data types, not only can you model what a valid state looks like - you can also model the state machine in such a way that you can't represent illegal states.

This notion is eloquently captured by the aphorism:

Make illegal states unrepresentable.

This is solving an entirely different type of problem than distinguishing between 32-bit and 64-bit integers. Writing even moderately complex code involves dealing with many edge cases. In most mainstream languages (including C# and Java), it's your responsibility to ensure that you've handled all edge cases. It's easy to overlook or forget a few of those. With algebraic data types, the compiler keeps track of that for you. That's a tremendous boon because it enables you to forget about those technical details and instead focus on adding value.

Scott Wlaschin wrote an entire book about domain modelling with algebraic data types. That's what we talk about when we talk about stronger type systems. Not 'numbers on steroids'.

Exhibit: summing notionals #

I consider this notion of strong type systems viewed as numbers on steroids a red herring. I don't blame anyone from extrapolating from what they already know. That's a natural way to try to make sense of the world. We all do it.

I came across a recent example of this way of thinking in a great article by Alex Nixon titled Static types are dangerously interesting. The following is in no way meant to excoriate Alex or his article, but I think it's a great example of how easily one can be lead astray by thinking that strong type systems imply numbers on steroids.

You should read the article. It's well-written and uses more sophisticated features of Haskell than I'm comfortable with. The example problem it tries to solve is basically this: Given a set of trades, calculate the total notional in each currency. Consider a collection of trades:

Quantity, Ticker, Price, Currency
100,      VOD.L,  1,     GBP
200,      VOD.L,  2,     GBP
300,      AAPL.O, 3,     USD
50,       4151.T, 5,     JPY

I'll let Alex explain what it is that he wants to do:

"I want to write a function which calculates the total notional in each currency. The word notional is a fancy way of saying price * quantity. Think of it as "value of the thing that changed hands".

"For illustration, the function signature might look something like this:

"sumNotionals :: [Trade] -> Map Currency Rational

"In English, it’s a function that takes a list of trades and returns a map from currency to quantity."

If given the above trades, the output would be:

Currency, Notional
GBP,      500
USD,      900
JPY,      250

The article proceeds to explore how to model this problem with Haskell's strong type system. Alex wants to be able to calculate with money, but on the other hand, he wants the type system to prevent accidents. You can't add 100 GBP to 300 USD. The type system should prevent that.

Early on, he defines a sum type to model currencies:

data Currency
  = USD
  | GBP
  | JPY
  deriving (EqOrdShow)

Things basically go downhill from there. Read the article; it's good.

Sum types should distinguish behaviour, not values #

I doubt that Alex Nixon views his proposed Currency type as anything but a proof of concept. In a 'real' code base, you'd enumerate all the currencies you'd trade, right?

I wouldn't. This is the red herring in action. Algebraic data types are useful because they enable us to distinguish between cases that we should treat differently, by writing specific code that deals with each case. That's not the case with a currency. You add US dollars together in exactly the same way that you add euros together. The currency doesn't change the behaviour of that operation.

But we can't just enable addition of arbitrary monetary values, right? After all, we shouldn't be able to add 20 USD and 300 DKK. At least, without an exchange rate, that shouldn't compile.

Let's imagine, for the sake of argument, that we encode all the currencies we trade into a type. What happens if our traders decide to trade a currency that they haven't previously traded? What if a country decides to reset their currency? What if a country splits into two countries, each with their own currency?

If you model currency as a type, you'd have to edit and recompile your code every time such an external event occurs. I don't think this is a good use of a type system.

Types should, I think, help us programmers identify the parts of our code bases where we need to treat various cases differently. They shouldn't be used to distinguish run-time values. Types provide value at compile time; run-time values only exist at run time. To paraphrase Kent Beck, keep things together that change together; keep things apart that don't.

I'd model currency as a run-time value, because the behaviour of money doesn't vary with the currency.

Boring Haskell #

How would I calculate the notionals, then? With boring Haskell. Really boring Haskell, in fact. I'm only going to need two imports and no language pragmas:

module Trades where
 
import Data.List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

Which types do I need? For this particular purpose, I think I'll just stick with a single Trade type:

data Trade = Trade {
    tradeQuantity :: Int
  , tradeTicker :: String
  , tradePrice :: Rational
  , tradeCurrency :: String }
  deriving (EqShow)

Shouldn't I introduce a Money type? I could, but I don't have to. As Alexis King so clearly explains, you don't have to model more than you need to do the job.

By not introducing a Money type and making it an instance of various type classes, I still prevent client code from adding things together that shouldn't be added together. You can't add Trade values together because Trade isn't a Num instance.

How do we calculate the notionals, then? It's easy; it's a one-liner:

sumNotionals :: Foldable t => t Trade -> Map String Rational
sumNotionals = foldl' (\m t -> Map.insertWith (+) (key t) (value t) m) Map.empty
  where key   (Trade _ _ _ currency) = currency
        value (Trade quantity _ price _) = toRational quantity * price

Okay, that looks more like four lines of code, but the first is an optional type declaration, so it doesn't count. The key and value functions could be inlined to make the function a single (wide) line of code, but I made them two named functions in order to make the code more readable.

It gets the job done:

*Trades> sumNotionals trades
fromList [("GBP",500 % 1),("JPY",250 % 1),("USD",900 % 1)]

While this code addresses this particular problem, you probably consider it cheating because I've failed to address a wider concern. How does one model money in several currencies? I've previously covered that, including a simple Haskell example, but in general, I consider it more productive to have a problem and then go looking for a solution, rather than inventing a solution and go looking for a problem.

Summary #

When people enter into a debate, they use the knowledge they have. This is also the case in the debate about static versus dynamic types. Most programmers have experience with statically typed languages like C# or Java. It's natural to argue from what you know, and extrapolate from that.

I think that when confronted with a phrase like a more powerful type system, many people extrapolate and think that they know what that means. They think that it means statically typed numbers on steroids. That's a red herring.

That's usually not what we mean when we talk about more powerful type systems. We talk about algebraic data types, which make illegal states unrepresentable. Judged by the debates I've participated in, you can't extrapolate from mainstream type systems to algebraic data types. If you haven't tried programming with both sum and product types, you aren't going to grok what we mean when we talk about strong type systems.


Comments

"but in general, I consider it more productive to have a problem and then go looking for a solution, rather than inventing a solution and go looking for a problem."

This really resonates with me. I've been observing this in my current team and the tendency to "lookout" for the solutions to problems not yet present, just for the sake of "making it a robust solution" so to say.

I really like the properties of the Haskell solution. It handles all the currencies (no matter how many of them come in the dataset) without explicitly specifying them. And you can't accidentally add two different currencies together. The last part would be pretty verbose to implement in C#.

2020-01-20 20:54 UTC

I'm not sure the above is a good example of what you're trying to say about algebraic data types. The problem can be solve identically (at least semantically) in C#. Granted, the definition of the Trade type would be way more verbose, but once you have that, the SumNotionals method is basically the same as you code, albeit with different syntax:

Dictionary<string, int> SumNotionals(IEnumerable<Trade> trades)
{
    return trades
        .GroupBy(t => t.Currency, t => t.Price * t.Quantity)
        .ToDictionary(g => g.Key, g => g.Sum());
}

Am I missing something?

2020-01-20 22:30 UTC

You are right Andrew. The LINQ query indeed has the same properites as the Haskell function.

I'm not sure what I was thinking yesterday, but I think I subconsciously "wanted" C# to be less robust.

2020-01-21 18:04 UTC

Andrew, thank you for writing. I didn't intend to say much about algebraic data types in this article. It wasn't the topic I had in mind. It can be difficult to communicate any but the simplest ideas, so it's possible that I didn't state my intention well enough. If so, the fault is mine. I've tried to demonstrate the power of algebraic data types before, so I didn't want to repeat the effort, since my agenda was another. That's why I linked to that other article.

The reason I discussed Alex Nixon's blog post was that it was the article that originally inspired me to write this article. I always try to include an example so that the reader gets to see the connection between the general concept and specifics.

I could have discussed Alex' article solely on its merits of showcasing failed attempts to model a 'stronger number'. That would, however, have left the reader without a resolution. I found that a bad way to structure my text. Readers would be left with questions. Okay Mark, that's all fine, but then how would you solve the problem?

So I decided to include a simple solution in an attempt to cut the Gordian know, so to speak.

2020-01-22 14:11 UTC

Mark, thanks for your response. It does indeed clear up my confusion. In my eagerness to learn more about algrebraic data types I read the second half of your post the wrong way. Thanks for clearing it up.

2020-01-22 21:30 UTC


Wish to comment?

You can add a comment to this post by sending me a pull request. Alternatively, you can discuss this post on Twitter or somewhere else with a permalink. Ping me with the link, and I may respond.

Published

Monday, 20 January 2020 07:39:00 UTC

Tags



"Our team wholeheartedly endorses Mark. His expert service provides tremendous value."
Hire me!
Published: Monday, 20 January 2020 07:39:00 UTC