3 ms·

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

• 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
      > 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? 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 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.
    • dllthomas 9y ago
      On the one hand, in GHC you already have type level naturals. 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.
      • kerkeslager 9y ago
        > 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).
    • whateveracct 9y ago
      > wouldn't that require a lot of coding to define type level naturals for all the possible values of X? It’s a one-liner in Haskell (two if you count the DataKinds pragma): data Nat = Z | S Nat