When writing code in a statically typed language sometimes types are considered as orthogonal to the logic of the code. We write them to appease the compiler, or get performance or intellisense & navigation, but all of these has no relation to the code itself.


This is wrong.


According to the Curry-Howard Correspondance, types can be interpreted as logical statements. For example, consider an application dealing with people. Our most basic entity might be (I'm using Scala here):


case class Person(name: String)

What this means is there's a logical implication Person => String. This literally means "A person has a string". Which is silly. What we want is to encode "A person has a name":

case class Name(s: String)
case class Person(name: Name)


(In Scala we can go further: We don't have to box the string inside a Name class. Instead, we can define an empty trait Named, and a type alias Name for 'String with Named'. See Eric Torreborre's excellent post on this subject)


Now methods that are supposed to work with names, accept an argument of type Name, instead of String. These methods encode further logic. Our application might have a registry of all people:

trait Registry {
  def getPerson(name: Name): Person


This encoding means that given a Registry and  a Name, we have a Person. If this is not true all the time (maybe some people are not registered), then we can encode:

trait Registry {
  def getPerson(name: Name): Option[Person]


Which means that given a Registry and a Name we can either get a Person or None.


About untyped languages



In untyped languages such as Ruby or Python, we can't encode these logical assertions. When the code base is small, and there are few members of the team, this is manageable, since peopl keep these assertions in their heads. Once the code base starts to grow, it becomes more and more difficult to keep track.


Some suggest that test-driven-development solves this: if all tests pass, and code coverage is 100%, then the code is sound. I have 2 problems with this:

  1. Getting at 100% code coverage is hard. And after you do, it means refactoring is hard since it means rewriting (manually) a lot of tests
  2. Code coverage is not enough. Some logical issues are "between the lines" of the code

About the second point, lets consider this untyped pseudo code:


def factorial(n) = {
  if (n == 1) 1
  else n * factorial(n - 1)


It is trivial to write a test that obtains 100% code coverage for this method. But this method is not correct. It does not work for negative numbers.


Here is the typed version:

def factorial(n: Int) = {
  if (n == 1) 1
  else n * factorial(n - 1)


Well, this version fails for negative numbers. But there is a clear destinction here: because of the type, we can have automatic test generation, such as ScalaCheck (or see Java alternatives). These tools will test the code with a range of integers including negatives, 0, etc. They can do that because the argument is typed.


I'm sure there are such frameworks in untyped languages. Something that allows you to write 'integers.test(factorial)'. But if we use this, then it means we're typing our arguments in the test (saying the 'n' is an int), then why not type it in the source code and have all the other benefits of typing? 


Inferring behavior from type



Another example of where types help is they can allow to infer behavior. In Scala this is done with implicit arguments. Consider this method:

def sort[A](l: List[A]): List[A]

There is no way to write this method. The reason is that sort needs to compare the elements (without resolving to reflection hacking). Another approach is this:

def sort[A <: Comparable](l: List[A]): List[A]

Now we've endoded that for every list of Comparable elements, it can be sorted. This is nice, but it means that elements are subtype of Comparable, which may not always be true (primitives, 3rd party code). It also means there's one way to compare. A better approach is this:

def sort[A](l: List[A], c: Comparator[A]): List[A]

Which means that given a list and a way to compare elements, we can get a sorted list. However, such a code is not very nice to use, since every call must now contain another argument which the client needs to provide.

Scala has implicit arguments. This feature uses the type in a method signature to find instances  required for arguments:

def sort[A : Ordering](list: List[A]): List[A]

This reads as 'for all A with associated or explicit Ordering, a list of A can be sorted'.
Now we can supply implicit values for various types and the compiler will create the code that uses the right value for each call of sort. This is only possible because we have the type to tell the compiler what to find.


I hope this post convinced you to use types to encode the logic of your program. TDD FTW!