Unification Of Static Types And Unit Tests

As noted in StrictTypingIsaTest, it is worth considering StaticTypeSafety and UnitTests as closely related tools, two approaches that mesh together. They are not just different approaches. UnitTests are general and flexible. StaticTypeSafety just breaks out one part of what you can do with UnitTests and puts it on a formal basis.

There are countless analogies for this. In AssemblyLanguage, you can implement loops by jumping back to the start of a section of code until some register contains the value zero. Along with subtraction, this lets you build the equivalent of for loops, while loops, do loops, and any other kind of loop you could think of. So it's very powerful. But if you've got high-level alternatives, it's better to use them, because there's less donkey-work that way, and less chance to make a mistake. It's just a kind of reuse.

StaticTypeSafety is like the while loop. Hand-coded UnitTests are like jump-if-not-zero instruction. Therefore, you can survive without StaticTypeSafety because you can implement the same things with UnitTests. But if you have StaticTypeSafety in your environment, you may as well use it, because it will save you writing and maintaining a specific subset (see below) of your test code. But it will still leave you with stuff that requires UnitTests to be designed and implemented.

I agree with (what I perceive to be) the essence of the preceding paragraph, but feel that it does not go far enough. UnitTests let you achieve the goal of confirming, after the fact, that you have done what what you intended to do, or the (perhaps weaker) goal of confirming that you have not done what you did not intend to do (or what you intended not to do, which is not necessarily the same thing) (gee, this is getting grammatically complicated...). The point is, they operate after the fact: you code something, and then you test what you coded. StaticTypeSafety can be used to achieve that purpose in a different way: by making constructs that do what you didn't intend illegal. But it obviously isn't as powerful for that purpose as UnitTesting, since there are things a static type system cannot express that a UnitTest can check. This is discussed below. But the point that this misses is that StaticTyping is visible during the coding, and expresses intention. After all, the guy who writes code knows what he's trying to achieve, and will not stop working on the code until he has achieved it, regardless of what tools he has at his disposal. The real danger is the guy who comes along later, who may have only an imperfect understanding of the original intent. StaticTyping helps him because it makes the original intent manifest while he is working on the code. A UnitTest can confirm, later, that he hasn't violated that intent, and make him go back and fix it if he has, but isn't the code more likely to be right in the first place if the intent is clearly visible as he's working on it?

I think something is missing from the paragraph above: TestDrivenDevelopment, eg you should write a test for functionality before writing code to add that functionality (not "after the fact"). This actually makes a tremendous difference. I would be very suspicious of anyone claiming to have thorough UnitTests who did not do this. It's very hard to add good unit testing after code has been written. It is also worth noting that the presence of UnitTests, while it can't ensure that refactoring won't break anything, adds to confidence massively. I have seen many, many statically typed systems rewritten because the absence of unit tests made incremental refactoring impossible. After all, you can't break stuff out subsystem by subsystem and rework it unless you know what the subsystems are supposed to achieve.

Writing the preceding paragraph led me to consider a seemingly related weakness of UnitTests (which might be better discussed elsewhere; if so, please move this, but please also leave a reference here). Suppose a maintenance programmer comes back to your code at a later date, makes changes, and does so in a way that causes some UnitTest to fail. Isn't it possible that he will (unwisely) decide to ignore the failure, and instead delete the bothersome UnitTest from the testing suite? He may believe that the condition tested for is invalidated by new requirements (and if he's correct, I suppose deleting the test is the right thing to do), but there's also the chance that he'll simply say "Oh well, it's only a test; the main program still compiles and runs..." and forget about it. However, when intentions can be captured and expressed in code, they are harder to disregard: if a property or behavior can be guaranteed of any instance of a class (or value of a type) merely by the fact of its being an instance of the class (or by the value having that type), then a later programmer cannot violate that property or behavior unless he is willing to rewrite the context sufficiently that the value in question no longer has that type. Saying that "in this function, the parameter my_car is of type FamilySedan?, and not merely of type MovingObject?" both communicates the intended use of the parameter and also prevents the later programmer's accidental misuse of the routine on the calling side (he can't pass in a LearJet? or a CitrusFruit?) and in the function body itself (he cannot invoke some Toyota-specific behavior). To change the behavior he would have to change the type of the parameter, and if this mattered, it would create type errors all through the system. So, as I see it, StaticTyping lets such of the original programmer's intention as it is capable of expressing be embedded in the code in a less ignorable way than UnitTests, and I guess I think that's a GoodThing. Maybe it's just because of my background with BondageAndDisciplineLanguages, or with the TypedLambdaCalculus. -- CameronSmith

Apologies for my prolixity. I will try to condense the above later. Others are welcome to do so, if they can do it in a meaning-preserving way. But I want to be clear: I am not arguing against UnitTests, which is why I put this comment on a Unification... page. I think UnitTests and StaticTyping serve different aims, or serve the same aims differently, and I think it's not a question of "if you have one do you really need the other".

---

OH MY (insert deity of your choice here.) !!! This is the single most coherent comparison of the two methodology camps I've ever seen. Thank you!

---

Why Is StaticTypeSafety Deliberately More Limited?

Suppose that there is an integer in my program:

  int nMilesPerHour; // Must always have a value between 0 and 55

Fact: It is impossible to construct an algorithm that can (given finite time) analyze any arbitrary program and ensure that the condition in the comment is always met. (It comes from the the HaltingProblem. To put it simply, some programs just have to be executed in order to check such things, and some will neither terminate nor break the condition, so the compiler would hang up whilst attempting to check them! Related to GoedelsIncompletenessTheorem.)

• One should note that, despite this fact, one needn't actually find a solution that applies to "any arbitrary program". Going for a solution that applies to at least the more common programming patterns is good enough. When programmers need to perform a proof, they often help themselves out by structuring the code to make a necessary proof a bit easier, and providing hints in the form of comments. If one wishes for a static type system and apply a guarantee that nMilesPerHour is between 0 and 55 at all times, this can be done... but the prover might complain and tell you to provide more structure or better hints so it can complete the proof within some delta-t milliseconds. There will still be limits on what the prover can prove (even given its axioms AND any assumption-hints you specify), but those limits can be expanded far, far beyond the provably decidable.

StaticTypeSafety can only perform checks that don't hang up, or you would complain about a bug in the compiler. So it limits itself to checking for those things that can be verified without getting into such problems. It steps aside for anything else and says "sorry, you'll have to write a UnitTest for that, I'm not going to get hung up!"

• StaticTypeSafety systems don't need to be decidable. They just need to not "hang up". Once you decide you're going to use an undecidable type system, that's when things become interesting - you need to design the computation differently (so it proves as much as it can rather than focusing on some single object forever), and you need to prevent hangs by another mechanism than trusting the type-check to terminate naturally (e.g. provide user-adjustable time and memory limit for computation). Finally, you need to handle the new case where you do end up running out of resources - the ability to tell the programmer where some restructuring of code or an extra hint might aide the proof, for example, or saying what it could prove and which pieces the code is missing. Or, if you're using SoftTyping, simply insert the necessary checks for those places the proof failed. After deciding to support the potentially undecidable, this becomes as much a user-interface issue as it is a type-system issue.

There are other statically typed languages that have ordinal types, in which case the example above becomes:

 TYPE MilesPerHour? = [0..55];
 VAR milesPerHour : MilesPerHour?;

The nice thing about this is that you (and your compiler) can throw away bounds checking. You can say things like:

  TYPE WorkDays? = [Monday, Tuesday, Wednesday, Thursday, Friday];
  VAR dailyResults : ARRAY WorkDays? OF Result;

Whilst such languages do allow you to specify the bounds, they do not guarantee to test them at compile-time. For example, does the assignment

 milesPerHour = milesPerHour + 7;

violate the bounds? To decide this, we'd need to know the precondition. Even a language like Eiffel does not allow you to specify sufficiently powerful pre/post conditions to permit static analysis in all cases.

So instead of static analysis, the compiler inserts run-time assertions. You hope that these will never be triggered, but can you be sure? Well, you can't be certain; but you can write UnitTests to hit the boundary conditions. If you have post-conditions in your contracts then the unit tests will not need to check the results: they only need to stimulate the interesting input patterns.

''By using an integer instead of an object that encaps the idea of miles per hour you have deliberately said any integer value is ok and any integer operation is ok. If you don't want that then don't be lazy and make a real abstraction. Just this simple approach could have solved the Arianne-5 disaster.''

[True, but that's beside the point of the example. In the RealWorld, one wouldn't (or shouldn't) use an int to represent a continuous physical parameter like miles per gallon anyway; a float is the most appropriate datatype for such quantities in most languages. Depending on how much precision you want to give to the milesPerGallon parameter]

No, a MilesPerHour? object the best representation because that can enforce semantics. If a float is used internally it hardly matters. Using a MilesPerHour? object allows the compiler to make sure it is used being properly. Runtime checks add another level of checking.

[Agreed, which is what I meant: A discrete unit type to represent the quantity; with a more appropriate internal representation (i.e. not an integer).]

---

Two Aspects of UnitTests

We can consider two aspects of unit tests:

• State Tests - which do the things described above that require some code execution to take place, and so need some creative input to ensure that they test something worthwhile, but still don't spend an infinite amount of time doing it.

• Interface Tests - which actually do the same job as StaticTypeSafety.

Most of the information used for type safety naturally falls out of the way you write a class anyway (this is much more true of Java than C++.)

So why do that part yourself, manually, every time? Why not get the computer to do that part for you?

---

Automatically Generated UnitTests

To make this as clear as mustard, let's try to answer the question, what parts of typical UnitTests can we invent a tool to automatic generate?

Suppose we were working in a non-typesafe language that let us define classes like this:

  class StairMaster
  {
public void goUp();
public void goDown();
public boolean isUpstairs();
  };

A reasonably pure interface test for this class would be like this:

  try
  {
StairMaster sm;
sm.goUp()
sm.goDown()
bool junk = sm.isUpstairs();
  }
  catch(MethodCallException e)
  {
// report failure!
  }
  catch(...)
  {
// ignore all other exceptions (this is a pure interface test)
  }

All this test does is attempt to call the methods that should be there. It isn't interested in what effect they have on the state of the object (for example, we don't check that junk is false.)

So this test can be used to verify if another class is polymorphically compatible with StairMaster?, and so can be used by any StairMaster? clients.

Of course, this unit test can be automatically generated by a tool that reads the class declaration. That's all StaticTypeSafety is. It saves you hand coding those parts of your UnitTests.

What you described here is hardly enough of an UnitTest to replace static type checks. You miss to specify how you get that reference (not to mention that it is pointless to declare it StairMaster x in an untyped language (you just state something like var x= someFunction( someArguments); ), so you have to call a function (or a constructor, but let's assume a constructor is like any other function), that function can return any reference and maybe based on if branches, the results of other functions returning other untyped references, and so on).

So what you presented here is a very symplistic view, and by far not good enough to replace a type-checking compiler. And I hope you won't try to reinvent the whole type theory by means of unit tests. If you do that, please present it in a formal consistent matter, with references to previous work and research, before you lay any claims that you reinvented the wheel. (- That's all StaticTypeSafety is. - You must be kidding, right?) -- CostinCozianu

You seem to have missed the point of my argument - I'm not preaching in favour of abandoning StaticTypeSafety. I'm doing the exact opposite. I'm totally convinced that type safety is important and I'm (consequently) fascinated by those who (a) manage without it and even (b) claim that this gives them an advantage. This Wiki has a general bias against StaticTypeSafety because it (the Wiki) is firmly part of Smalltalk culture. Hence I'm trying to convince Smalltalkers that there is value in the type systems of Java and (dare I say it?) C++, which personally I'm culturally tied to - as I've said elsewhere, I think in interfaces, not classes. Aside from that, if you look at the writings on this Wiki, I think you'll find very few of them are presented as normative specifications with full references! Perhaps you're applying a high standard here simply because you don't like what (you thought) I was saying? :) -- DanielEarwicker

UnitTests used in this style but beefed up enough to be useful would likely turn out to be design by contract, wouldn't they?

Anyway, how can I automatically generate unit tests when I write the tests first? What would be more useful would be to have a tool that automatically (and without me ever having to see them) generated the class definitions that my tests need to compile today. -- KeithBraithwaite

You can actually do this with QuickCheck, because you only establish properties that must be for all legal inputs, not properties that must be true for a single input. -- ShaeErisson

---

It is impossible to construct an algorithm that can analyze any arbitrary program and ensure that the condition in the comment is always met.

This is true, but misleading. Most people aren't interested in properties of arbitrary programs, such as generated by the proverbial monkey on the typewriter. There is some research in type systems that are not decidable, which means that your compiler might loop. Which sounds scary, but bear in mind that even compiling C++ programs is undecidable in general (due to possible non-termination of template expansion).

See the Cayenne paper:

http://www.cs.chalmers.se/~augustss/cayenne/paper.ps

More recently, Epigram:

http://www.e-pig.org/

Extending/explaining this. It's obvious that with or without static typing, unit tests are useful. Further, with or without unit tests, static typing is useful, why? Because static typing can replace an infinite number of unit tests, the same way a proof that there are an infinite number of primes replaces the (impossible) task of showing them. A trivial and unconvincing example is (using Haskell):

  data A = A
  data B = B

  f :: Integer -> Either A B

in a dynamically typed language it would take an infinite set of unit tests to show the simple property (ignoring non-termination), that for all values this function will return either A or B, in a (sound) statically typed language it takes zero. A much less trivial and much more useful example is the use of parametricity in the definition runST (see "Lazy Functional State Threads"). The type disallows one misuse of the library. Furthermore, the misuse is quite subtle and almost certainly would be missed by test suites for a specific application. Yet, with static typing, the fact that your program typechecks is a proof that it doesn't have this bug. (This example is also another example of static typing allowing program optimizations, notable in that it doesn't just get rid of a simple run-time type check. Making a run-time check to catch this misuse would be difficult to implement and difficult to prove correct, and certainly slower.) -- Darius

---

See UnitTestsRequirePerfectDevelopers