3 ms·

Only insofar as your types essentially become the bones of the program... which you'll then want to refactor at some point. Types are awesome. Languages like R

Only insofar as your types essentially become the bones of the program... which you'll then want to refactor at some point. Types are awesome. Languages like Rust give them to me without having to learn a ton of theory. However, eventually, I realise that my types have boxed me into a certain design - and I need to refactor heavily, which involves rewriting a large chunk of my types which I was relying on to show me that my code was correct.

lmm 10y ago
Of course you sometimes need to refactor your types. That's fine; the type checker will guarantee that you can do so safely. You probably want to be cautious about changing your axioms, and to that end it might be worth distinguishing them explicitly, but that's easily done (e.g. you can put them in a separate module).
- vertex-four 10y ago
  It'll tell you your program compiles. Unless you've gone seriously overboard and typed every piece of information down to primitives, and built your types so there's no possible way to convert them out of those types at the wrong time, you've still got a chance of having bugs. Functionality testing will tell you when you've failed to encode an invariant in your type, and there's a good chance that the reason you failed to is just that it's more effort than it's worth. Else we'd all be writing proofs for every program in Coq.
  - paulddraper 10y ago
    Do your tests also contain every single piece of information?
    - vertex-four 10y ago
      You can at least add a new test easily when someone reports a bug. Tightening up your types, otoh, is a trade-off against brittleness. In practice, as I alluded to in my previous post, you really want types combined with broad functionality testing across a range of scenarios. You really don't want to be relying on "it compiles, I assume it works" unless you're able to back out of a deployment in seconds when it doesn't.
      - lmm 10y ago
        Tests are much more brittle than types; automated tooling doesn't know what the tests are saying, and there's no way to make code "test-generic". Some things are probably not worth typing, but if they're not worth typing they're not worth testing either. Whatever your target defect rate, the most efficient way to hit that target is using types.
        vertex-four 10y ago
        > there's no way to make code "test-generic" Sure there is. Stop testing random bits of internal functionality, start testing huge modules with well-known (semi-public) APIs, or your entire program, and combine that with a ~reasonable~ type system. You want full-system testing. You don't need a whole lot of tests to be sure "it's basically working", and it's a lot easier to turn repeatable bug reports into tests. When you inevitably break a piece of functionality despite your types, you might not know precisely how it broke, but at least you know it's broken without a customer calling you up. And every time a customer does call you up, you can add a full-functionality test - "this is what the user did, and this is what I expect from that". Every other engineering branch backs up good practices and solid math with lots of testing. So should we, types or no types.

lmm 10y ago

Of course you sometimes need to refactor your types. That's fine; the type checker will guarantee that you can do so safely. You probably want to be cautious about changing your axioms, and to that end it might be worth distinguishing them explicitly, but that's easily done (e.g. you can put them in a separate module).

vertex-four 10y ago
It'll tell you your program compiles. Unless you've gone seriously overboard and typed every piece of information down to primitives, and built your types so there's no possible way to convert them out of those types at the wrong time, you've still got a chance of having bugs. Functionality testing will tell you when you've failed to encode an invariant in your type, and there's a good chance that the reason you failed to is just that it's more effort than it's worth. Else we'd all be writing proofs for every program in Coq.
- paulddraper 10y ago
  Do your tests also contain every single piece of information?
  - vertex-four 10y ago
    You can at least add a new test easily when someone reports a bug. Tightening up your types, otoh, is a trade-off against brittleness. In practice, as I alluded to in my previous post, you really want types combined with broad functionality testing across a range of scenarios. You really don't want to be relying on "it compiles, I assume it works" unless you're able to back out of a deployment in seconds when it doesn't.
    - lmm 10y ago
      Tests are much more brittle than types; automated tooling doesn't know what the tests are saying, and there's no way to make code "test-generic". Some things are probably not worth typing, but if they're not worth typing they're not worth testing either. Whatever your target defect rate, the most efficient way to hit that target is using types.
      - vertex-four 10y ago
        > there's no way to make code "test-generic" Sure there is. Stop testing random bits of internal functionality, start testing huge modules with well-known (semi-public) APIs, or your entire program, and combine that with a ~reasonable~ type system. You want full-system testing. You don't need a whole lot of tests to be sure "it's basically working", and it's a lot easier to turn repeatable bug reports into tests. When you inevitably break a piece of functionality despite your types, you might not know precisely how it broke, but at least you know it's broken without a customer calling you up. And every time a customer does call you up, you can add a full-functionality test - "this is what the user did, and this is what I expect from that". Every other engineering branch backs up good practices and solid math with lots of testing. So should we, types or no types.