7 ms·

The Anti-Human Consequences of Static Typing

43 points by nickmain 13y ago

grannyg00se 13y 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.
- kbenson 13y 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.
  - grannyg00se 13y 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.
    - pdonis 13y ago
      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.
      - dragonwriter 13y ago
        > 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,
        kbenson 13y ago
        And that's the whole point of his post. Don't let strict adherence from static typing overshadow interesting new techniques from being developed when we don't use static typing. We can then go back and update our type models to allow that new usage. The first comment on the article (bottom of the list of comments) clarifies his purpose.
      - pogden 13y ago
        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.
        pdonis 13y ago
        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. It's the purpose of having a static type system, yes. But the drawback is that you have to be explicit; you don't have a choice. There are situations where that is indeed a drawback; see my other posts in this thread.
      - acomar 13y ago
        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.
- themstheones 13y 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 13y 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.
    - fournm 13y ago
      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.
  - Someone 13y 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 13y ago
I don't think I've ever seen someone use such gleefully religious rhetoric to advocate dynamic types before.
- gngeal 13y 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 13y ago
  Me too. This and all those Go fanboys make me really embarrassed of my profession.
ExpiredLink 13y ago
This is science. It must be true.
deleted 13y ago
[deleted]
dustyleary 13y 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"?
- jeapostrophe 13y 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
- freyrs3 13y 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 13y 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 13y 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.
- jeapostrophe 13y 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.
- Someone 13y ago
  Does it? I thought string + number does that, but number + string does not compile.
Kliment 13y 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?
- jeapostrophe 13y ago
  I suggest reading about progressive types: http://blog.brownplt.org/2012/09/01/progressive-types.html http://blog.brownplt.org/2012/09/01/progressive-types.html
  - Kliment 13y ago
    Wow, thank you, that is exactly what I had in mind
- enupten 13y 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 13y ago
  GHC (a Haskell compiler) can defer type errors until runtime: http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/defer-type-errors.html http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/defer...
fournm 13y 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 13y 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 13y 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.
- dragonwriter 13y 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."
  - jeapostrophe 13y ago
    Let's put that on a bumper sticker :)
zeidrich 13y 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 13y ago
  "I don't know, you asked me to divide that integer by this string. What am I supposed to do?"
- bitwize 13y ago
  a typedef name was a complete surprise to me at this point in your program
freyrs3 13y 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?
- jeapostrophe 13y 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.
  - freyrs3 13y 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."
    - jeapostrophe 13y ago
      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.
      - freyrs3 13y ago
terhechte 13y 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/ http://docs.racket-lang.org/ts-guide/ [2] http://docs.julialang.org/en/release-0.1-0/manual/types/ http://docs.julialang.org/en/release-0.1-0/manual/types/
- deleted 13y ago
  [deleted]
jongraehl 13y 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 13y 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 13y 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?
- jeapostrophe 13y 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.
bitwize 13y 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 13y 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.
pasquinelli 13y ago
"Advocates for static typing are anti-human, because they argue that the only programs we should allow to run are the ones that have been verified by machines! In contrast, the freedom fighters contra to these typing terrorists argue that humans can perform analysis and decision making as well!" humans suck at verifying programs. let's keep going with this, why do we only consider a program to be running when it's running on a machine!? humans can run programs as well!
hcarvalhoalves 13y 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.

43 points by nickmain 13y 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.

kbenson 13y 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.
- grannyg00se 13y 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.
  - pdonis 13y ago
    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.
    - dragonwriter 13y ago
      > 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,
      - kbenson 13y ago
        And that's the whole point of his post. Don't let strict adherence from static typing overshadow interesting new techniques from being developed when we don't use static typing. We can then go back and update our type models to allow that new usage. The first comment on the article (bottom of the list of comments) clarifies his purpose.
    - pogden 13y ago
      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.
      - pdonis 13y ago
        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. It's the purpose of having a static type system, yes. But the drawback is that you have to be explicit; you don't have a choice. There are situations where that is indeed a drawback; see my other posts in this thread.
    - acomar 13y ago
      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.
themstheones 13y 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 13y 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.
  - fournm 13y ago
    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.
- Someone 13y 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 13y ago

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

gngeal 13y 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 13y ago
Me too. This and all those Go fanboys make me really embarrassed of my profession.

ExpiredLink 13y ago

This is science. It must be true.

deleted 13y ago

[deleted]

dustyleary 13y 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"?

jeapostrophe 13y 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
freyrs3 13y 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 13y 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 13y 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.

jeapostrophe 13y 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.
Someone 13y ago
Does it? I thought string + number does that, but number + string does not compile.

Kliment 13y 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?

jeapostrophe 13y ago
I suggest reading about progressive types: http://blog.brownplt.org/2012/09/01/progressive-types.html http://blog.brownplt.org/2012/09/01/progressive-types.html
- Kliment 13y ago
  Wow, thank you, that is exactly what I had in mind
enupten 13y 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 13y ago
GHC (a Haskell compiler) can defer type errors until runtime: http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/defer-type-errors.html http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/defer...

fournm 13y 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 13y 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 13y 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.
dragonwriter 13y 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."
- jeapostrophe 13y ago
  Let's put that on a bumper sticker :)

zeidrich 13y 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 13y ago
"I don't know, you asked me to divide that integer by this string. What am I supposed to do?"
bitwize 13y ago
a typedef name was a complete surprise to me at this point in your program

freyrs3 13y 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?

jeapostrophe 13y 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.
- freyrs3 13y 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."
  - jeapostrophe 13y ago
    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.
    - freyrs3 13y ago

terhechte 13y 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/ http://docs.racket-lang.org/ts-guide/ [2] http://docs.julialang.org/en/release-0.1-0/manual/types/ http://docs.julialang.org/en/release-0.1-0/manual/types/

deleted 13y ago
[deleted]

jongraehl 13y 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 13y 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 13y 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?

jeapostrophe 13y 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.

bitwize 13y 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 13y 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.

pasquinelli 13y ago

"Advocates for static typing are anti-human, because they argue that the only programs we should allow to run are the ones that have been verified by machines! In contrast, the freedom fighters contra to these typing terrorists argue that humans can perform analysis and decision making as well!" humans suck at verifying programs. let's keep going with this, why do we only consider a program to be running when it's running on a machine!? humans can run programs as well!

hcarvalhoalves 13y 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.