types_AND_tests.md

Here's a response to Uncle Bob's post here: http://blog.cleancoder.com/uncle-bob/2017/01/13/TypesAndTests.html

No, types are not tests. Type systems are not tests. Type checking is not testing. Here’s why.

Types definitely are not tests. Types are stronger than tests. This is a test:

describe 'add' do
  it 'returns a number when given two numbers' do
    expect((1 + 2).class).to be Numeric
  end
end

This is a type:

add :: Num a => a -> a -> a

The test says that for the numbers 1 and 2, when I add them together I get a number back. The type says that for any two Numeric types I add together, I'll always get a Numeric type back.

A computer program is a specification of behavior. The purpose of a program is to make a machine behave in a certain way. The text of the program consists of the instructions that the machine follows. The sum of those instructions is the behavior of the program.

This seems like a naive point of view. Yes a computer program is a specification of a behavior. However there are many programs that are not sequences of instructions. For example, this program to calculate Fibonacci numbers:

fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

main = do
  print (fib 20)

This is almost a literal translation of the mathematical formula for calculating the Fibonacci numbers. It's very different from a sequence of instructions.

Types do not specify behavior. Types are constraints placed, by the programmer, upon the textual elements of the program. Those constraints reduce the number of ways that different parts of the program text can refer to each other.

This is the real doozy. I think I understand what Bob's getting at in the second part of this paragraph. It's that a type checker is static. It imposes constraints on the structure of the program. This is true, if a bit awkwardly worded. However types absolutely can specify behavior! For example, here's a test:

describe 'Order#purchase' do
  it "raises an error when the order isn't confirmed" do
    order = create_unconfirmed_order(3.00)

    expect { order.purchase }.to raise UnconfirmedOrder
  end

  it "changes the status of the order to purchased" do
    order = create_confirmed_order(3.00)

    expect(order.purchased?).to be false

    order.purchase

    expect(order.purchased?).to be true
  end
end

And here's some types:

data Order status = Order { price :: Integer }
data PurchasedStatus
data ConfirmedStatus

purchase :: Order ConfirmedStatus -> Order PurchasedStatus

The test says that Order#purchase has two behaviors: it can't be called on unconfirmed orders, and when called it changes the order status to purchased. That sounds like a test of behavior to me.

The type uses a technique in Haskell called phantom types. They are used to specialize a type. In this case we specialize the Order types in the signature of purchase to say two things. The first is that we can never call purchase with an unconfirmed order. This is a much stronger statement than we made in the test, and actually frees me as the programmer from even worrying about handling that case. The second statement is that, in our domain of orders, we can treat any order that comes out of purchase as purchased. This is, again, a much stronger statement than a purchased? method.

I'll give a fair shake to the Ruby system in that we can also achieve some of the same guarantees as we do with the Haskell type system. See:

class ConfirmedOrder
  def purchase
    # do magic
    return PurchasedOrder.new
  end
end

class PurchasedOrder
end

In the same manner that we said purchase can never be called on an unconfirmed order in the Haskell code, now we can never call purchase on an unconfirmed order in the Ruby code. We've also eliminated the need for a purchased? check be clarifying what that means in the domain model.

Note that I did not specify in either tests or types what exactly happens when an order is purchased. It might be that a credit card is charged or an email is sent. Those are both things that we would test regardless of the type system. I agree that types are not a replacement for all tests. However they are a replacement for many tests, and types absolutely can specify behavior.

You might therefore say that the type system is a kind of “test” that fails for all inappropriate invocations of f. I might concede that point except for one thing – the way f is called has nothing to do with the required behavior of the system. Rather it is a test of an arbitrary constraint imposed by the programmer. A constraint that was likely over specified from the point of view of the system requirements.

I'd like to point out that the way f is called absolutely has something to do with the required behavior of the system. If f is purchase and it's called on an order that doesn't have all of the appropriate information for charging a credit card that is an inappropriate invocation of f! Types can make that impossible. I will concede that specification takes practice. It does not come for free, but it can be learned.

Now this is no small thing. Writing program text that is internally consistent is pretty important. Inconsistencies and ambiguities in program text can lead to misbehaviors of all kinds. So I don’t want to downplay this at all.

On the other hand, internal self-consistency does not mean the program exhibits the correct behavior. Behavior and self-consistency are orthogonal concepts. Well behaved programs can be, and have been, written in languages with high ambiguity and low internal consistency. Badly behaved programs have been written in languages that are deeply self-consistent and tolerate few ambiguities.

These two paragraphs are actually contradictory. Bob says that inconsistencies and ambiguities can lead to misbehaviors. Then he proceeds to say that behavior and self-consistency are orthogonal concepts. If they truly were orthogonal, how could inconsistencies lead to any behavioral changes? I suspect that Bob is mixing up two different perspectives of behavior here: behavior as specified by the programmer, and behavior as specified by the end-user. A fully specified program will exhibit precisely the behavior that is specified by the programmer. In that sense it can never have a bug. However, that same program might not have the behavior as specified by the end-user. Types cannot help with translating user requirements correctly. However they can help in making sure the specifications of those requirements are consistent and prevent undesired behaviors.

So just how internally consistent do we need the program text to be? Does every line of text need to be precisely 60 characters long? Must indentations always be multiples of two spaces? Must every floating point number have a dot? Should all positive numbers begin with a +? Or should we allow certain ambiguities in our program text and allow the language to make assumptions that resolve them? Should we relax the specificity of the language and allow it to tolerate certain easily resolvable ambiguities? Should we allow this even if sometimes those ambiguities are resolved incorrectly?

This is disingenuous and seems to relegate type checkers to a role of glorified spell checkers and linters. They are much, much more powerful than that.

Clearly, every language chooses the latter option. No language forces the program text to be absolutely unambiguous and self consistent. Indeed, such a language would likely be impossible to create. And even if it weren’t, it would likely be impossible to use. Absolute precision and consistency has never been, nor should it ever be, the goal.

I'm not sure if Bob is being deliberately obtuse or not, but ambiguous program text leads to undefined, implementation defined, or just downright confusing behavior. The point of programming is to be predictable, and for something to be predictable it must be unambiguous.

The problem with increasing the level of precision and internal self consistency, is that it implies an increase in the number of constraints. But constraints need to be specified; and specification requires notation. Therefore as the number of constraints grows, so does the complexity of the notation. The syntax and the semantics of a language grows as a function of the internal self-consistency and specificity of the language.

What are we arguing against here, syntax or concepts?

Do languages like this exist? No; but the more type-safe a language is, the more internally consistent and specific it forces the programmers to be, the more it approaches that ultimate TDP condition.

This is blatently false. A language can be very type-safe, include polymorphism and allow programmers to be as general as possible. Haskell is proof of this. On a side-note, the more generic a function is the more specific its implementation must be. Counter-intuitive I know, but think about the following functions:

id :: a -> a

foo :: Int -> Int

How many possible implementations of id are there that satisfy the generic constraint that for any value we pass in we get any value back. Because we must handle any value, we can't make any assumptions about the value. So there's only one thing we can do, immediately returned the passed in value. On the other hand, the more specific function foo has a practically infinite number of implementations because there's a practically infinite number of integers. A corollary to this is that when there are more potential implementations you must write more tests. This is why Haskellers tend to favor generic functions so much. There are fewer ways for them to be wrong.

Every step down that path increases the difficulty of using and maintaining the language. Every step down that path forces users of the language to get their type models “right” up front; because changing them later is too expensive. Every step down that path forces us back into the regime of Big Design Up Front.

I'd like to know in what way Bob is saying languages get more expensive. If he means that changes require more subsequent changes to remain consistent I'll agree. However those come with the very nice tradeoff that the type checker tells you every single place you need to change. So in another sense (the cognitive overhead sense) it actually becomes cheaper.

No. A thousand times: NO. Type models do not specify behavior. The correctness of your type model has no bearing on the correctness of the behavior you have specified. At best the type system will prevent some mechanistic failures of representation (e.g. Double vs. Int); but you still have to specify every single bit of behavior; and you still have to test every bit of behavior.

Again, false as I've demonstrated above. Types do specify behavior. The consistency of your type model absolutely has a bearing on the correctness of the behavior you the programmer have specified. Bob is also persisting in his notion that Doubles and Ins are the only types we've got, when a good type system will allow cheap user defined types to precisely capture a domain model.