Re:Learning Elm has gotten me confused about static vs. dyna...
by dllthomas on Wednesday June 15, 2016 @02:50AM
(#11907570)
> 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.
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.