As a side note: The TDD-ish alternative to this, which I also use sometimes is just adding a test where you pass in undefined on your optionals, and then iterating until the test stops throwing.
int* increment(int* i, int step)
{
return i + step;
}
Even Haskell's type system can't tell what you intend:
increment i = i + 11;
A unit test would clarify the intent of both these functions, and catch both bugs fairly reliably (if they aren't the intended behavior).
Ultimately I think TDD and types guarantee different things, and both are useful/needed.
Proving Programs Correct Using Plain Old Java Types, http://lambda-the-ultimate.org/node/5387
Obviously you have to be willing to use types to express intent, but even if you're willing, types are limited in what kinds of intent they can express.
int* increment(int* i, int step)
{
return i + step;
}
int* increment(int* i, int step)
{
return prt_add(i, step);
}
To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function?
increment x = x + 11;
def test_increment(x):
assertEqual(increment(x), x - 1)
def test_increment(x):
assertEqual(increment(x), x - 1)
If you write the wrong test or the wrong type AND the wrong implementation, they won't help you, but the point of both types and tests is that you have to make two mistakes for a bug to get into production. It's possible that in your test, I could have made the same error in the implementation of `increment`, but it's a great deal less likely than making that error in just the implementation or just the test.
And to be clear, I'm not saying any of this as a "types versus unit tests" thing. I've specifically said that both are useful and needed for reliable software.
> The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge.
You totally can catch this bug with some type systems (Coq, for example), it's just much easier to catch this bug with a unit test in most languages.
I think that your boss would probably disagree with you that this bug is not meaningful if it makes it into production. You don't get to pick and choose which bugs are meaningful because they don't support your views.
def increment(x):
return x + 1
def test_increment():
assert increment(0) == 1
assert increment(1) == 2
assert increment(42) == 43
assert increment(-5) == -4
> Therefore, I think your point would be better demonstrated using a more complicated example.
The example is a simplification of a bug I came across last year:
available_date = datetime.date.today() + datetime.timedelta(days=11)
The intern who wrote the code didn't know how to use mocks to mock out `today` so they didn't write a test, resulting in this bug. I remember this case because I use it as an example to teach mocks.
I simplified my original example to make it clearer, but I think you'll see that this real-life bug suffers from the same difficulties if you try to verify it with a type system, but is (fairly) easy to test.
EDIT: Actually, the relevant bits of the test were fairly simple (from memory so please excuse errors):
@unittest.mock('datetime.date.today')
def test_available_date_set_to_tomorrow(self, today):
today.return_value = datetime.date(1984, 4, 20)
[...]
ticket_claim = claim_ticket(user, voucher)
self.assertEqual(
ticket_claim.available_date,
datetime.date(1984, 4, 21),
)In other contexts without polymorphic types, like with C, I'd wrap the input and output types in custom structs that expose trusted operations. The more minimal the better. It's definitely more cumbersome without polymorphism, but you do what you can for the code that's mission critical.
increment x = x + 11;
In C, my first thought would be to define a static value representing ONE, checked via static_assert, and then the increment function becomes input + ONE.
I'm a bit out of my comfort zone with this one so I may be wrong, but wouldn't that require a lot of coding to define type level naturals for all the possible values of X?
> In C, my first thought would be to define a static value representing ONE, checked via static_assert, and then the increment function becomes input + ONE.
Okay, but do you agree that in this case a unit test would be a better solution?
I'm not saying this as a types versus unit tests sort of thing. I'm saying both are needed tools for writing reliable software.
Not for your simple example. See [1] for more info. There are a number of packages that do the work for you.
[1] https://wiki.haskell.org/Type_arithmetic
> Okay, but do you agree that in this case a unit test would be a better solution?
Depends how mission critical the property is. Even simple increments and offsets might deserve some type-level encoding if they are core, mission critical properties.
For other things, tests are fine, although I recommend property-based testing frameworks like QuickCheck, Hypothesis, etc. which test logical properties against a large range of input values instead of a static set of values encoded into your tests.
On the other hand, I don't see that they'd actually be useful for catching this error in any way people are likely to use, although I'd be interested to see attempts...
On the third hand, the way I'd actually implement this in Haskell is probably `succ`, so typo would be caught during compilation. But of course you can construct alternative examples.
To my mind, types and tests are very much complimentary - ideally tests check that your solution gives correct answers at some points in your domain, while types help make that space more uniform (so if it's correct at some points it's more likely correct at others). There are some practical cases where the types sufficiently constrain things that checking any actual points is redundant, but that's not the common case.
Yeah, this is my ultimate point, and I worry that some people have misunderstood my intent. I'm not criticizing types: I think they're a very important tool. I'm saying that types don't handle every kind of possible error. And conveniently, tests often cover the kinds of errors that types don't (and vice versa).
It’s a one-liner in Haskell (two if you count the DataKinds pragma):
data Nat = Z | S NatRegardless, even with Java's limited expressiveness you can encode some powerful propsitions, as the paper I linked shows.
The paper you linked uses Java's type system for a mechanized proof, meaning...you probably don't want to be writing that out by hand.
I think that's overstating it a little too. You don't have to use the dependent types, at their core, Coq and Agda are still functional languages and you can just stick to algebraic sums and products and still enjoy type inference. Most people aren't using these languages for general purpose programming because a) poor tooling, and b) because they are explicitly marketed as research languages.