5 ms·

A bit off topic, but I've been learning about languages like ML and Scala, and what does everybody have against static typing? I feel like if we used type syste

A bit off topic, but I've been learning about languages like ML and Scala, and what does everybody have against static typing? I feel like if we used type systems better, we'd have a lot fewer problems. You can prove that your programs have no bugs! That's much stronger than unit testing. When thinking 'static types', does everybody just think C/C++/Java? Is it upfront costs? My first ML program, I took half an hour to write a function that output all the words in a trie. It gets easier, and more interesting afterward, but I might have given up had it not been for a class. Are static types too rigid for prototyping? Scala, Haskell and OCaml have REPLs. Some of the "experimental features of static type systems" like dependent types are really powerful; you can make some strong proofs about the logic of your program. I'd be willing to give up (or at least try going without) duck typing for that.

papsosouid 14y ago
>what does everybody have against static typing? A lack of understanding. People get very upset when you say this, but I have yet to see a single person argue against static typing accurately. Every single argument (oh look, a bunch have been posted in reply to you even) I've seen has been based on exactly this fallacious reasoning: >When thinking 'static types', does everybody just think C/C++/Java? Yep. Including the people who write dynamically typed languages even: http://www.artima.com/intv/strongweak.html http://www.artima.com/intv/strongweak.html
jes5199 14y ago
Yeah, a lot of people's only experience with static types is C or Java. (A programming-language-theory PhD student friend-of-mine was first exposed to C while writing her dissertation. "This isn't a type system at all!" was the diagnosis) Also, sometimes in Haskell it's so hard to write a function that mostly-works (because they type system sees your mistake but you don't) that you can't get enough of your half-baked idea down so that you can see it clearly enough to figure out how it's supposed to really work correctly Also, I've seen plenty of programs that provably have no bugs, but still grow to exhaust all system memory or occasionally take several hours to return from a function call for no apparent reason. And those are a major pain to diagnose.
- papsosouid 14y ago
  >Also, I've seen plenty of programs that provably have no bugs, but still grow to exhaust all system memory or occasionally take several hours to return from a function call for no apparent reason I think you mean programs that type checked, not programs that provably had no bugs.
  - jes5199 14y ago
    What if those programs were guaranteed to do the right thing, if only that had enough time or space to finish? Maybe they're still "correct". Or, to put it another way: our existing type systems don't make code "provably correct", and when people say that it does (like the commenter above), they're trying to talk you into something.
    - papsosouid 14y ago
      >our existing type systems don't make code "provably correct" That is what I am telling you. >and when people say that it does (like the commenter above) They said no such thing.
      - jes5199 14y ago
        Yes, you're telling me something that I was already trying to demonstrate with my example.
        papsosouid 14y ago
        I can't speak to your motive, all I can do is read what you posted. What you posted was wrong, and I explained that.
        jes5199 14y ago
        What I posted was obviously self-contradictory, which is not the same as wrong.
brudgers 14y ago
I have a bowl. What types should it accept? Well certainly soup. And nuts. And everything in between. Plus washers and ball bearings and my son's head for haircuts. Solids, liquids and gasses need to implement the Bowlable interface. Just to be <type> safe, vacuums should probably implement Bowlable as well. I've got some classes to write and inheritance to track. Then all that's left is to implement Microwavable, Edible, Spoonable, and Unhealthy. Then I can enjoy my Maruchan Ramen. Bad things will happen if I put a can of Rustoleum in my Microwave and power it up on high for five minutes. So I'm not saying type safety doesn't matter. Just that it is not always better.
- pohl 14y ago
  Put pesticide in the bowl. Try to get soup out of the bowl. Feed to son. This old debate will rage on forever.
  - deleted 14y ago
    [deleted]
aidenn0 14y ago
People really don't like spending 6 hours trying to get something to compile. Compiling and running a possibly incorrect program that seems to work is more rewarding than trying to figure out how exactly it was that your compiler inferred a type different than you intended.
kd0amg 14y ago
Some of the "experimental features of static type systems" like dependent types are really powerful; you can make some strong proofs about the logic of your program. Yes, it is nice to be able to write proofs and have them checked mechanically. However, for nontrivial programs, even stating correctness (to a level of precision a proof checker can understand) is often very difficult. Once you've figured out how to do that, you still have to take the time to write the proof. There is also a cost associated with this capability even if you don't exercise it: dependent type systems (aside from things like Dependent ML, which restrict type indices to a much smaller language) tend not to play nicely with side effects like mutation, I/O, exceptions, nontermination, etc. So the proof system is not just something that's there for those times when you need it and fades away when you don't.

papsosouid 14y ago

>what does everybody have against static typing? A lack of understanding. People get very upset when you say this, but I have yet to see a single person argue against static typing accurately. Every single argument (oh look, a bunch have been posted in reply to you even) I've seen has been based on exactly this fallacious reasoning: >When thinking 'static types', does everybody just think C/C++/Java? Yep. Including the people who write dynamically typed languages even: http://www.artima.com/intv/strongweak.html http://www.artima.com/intv/strongweak.html

jes5199 14y ago

Yeah, a lot of people's only experience with static types is C or Java. (A programming-language-theory PhD student friend-of-mine was first exposed to C while writing her dissertation. "This isn't a type system at all!" was the diagnosis) Also, sometimes in Haskell it's so hard to write a function that mostly-works (because they type system sees your mistake but you don't) that you can't get enough of your half-baked idea down so that you can see it clearly enough to figure out how it's supposed to really work correctly Also, I've seen plenty of programs that provably have no bugs, but still grow to exhaust all system memory or occasionally take several hours to return from a function call for no apparent reason. And those are a major pain to diagnose.

papsosouid 14y ago
>Also, I've seen plenty of programs that provably have no bugs, but still grow to exhaust all system memory or occasionally take several hours to return from a function call for no apparent reason I think you mean programs that type checked, not programs that provably had no bugs.
- jes5199 14y ago
  What if those programs were guaranteed to do the right thing, if only that had enough time or space to finish? Maybe they're still "correct". Or, to put it another way: our existing type systems don't make code "provably correct", and when people say that it does (like the commenter above), they're trying to talk you into something.
  - papsosouid 14y ago
    >our existing type systems don't make code "provably correct" That is what I am telling you. >and when people say that it does (like the commenter above) They said no such thing.
    - jes5199 14y ago
      Yes, you're telling me something that I was already trying to demonstrate with my example.
      - papsosouid 14y ago
        I can't speak to your motive, all I can do is read what you posted. What you posted was wrong, and I explained that.
        jes5199 14y ago
        What I posted was obviously self-contradictory, which is not the same as wrong.

brudgers 14y ago

I have a bowl. What types should it accept? Well certainly soup. And nuts. And everything in between. Plus washers and ball bearings and my son's head for haircuts. Solids, liquids and gasses need to implement the Bowlable interface. Just to be <type> safe, vacuums should probably implement Bowlable as well. I've got some classes to write and inheritance to track. Then all that's left is to implement Microwavable, Edible, Spoonable, and Unhealthy. Then I can enjoy my Maruchan Ramen. Bad things will happen if I put a can of Rustoleum in my Microwave and power it up on high for five minutes. So I'm not saying type safety doesn't matter. Just that it is not always better.

pohl 14y ago
Put pesticide in the bowl. Try to get soup out of the bowl. Feed to son. This old debate will rage on forever.
- deleted 14y ago
  [deleted]

aidenn0 14y ago

People really don't like spending 6 hours trying to get something to compile. Compiling and running a possibly incorrect program that seems to work is more rewarding than trying to figure out how exactly it was that your compiler inferred a type different than you intended.

kd0amg 14y ago

Some of the "experimental features of static type systems" like dependent types are really powerful; you can make some strong proofs about the logic of your program. Yes, it is nice to be able to write proofs and have them checked mechanically. However, for nontrivial programs, even stating correctness (to a level of precision a proof checker can understand) is often very difficult. Once you've figured out how to do that, you still have to take the time to write the proof. There is also a cost associated with this capability even if you don't exercise it: dependent type systems (aside from things like Dependent ML, which restrict type indices to a much smaller language) tend not to play nicely with side effects like mutation, I/O, exceptions, nontermination, etc. So the proof system is not just something that's there for those times when you need it and fades away when you don't.