3 ms·

Okay, can you say how you would reasonably catch the typo in my second example with types? Obviously you have to be willing to use types to express intent, but

Okay, can you say how you would reasonably catch the typo in my second example with types? 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.

wtetzner 9y ago
int* increment(int* i, int step) { return i + step; } I think your example is flawed. The real problem here is that you're allowed to add an int to an int* with +. int* is not be of type int, and should therefore require some sort of cast to make it possible to add an int to it. Either that, or require a different operator/function to add to a pointer, e.g.: int* increment(int* i, int step) { return prt_add(i, step); } Not all type systems are equal, and how the type system interacts with the language is important.
- kerkeslager 9y ago
  That's my first example, not my second. I specifically asked about the second example because it's fairly obvious that C's type system is garbage. To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function? increment x = x + 11; ...noting that this typo is reliably caught by a unit test.
  - tome 9y ago
    How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) 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.
    - kerkeslager 9y ago
      > How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) This isn't a trick question. You run the test, and see that it fails. 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.
      - tome 9y ago
        My point is, when the program is the same as the specification then there's essentially no point writing either tests or proofs. Therefore, I think your point would be better demonstrated using a more complicated example.
        kerkeslager 9y ago
        This is getting a bit off topic and into the theory of how you write tests, but if you wrote a better test it wouldn't be the same as the specification. 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 This is admittedly overkill, but the point is you really should only be testing inputs and outputs in a test, not doing calculations. > 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) I won't paste the full test here because this is part of a larger function, but rest assured I'm not duplicating the definition of the function in the test. 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), )
        tome 9y ago
        Aha, yes, OK, I agree. Good example.
    - dllthomas 9y ago
      Ideally, it's like double-entry book keeping. If you try to express the same thing in two different places, ideally in two different ways, you're less likely to make the same mistake in both places than to make any mistake in the first place. This applies both to types and tests.
      - kerkeslager 9y ago
        Exactly!
naasking 9y ago
If the context is Haskell, I'd probably user type-level naturals to encode the correct input/output types. 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.
- kerkeslager 9y ago
  Okay, I didn't ask clearly enough. The following function is supposed to take x and return x + 1: increment x = x + 11; How would you catch this bug via a reasonable usage of the type system? Noting that a unit test catches this bug trivially.
  - naasking 9y ago
    I know what you asked, and I answered as best I could without further information. The solution ultimately depends on the specific type system. Like I said, with Haskell I'd use type-level naturals to ensure the output type is 1+input type. 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.
    - kerkeslager 9y ago
      > Like I said, with Haskell I'd use type-level naturals to ensure the output type is 1+input type. 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.
      - naasking 9y ago

wtetzner 9y ago

int* increment(int* i, int step) { return i + step; } I think your example is flawed. The real problem here is that you're allowed to add an int to an int* with +. int* is not be of type int, and should therefore require some sort of cast to make it possible to add an int to it. Either that, or require a different operator/function to add to a pointer, e.g.: int* increment(int* i, int step) { return prt_add(i, step); } Not all type systems are equal, and how the type system interacts with the language is important.

kerkeslager 9y ago
That's my first example, not my second. I specifically asked about the second example because it's fairly obvious that C's type system is garbage. To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function? increment x = x + 11; ...noting that this typo is reliably caught by a unit test.
- tome 9y ago
  How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) 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.
  - kerkeslager 9y ago
    > How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) This isn't a trick question. You run the test, and see that it fails. 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.
    - tome 9y ago
      My point is, when the program is the same as the specification then there's essentially no point writing either tests or proofs. Therefore, I think your point would be better demonstrated using a more complicated example.
      - kerkeslager 9y ago
        This is getting a bit off topic and into the theory of how you write tests, but if you wrote a better test it wouldn't be the same as the specification. 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 This is admittedly overkill, but the point is you really should only be testing inputs and outputs in a test, not doing calculations. > 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) I won't paste the full test here because this is part of a larger function, but rest assured I'm not duplicating the definition of the function in the test. 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), )
        tome 9y ago
        Aha, yes, OK, I agree. Good example.
  - dllthomas 9y ago
    Ideally, it's like double-entry book keeping. If you try to express the same thing in two different places, ideally in two different ways, you're less likely to make the same mistake in both places than to make any mistake in the first place. This applies both to types and tests.
    - kerkeslager 9y ago
      Exactly!

naasking 9y ago

If the context is Haskell, I'd probably user type-level naturals to encode the correct input/output types. 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.

kerkeslager 9y ago
Okay, I didn't ask clearly enough. The following function is supposed to take x and return x + 1: increment x = x + 11; How would you catch this bug via a reasonable usage of the type system? Noting that a unit test catches this bug trivially.
- naasking 9y ago
  I know what you asked, and I answered as best I could without further information. The solution ultimately depends on the specific type system. Like I said, with Haskell I'd use type-level naturals to ensure the output type is 1+input type. 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.
  - kerkeslager 9y ago
    > Like I said, with Haskell I'd use type-level naturals to ensure the output type is 1+input type. 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.
    - naasking 9y ago