4 ms·

Leaving Haskell's deferred type errors aside for a moment; after you are done with your partially working code, what then? Relying on (the surely preexisting) 1

• kazinator 10y ago
  Say you have 65% test coverage over the refactored code. You have that before the refactoring and you have it after. What does it mean? It means 35% of the code is being refactored without coverage. Its status is "unknown" before refactoring and "unknown" after. Oh, but it compiles!
  • pka 10y ago
    But if it compiles its status is not unknown. It means it is well typed, proving the absence of a whole lot of bugs. Generally, refactoring in dynamic languages without tests or something like Clojure's schema is madness. Usually not a problem in strongly typed languages, even without much test coverage.
    • kazinator 10y ago
      Well typed means nothing. Complete garbage can be well typed. Well typed proves the absence of a tiny, tiny subset of the possible bugs. A subset which has nothing to do with, for instance, the corretness of loops. Because type checking doesn't verify those. Well typed doesn't even tell you whether a program terminates or not and on what inputs. A program that is supposed to calculate pi could calculate e instead, yet be well typed (everything is a double-precision float, or a function from several of them to one, check!)
      • pka 10y ago
        As I said above, you can verify/prove the invariants you capture in the types. I don't know what you mean by "correctness of loops", but if you capture whatever it means in a particular type, yes you can. If you really wanted, you could derive a proof that pi is equivalent to some sort of corecursive series, which you can then evaluate in a dependently typed language, I guess. A proof is a type. On the other hand, how would you write a unit test that checks whether something calculates pi without comparing its result to pi itself?
        • kazinator 10y ago
          If I really wanted to waste my time, yes. > A proof is a type. Yes, Curry-Howard and all that. If I just write a well-typed function which supposedly calculates pi, the rather trivial well-typedness is not informative by itself. You're talking about adding reams of verbiage requiring expertise in using an advanced type system for executing a proof. This isn't how static type systems are actually used and advocated in the field, and it is not feasible in general, only for toy, academic examples. The proof code, which will exceed the size of the original function by at least an order of magnitude, could also be buggy. At the end of the day, it's just more code. It reminds me of the argument fropm the Lisp camp: "Well, I could just write (supermacro ...) which implements any syntax and semantics whatsoever". (No, in fact you can't, and the proof is that you never actually will.)
      • dllthomas 10y ago
        > Well typed doesn't even tell you whether a program terminates or not and on what inputs. On the contrary, knowing that a piece of lambda calculus can be simply typed tells me for certain that the program halts for all inputs. If you demand it work for arbitrary programs, then sure, well typed doesn't "even" tell you that. But no procedure can "even" tell you that (including, probably, anything that can be done by our brains), so it's a rather odd choice as a low-bar.
    • deleted 10y ago
      [deleted]