The Anti-Human Consequences of Static Typing • Hacker News Board

Re: The Anti-Human Consequences of Static Typing

#31

Post by npsimons » Mon, Aug 12, 2013, 9:07 PM UTC

Permit wrote: post #20

>The logic goes that if you reject "bad" programs then only "good" programs remain, and who would want to run "bad" programs anyways? I thought the logic was: if you reject all bad programs and some good programs, only good programs remain, is it not?

This article appears to me to failing in being entirely cogent; his example of the if that returns a number or a string seems nonsensical, and therefore "bad" by some definitions, which also points out that bad is subjective.

That being said, perhaps it would have been a better article if the author presented some arguments of "bad" programs that pass the type system, as type systems are no silver bullet and do not guarantee rejection of all bad programs.

Re: The Anti-Human Consequences of Static Typing

#32

Post by terhechte » Mon, Aug 12, 2013, 9:07 PM UTC

Funny coincidence, just today I wondered if there's such a thing as a statically typed Lisp, and stumbled upon Racket with types [1]

I think another good example of a optionally static typed language would be Julia, where you can add types, and if you add them, the compiler will try to leverage that information to optimize your code [2].

I've used dynamic and static languages mixed for most of my life (Javascript, Python, PHP back in the early 2000's VS. C and Objective-C). Recently I started working with Scala, which has much stricter typing than, say, Objective-C, and I have to admit that after a bit of early helplessness in the beginning, it feels strangely liberating that, once the code compiles, the program is solid. Successful compilation brings with it a sort of satisfaction.

[1] http://docs.racket-lang.org/ts-guide/ [2] http://docs.julialang.org/en/release-0.1-0/manual/types/

Re: The Anti-Human Consequences of Static Typing

#33

Post by jongraehl » Mon, Aug 12, 2013, 9:07 PM UTC

Dumb. Mangles Godel.

The premise is that for real world inputs some code may never be used, and so it's an advantage for late-checked types that you can have wrong code that will never cause any observed bug. I'd rather "waste" my time deleting nonsense code after it fails an early type-check. Less code = better reading/maintenance/extension.

Better to focus on the real advantages of single-type languages (usually, terser programs, although type inference can make some haskell/ML programs apparently type-less).

Re: The Anti-Human Consequences of Static Typing

#34

Post by jeapostrophe » Mon, Aug 12, 2013, 9:08 PM UTC

freyrs3 wrote: post #27

> Theorems and conclude that in every logic there are statements which are true, but not provable, or provable, but not true. And this is the ultimate problem with type systems: in their quest to reject "bad" programs, they must reject "good" programs as well because they cannot prove their "goodness". This really is a gross misuse of Gödel's theorem. Taken to it's logical end his argument is that any field that has…

We should not throw out mathematics, but we should recognize that most mathematical proofs are not based on logic, but human intuition in the first place. Human intuition and wisdom are valuable and lay the foundation for all that we do and there's no reason to ignore them when we're programming and insist that all valid programs have to follow some particular set of rules.

Re: The Anti-Human Consequences of Static Typing

#35

Post by jfb » Mon, Aug 12, 2013, 9:09 PM UTC

zeidrich wrote: post #25

I agree, we need to have far more human compilers. Perhaps, when I compiler runs across a type violation it just breaks out laughing at you. "HA HA HA! You idiot! You defined this variable as a string, and then you tried to do arithmetic on it, WHAT WERE YOU THINKING?" Maybe the compiler can just complain about the user. "Seriously, this guy first gets me to make this integer, and that's cool, but then he starts to u…

"I don't know, you asked me to divide that integer by this string. What am I supposed to do?"

Re: The Anti-Human Consequences of Static Typing

#36

Post by noodly » Mon, Aug 12, 2013, 9:10 PM UTC

I like the ending: "Please enable JavaScript to view the comments powered by Disqus." ;)

I know that the strengths of racket lie elsewhere, but I wish the performance would be better (at least comparable with sbcl) ;)

As for dynamic vs static typing - I don't care much about human rights, so I prefer static typing :D

Dynamic typing (and laziness) is good when you don't have to care about memory footprint nor performance of code you write e.g. when you're prototyping something.

Re: The Anti-Human Consequences of Static Typing

#37

Post by jobeirne » Mon, Aug 12, 2013, 9:12 PM UTC

> A static type system is a mechanism whereby an algorithm determines if a program exhibits a property, P, and if the property is not found to hold, then the program is rejected.

Doesn't this definition encompass dynamically typed languages as well? e.g. P is syntactic validity?

Re: The Anti-Human Consequences of Static Typing

#38

Post by freyrs3 » Mon, Aug 12, 2013, 9:15 PM UTC

jeapostrophe wrote: post #34

freyrs3 wrote: post #27

> Theorems and conclude that in every logic there are statements which are true, but not provable, or provable, but not true. And this is the ultimate problem with type systems: in their quest to reject "bad" programs, they must reject "good" programs as well because they cannot prove their "goodness". This really is a gross misuse of Gödel's theorem. Taken to it's logical end his argument is that any field that has…

We should not throw out mathematics, but we should recognize that most mathematical proofs are not based on logic, but human intuition in the first place. Human intuition and wisdom are valuable and lay the foundation for all that we do and there's no reason to ignore them when we're programming and insist that all valid programs have to follow some particular set of rules.

> mathematical proofs are not based on logic

Mathematical proofs are explicitly logical statements, if they aren't based in logic they aren't proofs by definition. Mathematical intuition is what leads us to ideas but it's only within the framework of formal reasoning that we "know" anything within mathematics. Poincare said it nicely:

"It is by logic we prove, it is by intuition that we invent."

Re: The Anti-Human Consequences of Static Typing

#39

Post by jeapostrophe » Mon, Aug 12, 2013, 9:16 PM UTC

freyrs3 wrote: post #38

jeapostrophe wrote: post #34

Earlier quoted context omitted.

We should not throw out mathematics, but we should recognize that most mathematical proofs are not based on logic, but human intuition in the first place. Human intuition and wisdom are valuable and lay the foundation for all that we do and there's no reason to ignore them when we're programming and insist that all valid programs have to follow some particular set of rules.

> mathematical proofs are not based on logic Mathematical proofs are explicitly logical statements, if they aren't based in logic they aren't proofs by definition. Mathematical intuition is what leads us to ideas but it's only within the framework of formal reasoning that we "know" anything within mathematics. Poincare said it nicely: "It is by logic we prove, it is by intuition that we invent."

If you really believe this, you should try to translate any contemporary (published) mathematical proof into a real logic, like Coq. It is hard and people earn PhDs doing this because most proofs are so intuition heavy in the first place.

Re: The Anti-Human Consequences of Static Typing

#40

Post by jeapostrophe » Mon, Aug 12, 2013, 9:18 PM UTC

jobeirne wrote: post #37

> A static type system is a mechanism whereby an algorithm determines if a program exhibits a property, P, and if the property is not found to hold, then the program is rejected. Doesn't this definition encompass dynamically typed languages as well? e.g. P is syntactic validity?

Syntactic validity is not a property of a program, but a property of a piece of text that makes it a program. In any case, the point is that type systems purport to identify some amount of "goodness" in a program. I agree that "The compiler will produce something" is a property, although I doubt it is a property any static type proponent would defend as particularly important.