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

Re: The Anti-Human Consequences of Static Typing

#21

Post by cmhamill » Mon, Aug 12, 2013, 8:47 PM UTC

dustyleary wrote: post #7

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

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

Re: The Anti-Human Consequences of Static Typing

#22

Post by Someone » Mon, Aug 12, 2013, 8:48 PM UTC

themstheones wrote: post #11

grannyg00se wrote: post #2

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.

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 metho…

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.

Re: The Anti-Human Consequences of Static Typing

#23

Post by fournm » Mon, Aug 12, 2013, 8:48 PM UTC

majormajor wrote: post #18

themstheones wrote: post #11

Earlier quoted context omitted.

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 metho…

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…

Honestly, the code's probably changed enough since it was commented out to not be worth considering anymore (short of maybe leaving the comment, reworded, to explain what used to happen and why).

Large amounts (I regularly see 500+ lines in a single file) of commented out code is a huge smell and it would take an outstanding justification to get me to not delete it.

Re: The Anti-Human Consequences of Static Typing

#24

Post by pdonis » Mon, Aug 12, 2013, 8:50 PM UTC

grannyg00se wrote: post #9

kbenson wrote: post #6

Earlier quoted context omitted.

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 .

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.

Static typing stopped the compile because the program does something foolish.

But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to return either a string, say, or None, depending on whether it is able to find a string meeting some set of criteria, and you can't use the empty string as your "not found" value because empty strings are semantically significant for your application.) So static typing unnecessarily restricts the kinds of code you can write. That seems to me to be the article's basic point.

Re: The Anti-Human Consequences of Static Typing

#25

Post by zeidrich » Mon, Aug 12, 2013, 8:51 PM UTC

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.

Re: The Anti-Human Consequences of Static Typing

#26

Post by dragonwriter » Mon, Aug 12, 2013, 8:57 PM UTC

pdonis wrote: post #24

grannyg00se wrote: post #9

Earlier quoted context omitted.

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.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

> To take a simple example from Python, there are plenty of cases where you want a function to return either a string, say, or None, depending on whether it is able to find a string meeting some set of criteria, and you can't use the empty string as your "not found" value because empty strings are semantically significant for your application.

Static typing is not a problem here. Static type with an inadequate type system is a problem here,

Re: The Anti-Human Consequences of Static Typing

#27

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

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

Re: The Anti-Human Consequences of Static Typing

#28

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

pdonis wrote: post #24

grannyg00se wrote: post #9

Earlier quoted context omitted.

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.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

But most statically typed languages let you represent that kind of code. C++ and Java have null. Haskell has Maybe. It doesn't prevent you from writing the code, but rather requires you to be explicit about what values a variable can take, which is the purpose of having a type system at all.

Re: The Anti-Human Consequences of Static Typing

#29

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

pdonis wrote: post #24

grannyg00se wrote: post #9

Earlier quoted context omitted.

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.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

Except most type systems can deal with that -- if you truly believe that mixing types isn't foolish in a particular case, just tell the compiler that you're doing it intentionally. The OP's example is trivially solved by using the Either type within the if statement to denote that the expression intentionally returns two different types. The compiler will then check for you that you actually deal with both cases. Better yet, one of the type constructors for Either is traditionally reserved as an error case, so it again correctly flags the code as always branching in the same direction barring an exceptional case.

Your Python example is a canonical use case for the Maybe/Option type. You either provide "Just" a value, or you provide "Nothing".

The point is, a type system of sufficient power can express your program just fine so long as you declare to the type checker that you're not just making a silly mistake. And let's be honest, we all make tons of those mistakes. Who wants them hiding for some unknown duration to crop up at the most unfortunate time. I'd rather know asap that my program has a problem.

Re: The Anti-Human Consequences of Static Typing

#30

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

pdonis wrote: post #24

grannyg00se wrote: post #9

Earlier quoted context omitted.

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.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

Statically typed mainstream languages would not allow you to do that, but languages with algebraic type systems, like Haskell, Scala and Rust, do. This is also how they get around not having null pointers. You just define a type that can be either a string, or the symbol "None". Or any other symbol that might be more fitting for the situation.