Hacker News Reader

Comment by kazinator | Hacker News Reader

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

View on HN

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

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?

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

Reply on news.ycombinator.com