The Anti-Human Consequences of Static Typing

http://jeapostrophe.github.io/2013-08-12-types-post.html

by nickmain • 13 years ago

43 63 13 years ago

jeapostrophe.github.io

grannyg00se2• 13 years ago

The first example of a "good" program contains an if statement that should only ever branch in one direction.

I question whether that is a "good" program.

kbenson2• 13 years ago

It's only good in that with the dual dichotomies he has defined as what the static typing compiler accepts and rejects and what will function or not function, it functions but may not compile.

grannyg00se2• 13 years ago

But he's presenting it as a bad thing that the program doesn't compile. Static typing stopped the compile because the program does something foolish. That's a win.

themstheones2• 13 years ago

There are only four options for removing a block of code you no longer want to use:

1. Add a comment around the whole block. This may not always work, as comments within the block may need to be removed.

2. Add string delimiters before and after the block, making the block an in-place string literal. This can be broken by strings within the block.

3. Use a goto statement to skip the block. This is a pretty good method but you have to worry about the label getting moved, and fellow developers laughing at you for using goto.

4. Wrap the block with a big if (false) { }. This is the most bullet proof method, but it violates your goodness criteria.

majormajor• 13 years ago

Delete it and refer to your version control system's history if you need to bring it back?

Edited addition to reduce the snarkiness a bit: if I see a block of dead code like that left in a file, regardless of which way it's been killed, I'm going to consider that bad unless there's a very clear comment explaining why this isn't needed anymore but was worth leaving in the code instead of fully deleting it. But if that comment's there, and the reason makes sense, it's still breaking the "rule" but becomes an example of knowing when to break the rule.

Someone2• 13 years ago

5) delete it from your code. You do have source control, so you will be able to recover the code later. If you want to leave evidence, add a comment:

  -- Removed Foo handling in revision ... because of ...

That should be rare, though.

For temporary disabling, I tend to do:

   const disableFooForDebugging = true
   if( disableFooForDebugging)

That makes it easier to recognize and correct accidental checkins.

chipsy• 13 years ago

I don't think I've ever seen someone use such gleefully religious rhetoric to advocate dynamic types before.

gngeal• 13 years ago

When was this a non-religious issue? But I believe the problem is following: Either the type system is incomplete (there are programs out there that you might want to run but won't be able to), or it's unsound (some programs will get a pass the type checker but fail at run time), or the type system will be so complex as to being undecidable. Since people generally aren't happy with number one, you either have to rely on the programmer (number two) or force everything to pass through a potentially loopy process every time you compile something (number three)

Ot, one might go the Qi/Shen route...

dubbledidu• 13 years ago

Me too. This and all those Go fanboys make me really embarrassed of my profession.

ExpiredLink• 13 years ago

This is science. It must be true.

dustyleary• 13 years ago

In the final analysis, we may appeal to the Gödel Incompleteness Theorems and conclude that in every logic there are statements which are true, but not provable, or provable, but not true.

Is this wrong?

"true but not provable" is easy.

What is an example of a statement that is "provable but not true"?

jeapostrophe8• 13 years ago

It's true. The theorems are a statement about the logics. Most of the time when you design a logic, you get to "choose" which case you'll get. Most people choose "true but not provable" because that's a little useful. It would be very bad to choose "provable but not true", because then you could never trust any conclusions of the proof system. - the author

freyrs34• 13 years ago

Poorly worded, and a bit disingenuous to bring Gödel's theorem in this context. Taken to it's logical conclusion, by his argument we shouldn't bother analyzing the properties of programs at all.

cmhamill• 13 years ago

"Provable but not true" statements only arise in logical systems which are inconsistent, so it's fairly normal to not be able to come up with one.

So you need to assume two contradictory things are true, somewhere deep down in your logical system. As a trivial example, assume that both the following are true:

1. I am a robot. 2. I am not a robot.

And our false statement which we are going to prove is:

Pizza is made of fear.

We know that the following proposition is true:

I am a robot OR pizza is made of fear

Because we know that I am not a robot, the first term in the above must be false, and so the second term must be true. Therefore, pizza is made of fear.

That's really more an example of the principle of explosion, but the above is a tiny logical system which contains statements that are provable, but not true.

In practice, we tend to use logical systems which can't prove all true statements, but don't let you prove false ones. Much more useful, really.

finnw• 13 years ago

Other more quaint languages like Java may have type systems that check properties such as "The program does not add numbers and strings"

Poor example. In Java, number + string means "convert the number to a decimal string then concatenate", and it can be invoked unintentionally.

jeapostrophe8• 13 years ago

That's not a counter-example. I'm not saying that Java doesn't allow syntax that might look like "number + string", just that it does not actually add them, like C does where: 3 + "4" means something very surprising.

Someone2• 13 years ago

Does it? I thought string + number does that, but number + string does not compile.

Kliment2• 13 years ago

Are there any languages that have a type mismatch warning rather than a type mismatch error? Something like how gcc warns about incompatible pointer types when compiling C programs, but lets you use them if you insist, but for all types?

jeapostrophe8• 13 years ago

I suggest reading about progressive types:

http://blog.brownplt.org/2012/09/01/progressive-types.html

Kliment2• 13 years ago

Wow, thank you, that is exactly what I had in mind

enupten• 13 years ago

A few implementations of Common-Lisp (like SBCL) do this already (not surprisingly), and I find it very useful to compile misbehaving programs (and having not being segfaulted upon). Once you verify function behavior with a bunch of test cases, you declare types everywhere in the code and set the compiler optimization to full.

strager• 13 years ago

GHC (a Haskell compiler) can defer type errors until runtime:

http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime

http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/defer...

fournm2• 13 years ago

I'm at a loss when it comes to considering something with dead code or a potentially unexpected return type to be good code, especially in something statically typed...

Permit• 13 years ago

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?

npsimons• 13 years ago

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.

dragonwriter2• 13 years ago

I think the logic actually goes "if you reject upfront all programs with a certain type of badness as well as some programs that falsely appear to have that type of badness, you will reduce the costs associated with bad programs by catching many of them sooner, at the cost of having to rewrite some already-good programs in less-simple ways to avoid the appearance of badness."

jeapostrophe8• 13 years ago

Let's put that on a bumper sticker :)

zeidrich• 13 years ago

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 use it like it was a float, so you know, I gotta go and rearrange ALL the bits. Then you know what he does, he goes and takes another integer and tries to math them together. Screw that guy. But you want to know the kicker? After all of this, he casts it back to an int and then tries to append a string. Seriously. Make up your mind. I need a beer. What do you think I am, Javascript?"

Maybe the compiler just gets angry. "You know what? First you claim it's this structure, then you treat it like that structure. Whatever, I say it's crap. I'm deleting it. Write it again, and make sense this time."

I prefer my computers less human.

jfb• 13 years ago

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

bitwize2• 13 years ago

a typedef name was a complete surprise to me at this point in your program

freyrs34• 13 years ago

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 logical foundations should value human judgement over rigor and proof because of incompleteness. Should we just throw out all of mathematics as well because there are true but unprovable theorems?

jeapostrophe8• 13 years ago

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.

freyrs34• 13 years ago

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

terhechte• 13 years ago

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/

jongraehl• 13 years ago

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

noodly• 13 years ago

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.

jobeirne• 13 years ago

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?

jeapostrophe8• 13 years ago

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.

bitwize2• 13 years ago

Static typing is pro-human; I would call it even more humane than dynamic typing.

Vastly more type errors (i.e., conditions which cause the program not to hold the property checked by the type system) are caused by programmer error than by deliberate design; a strong, static type system, checked at compile time, helps ensure that a whole class of relatively weak but trivially easy to write bugs do not find their way into the finished program. The programmer hours saved in not having to worry that some little-exercised code path will attempt to add an integer to a string, nor to write exhaustive tests covering every possible code path to make sure no integers get added to strings, adds up significantly over the program's lifecycle, from initial development through maintenance and support.

Be kind to your programmers. Use a statically-typed language.

mahyarm• 13 years ago

I mostly agree, but having the ability to use a dynamic type occasionally can be very useful. I like how objective-c handles it in practice.

hcarvalhoalves• 13 years ago

(+ 1 (if (negative? (fahrenheit->kelvin (abs some-number))) "2" 2))

This is inconsistent code to being with, though. You can't guarantee it "never" reaches the first branch, as much as you can't guarantee there aren't bugs in the conversion function, or on the underlying interpreter, or that machine details wouldn't make a big enough number wrap around and return negative. All in all, an inconsistent code branch hanging around is a bug even if it compiles.

This is more an evidence that "if" is evil rather than an argument about typing, really.

The Anti-Human Consequences of Static Typing

Related Stories