3 ms·

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

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).