Static typing is not a religion that someone can evangelize for or against, it is a practical technique that is proven time and again in - you guessed it, practice. No need to read any crappy layman blogs, sir.
Name:
Anonymous2014-06-25 16:48
I agree that the benefits of static typing are vastly exaggerated by a bunch of weenies who masturbate to the Curry-Howard correspondence every morning, but using Java as an example against type systems is ridiculous.
Name:
Anonymous2014-06-25 16:59
I read this before. It's nonsense. The Milner quote is out of context, as usual.
Most of those errors can be encoded as type errors. The fact is nothing is a type error if you don't first encode things into types, and you get very far with that if your type system is status quo. He's basically complaining that we don't need Haskell because Java is such a steamer.
You have bad taste in programming. That, or do it as a job (idiot).
Name:
Anonymous2014-06-25 17:15
Static typing slows down prototyping. You have to use these "patterns", like inversion of control and Liskov (shalom!) substitution principle, which are never an issue with Lisp. Moreover, in case of garbage collected languages like Haskell or Java, static typing doesn't really provide an optimization, because GC requires tags to be present on objects. The only justified use of static typing is in C and assembly, where it helps accessing structs.
conservative GC doesn't require, but it is also slower and less robust.
Name:
Anonymous2014-06-25 17:46
>>5 I assure you I have a most excellent taste in programming. And indeed, I do program as a part of my job, a concept that appears to be foreign to the static typing Haskell ``elite''.
Name:
Anonymous2014-06-25 17:56
>>6 I'm just trying to find a statement in your post that wouldn't be complete unfounded bullshit.
Name:
Anonymous2014-06-25 17:57
>>9 I'm just trying to find a statement in your post that wouldn't be complete unfounded bullshit.
Name:
Anonymous2014-06-25 18:03
Q: How does one detect a Jew? A: Jews have big 6-curved noses, bulging almond shaped eyes and tend to use statically typed languages. I.e. a lot of Jews use Haskell, inventors of Eiffel and C# are Jewish too!
>>13 I don't think you know what ``almond shaped'' means.
Name:
Anonymous2014-06-25 19:48
>>13 I don't think you know what ``almond shaped'' means.
Name:
Anonymous2014-06-25 20:47
Static typing apologists think that if you use types as a design tools in your coding, then bugs will go away. I.e. to avoid division by zero, static typing zealot would introduce NonZeroInteger and then mediate between it and normal Integer. Lisp allows achieving the same by attaching the code to the interface into the code requiring non-zero input. So static typing basically sweeps bugs under the carpet by obfuscating code.
That premise is false. It's like saying variable assignment and library calls slows down prototyping. Sure, you can prototype with little preamble on some dynamic languages, but by doing so you are risking the effects of missing assignments required for the emulation of the prototype. So when you do not write all your requirements, you end up wasting more time overall trying to emulate the desired prototype.
With static typing, you are forced to write down your requirements, keeping you focused of the overall goal of the prototype.
In GC, it makes even more sense, because proper GCs should have a cache or readily usable types, making it easier to map when operating values.
types as a design tools in your coding, then bugs will go away
That premise is also false. It provides safety in the type system, not coding errors. A type system is not some magical thing that prevent coders from writing spaghetti.
implying coders would use type-system verbosities explicitly to design safe programs, instead of fighting the typesystem and opening ways to circumvent it.
>>16 If you ever tried to use a statically-typed language in practice, you wouldn't spew that childish bullshit. Of course the type system can catch only the most trivial errors (like wrong order of arguments or mapping a function over a list twice in two different places), but these trivial errors make up the majority of your day-to-day errors. Static typing points the boring 90% of bugs out for you, so you have more time to think about the non-trivial bugs or flaws in your design.
And static typing is fast. Where with a unityped language you'd have to compile your program, run it, and wait for it to run the whole test suite, a fully statically typed language points out the type errors without even compiling anything! It's these fast turnaround speeds that make static typing so much better for rapid prototyping and refactoring.
Of course the type system can catch only the most trivial errors
What are you writing, C? Goddamn, learn F# or something. Or even C#.
Name:
Anonymous2014-06-26 16:45
>>26 The type systems that you mention can't even statically ensure that array indices are within bounds and that resources are disposed of correctly. So yes, they can catch only the most trivial "square peg in round hole" errors.
>>27 They can statically check that ACLs/credentials are enforced, statically check SQL queries, statically enforce taint checks and so on. Some type systems are turing complete, and can check anything that eventually does compile. You can do a lot of this in C, but then implicit coercion spoils everything.
Not all type systems can do static bounds-checking but dependent type systems can. Dependent types are halting equivalent in general, but I only need to concede the point if you can supply a useful program that is halting equivalent. It hasn't been done.
Hell, Xavier LeRoy wrote a verified C compiler with his Coq. From what I hear it admits no compiler bugs and won't emit code with UD.
Resource disposal is an odd complaint. C++ programmers and GC langs with poor type systems tend screw it up.
Theorem A: Units Testing catches all errors Static Typing does. Theorem B: Static Typing doesn't catch most of the errors Units Testing catches. Theorem C: Static Typing gets in the way, when you want to quickly prototype code and/or doesn't care if there are typing errors. ------ Corollary A: Static Typing is not a replacement for Unit Testing. Corollary B: Units Testing is a replacement for Static Typing. Corollary C: No reason bothering with Static Typing, when you have to do Unit Testing anyway.
If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable.
>>31 Defining 2 as S(S(0)) and 4 as S(S(S(S(0)))), where S is the successor function and addition is defined as usual in the Peano arithmetic, we can prove that 2 + 2 = 4.
I don't know why I even bothered replying to your post.
Programs are proofs, but only typed programs are useful proofs and only with regard to that which is expressed in types.
Tested programs can also be useful proofs, but testers aim for code coverage instead of spec and assumption coverage for some weird reason so they rarely ever prove anything useful.
>>47 Programs are programs, not proofs. Stop fucking doing this stupid shit. Next thing you're gonna say is that a computer is a homosexual nigger (you).
Name:
Anonymous2014-06-28 7:13
>>36 It's possible to keep it decidable, the only downside is requiring the programmer to declare types explicitly everywhere, which is a small price to pay for increased correctness guarantees.
Name:
Anonymous2014-06-28 7:49
>>48 You might not like the Curry-Howard correspondence, but it still exists.
It doesn't have anything to say anything about the GNAA, so I think maybe you have some things you need to work out.
Name:
Anonymous2014-06-28 10:48
>>46 DON'T MOCK KEINE SAFIKHDSFKLDJHADSJKLFHASDKJFHKASHFAJKDSFKDSA I FUCKING HATE YOU CRETIN DIE IN A FIRE
Name:
Anonymous2014-06-28 10:51
>>50 And it's still useless. What proofs are strcpy and memcpy equivalent to?
