Reading Types (in progress!!)

This post is about reading type signatures. It assumes you’ve never written Haskell (or a similar language) before. If you’ve written in such a language before, it’s likely this material will be familiar to you. This post is not for you.

It doesn’t assume you’ve used a typed programming language before. I’ll define things carefully and take care with jargon. I’ll give priority to concrete examples, so that you can use this to build things. It’s important to me that this can be a post you can come back to if you want to get more comfortable with typed programming and have the time and energy for it.

Types and type systems are powerful tools, and I want to make them a little easier to use. They’re great for communication, for expression, for correctness, for program maintenance, and peformance. The problem is, how do we use them well?

All examples will be given using the Haskell programming language. It’s pretty easy to install nowadays, and the syntax is pretty clean for talking about type system things.

What are types?

Types are, a lot of things. If I were to give an overarching definition, they’re at the very least, a way to describe the shapes of data and programs.

There’s a lot of context, often times left unsaid when folks talk about “types”, unqualified.

Some people talk about types and think of storage types. These describe how much space certain pieces of program take up in memory, and possibly, how that data is interpreted. Think: integers, longs, unsigned integers, floats, arrays, C.

Some people talk about types, and object-oriented design comes to mind. These sorts of types are one system for classifying data that mixes state, scope, and behavior together, and talks about types in terms of hierarchies of capabilities. These are known as sub-type systems. Think: Java, C Sharp, classes. This post is not about these systems.

Others still, talk about functional programming, and algebraic types, and a bunch of other things, sometimes of a very mathematical nature. There’s talk of how to compose things, how functions interact, and about side-effects and types to describe them. Think: Haskell, Elm, monads, and the like. This post is about these sorts of type systems, and how to understand and think about them. Let’s call them, algebraic data types.

Further still, some folks talk about types for proving whole programs adhere to specs. At this point, we’ve wandered into dependent types, provers, and type theory. While these systems can be extremely expressive, they’re outside the scope of this post. We’re starting small, to be able to read and make sense of things we can use right now.

There’s also the distinction between dynamic and static types. When I talk about dynamic type systems here, I’m talking about Python, Ruby, Racket, Javascript, Erlang, and others like them, who check the types of data at run-time. Some are more strict than others. Static type systems run all their checks at compile time, before a program is ever run. That’s what languages like Java, C, C++, Rust, Haskell, and OCaml do. Like the dynamic case, there’s sharp differences about what sorts of things each of these languages can check, some strictly more expressive than others.

Speaking of expressivity - I use this term in a strict sense, which I’ll make more clear with the rest of this post, this post about reading and understanding types. An expressive type system is one that let’s you say more about your data, without much hassle. These are the best sorts of type systems for communicating intent about your programs and data.

That’s “types”. “Types”, as it turns out, can mean a lot of different things to different people.

Type signatures: what can it do?

Given all the definitions up to this point, let’s talk about something more concrete: type signatures.

A type signature is a description of a function:

A lot of information can be packed into a small space. Type signatures are the first place to look to try to understand a function.

Type signatures are the main thing we’ll be working to understand how to read.

Here’s a type signature now:

add :: Int -> Int -> Int

add is a function that takes two Int arguments and returns an Int. More generally:

  someFunction ::  -- function name
    a -> b -> c    -- function parameters/arguments
    -> d           -- return type

Of course, different languages have different ways of expressing types signatures. Here’s add in C:

int add(int x, int y);

Here’s add in Scala:

def add(x: Int, y: Int): Int

We’ll look at far more interesting type signatures later as we build on what we know.

Simple and primitive types

Primitive types are those provided by a language that are closest to what might be stored on a machine. Things like:

In Haskell, these types are:

Function types: passing around functions

There are also types that can express functions, specifically, functions as arguments to other functions.

Let’s look at an example:

addAndShow :: Int -> Int -> (Int -> String) -> String
showInt :: Int -> String

This is almost add, but with more power. It now takes a function paramter that let’s us turn an integer into a string. Looking immediately below, we have such a function handy. Let’s go even more concrete for a moment. Here’s the definition of addAndShow:

addAndShow x y showFn = showFn (x + y)

That’s all there is to that one. Below, I’ll show what a definition of showInt might look like. A few notes before I get to it:

With that said, for the curious:

showInt :: Int -> String
showInt n =
    let n' = abs n in
    let ret = go (n' `div` 10) (n' `mod` 10) [] in
    if n < 0 then '-' : ret else ret

  where go :: Int -> Int -> String -> String
        go leftDigits rightDigit acc
          | leftDigits == 0 && rightDigit == 0 = acc
          | otherwise = go (leftDigits `div` 10) (leftDigits `mod` 10) (toChar rightDigit : acc)

        toChar :: Int -> Char
        toChar x = case x of
          0 -> '0'
          1 -> '1'
          2 -> '2'
          3 -> '3'
          4 -> '4'
          5 -> '5'
          6 -> '6'
          7 -> '7'
          8 -> '8'
          9 -> '9'
          _ -> error "out of bounds - toChar, Int not between 0 - 9"

It is important to note also that at this point, we don’t have enough tools to give really precise types. Notably, let’s look at another function that fits (Int -> String), but doesn’t do what we’d hope:

showInt2 :: Int -> String
showInt2 _ = "2"

This definition does satisfy the given type signature. Sure. But! This warning is here specifically to emphasize the limits of what we can express at this point. We know that:

Reading type signatures and designing types is every bit as much about what functions can do as it is about what functions cannot do. Keep this in mind as we proceed.

Let’s expand what we can express with types in the next section.

Product types: records, structs, and more

Sum types: tagged variants, enumerations, and more

Composing types: sums and products together

Type inference: the compiler can work with you

Polymorphism: types for more general functions

An example: types for optional data

Another example: types for tracking success and failure

ADTs: abstract and algebraic

Recursive types

Another kind of polymorphism: traits and typeclasses

Types for tracking effects

Types of a higher kind, or, type signatures for types

Writing types to be read - communicating effectively

Where to next?