7 ms·

Static Typing is not enough

• carsongross 14y ago
  Neither static typing (nor any of the other stuff mentioned) is enough to ensure correctness. Never has been, never will be. However, static typing is enough for some sweet, sweet hit-dot-wtf-can-i-do-completion-refactoring-like-a-boss tooling goodness.
  • fogus 14y ago
    (any of the other stuff mentioned) .. ensure correctness The post says that. Dot-completion in your IDE is not enough either, nor is it something particularly unique to static languages.
    • roryokane 14y ago
      > The post says that. I think the grandparent knew that, and was just repeating what you said to contrast it with his following statement about what static typing is good for. And dot-completion is not completely unique to static languages, but I would say it is “particularly unique” – it is more common for static languages. And that’s not just coincidence – it is generally easier to write a tool like dot-completion for a static language than a dynamic language, because dot-completion involves static analysis of the code.
      • derefr 14y ago
        > dot-completion involves static analysis of the code. Dot-completion involves having a living model of the program loaded in memory. You can do this with any language--static languages just partition the program model such that you get a certain phase of interpretation (compilation) past which you have a completed model of all of the code, without yet having seen any of the data. On the other hand, you can easily dot-complete method calls in a dynamic language's REPL--because there, at runtime, is when and where a dynamic language forms a complete model of the program it can use to do such things. Now, the real question is why we're still programming dynamic languages in text-editors instead of treating them as congealments of transactionally-replayable interactive REPL transcripts. (Are there any modern examples of programming in this style, anyway? I can only think of ancient ones: Emacs Lisp, Squeak Smalltalk, and the "immediate-command-line" of some Telnet-based simulated-world MOOs.)
        • carsongross 14y ago
          I code in both ruby (with a repl in the IDE) and java (with a traditional statically typed IDE). There are times I wish I had a repl in java (I typically use debugging in a test to fake it) but I'd give my left cortex for reliable code completion in ruby. There's no reason we can't have both. It just takes a reasonable terse statically typed language like C# or, dare I say... gosu.
          • jshen 14y ago
            Have you tried pry for ruby?
        • prodigal_erik 14y ago
          When you create a method which takes an argument in a dynamic language, there's no declaration of the type of that argument or which methods it will be known to support. So how does dot-completion work for any target other than "this"? The REPL isn't doing whole-program dataflow analysis to infer the only type(s) which could possibly be passed, is it?
          • jules 14y ago
            FYI, PyTools for Visual Studio does dataflow analysis for intellisense.
    • carsongross 14y ago
      Reliable dot completion without some batshit insane state-dependent VM-as-a-dev-env-or-constantly-running-tests system is... well, let's just say made much easier with static typing. I really could give a shit about what people think is "enough" (IMO, keeping stuff simple, as in simplicity of implementation, as in worse-is-better, is the only answer) I just want to hit dot and have a pretty good idea what I'm allowed to do. And static typing, in practice, appears to help there. But hey, man, I'm not advocating you use it.
      • fogus 14y ago
        But hey, man, I'm not advocating you use it. I'd be crazy to give up dot completion. I like it as much as the next guy. ;-)
      • jshen 14y ago
        Pry for ruby gives me great dot completion and isn't batshit insane. Most diehard dynamic typists live in their repl. When I use java with IntelliJ I miss my repl. I do gain some things from the IDE, but I feel hamstrung compared to my repl.
        • carsongross 14y ago
          I'll give pry a try, but I've tried a lot of dynamic IDE environments and none have come close to IJ w/ statically typed langs.
          • jshen 14y ago
            Minus the part about t only working well for java and having to write your code in java ;) I also use rubymine for ruby development and it gives me a lot of the IntelliJ stuff, but it doesn't always work. I.e cmd-b to jump to the method definition.
        • carsongross 14y ago
          Ah, fk man, another REPL? I don't want a repl for editing. I want to write code in a friggen editor and have dot completion work. I also want a repl for trying stuff out and debugging/light weight testing, but that's a different use case for me.
• tomp 14y ago
  Sometimes, I wish I could downvote stories... Accidentially, almost everything that the author suggests, except luck and user testing, can be provided by static type systems - e.g. Haskell's type system is Turing-complete, so you can make up any kind of contracts/tests and embed them into the type system...
  • jerf 14y ago
    With appropriate compiler flags, you can make up any sort of contracts you like in Haskell. But there's no guarantee that the compilation process will terminate if you do, even putting aside the impenetrability of the resulting code. Haskell is not a general purpose proof assistant, and the typing definitely has limits both practical and theoretical. Abstractly, static types can represent anything, however we (by which I mean humanity in general) certainly do not know how to use such powerful types in real, general purpose code. If you want to go that road, look up Agda or Coq.
    • prodigal_erik 14y ago
      Why do people worry about compilers hanging or giving up? If I know how to kill the failed compile and fix my program so that it is provably type-safe before shipping, I don't really care how many undecidable programs could also exist because I no longer have to ship one of those.
      • jerf 14y ago
        Because if the compiler hangs, you don't get any executable code. And in the specific case of Haskell, we are talking about type constraints that are perfectly cromulent, are perfectly correctly expressed and mean something in some abstract mathematical world in which your have infinite compiler time, but in the real world will simply never finish compiling. It's not because you've failed and you can fix it by twiddling something, it's because Haskell is not actually that sort of language, and if you try to actually use the type system as a Turing-complete constraints satisfaction language, you'll get exponential performance... or doubly-exponential performance, or worse, though it stops mattering pretty quickly. In both theory and practice, this means you can't really use Haskell that way. It's a typed language with the ability to occasionally skirt the limits, ride the line, and dip into a bit of undecidability when useful (and with a real, in-practice risk of it blowing up in your face even so), not a language in which one routinely uses the type system in a "Turing complete manner", if I may be allowed to gloss over precisely what that means. Richer type systems is a topic of ongoing research, but is not a solved problem.
• chipsy 14y ago
  This is as much a usability problem as it is a "getting it right" one. We could eventually "get it right" by plugging in raw machine code through switches or punchcards if that's really what it took, but what we're arguing over is the _price_ of getting it right. Static types are implemented and available for use at the language level, which isn't true of all of those features in most environments.
• saraid216 14y ago
  LDD ftw.
• ternaryoperator 14y ago
  Kind of a strawman argument, as no developer would argue that only unit tests and static typing are needed to guarantee quality.
  • lmm 14y ago
    It's a response to a previous article, which really did make the argument "unit testing does not guarantee quality, therefore you need static typing". So not a strawman.
    • skew 14y ago
      The previous article really didn't make the argument "all you need is static typing". It was specifically refuting the idea that "all you need is unit testing" - or at least that unit testing is a complete replacement for static types. The paper makes a point of reporting that most unit tests could not be replaced by static types. What of that looks like a claim that you only need types?
      • ajanuary 14y ago
        The previous article said "unit testing isn't enough, you need static types /as well/". This article is extending that argument to "unit testing and static types aren't enough, you need xyz /as well/". I believe the point is that there will always be something your current test strategy doesn't cover. At what point do you draw the line? If unit tests and static types don't cover everything, what says that's enough? And can the justification for that, whatever it is, be applied to "unit tests are enough" also?
• modarts 14y ago
  Yet another attempt to diminish the value of statically typed languages and the benefits that go along with them.
  • fogus 14y ago
    I'm question if you read the post because I didn't diminish anything. I did say that it is a tool in the fight of software validation however.
    • modarts 14y ago
      The undertone was pretty clear.
    • jdeseno 14y ago
      It seems to be a trend; gloss over the article then infer most of the meaning from the title. The title I submitted isn't great but, I can't seem to correct it.
  • soc88 14y ago
    Yes, exactly. The author didn't like the original article and decided to throw around some strawmen.
    • fogus 14y ago
      I disliked it so much that I called it "excellent".
• gbog 14y ago
  In a conference 15 years ago I heard a guy say The problem with software is we don't know what it is. He meant that: we know what is a car or a bridge, we know why and how they do their purpose, not so much with software, which is a strange beast our minds are not ready to grab yet.
  • morsch 14y ago
    There might be something to that. But maybe some construction and automobile engineers feel the same way about bridges and cars respectively. God, I hope not. :)
• tikhonj 14y ago
  Yes, static typing is not enough. Which is why a good statically typed language like Haskell also has great testing facilities. So you don't just write well typed code, but you also write unit tests (HUnit) and property-based tests (QuickCheck). The really neat bit is that static typing actually makes writing tests easier--QuickCheck is much easier to use in Haskell than it would be in some dynamically typed language.
  • Dn_Ab 14y ago
    QuickCheck is great and can be found in many languages - dynamic and static alike - nowadays. Another tool that is currently unique to Haskell and is easier to write tests for is Lazy/SmallCheck. SmallCheck shines in the left long tail of failure. Its core idea is based on a powerful principle: "If a program does not fail in any simple case, it hardly ever fails in any case."[] So SmallCheck works exhaustively to find a minimal counterexample within some depth bound. This makes sense - when trying to characterize a structure for failure (or anything) you can rarely do better than the simplest explanation. However, when the problem lies in larger examples SmallCheck fails where QuickCheck catches a result so something like Type Check -> SmallCheck -> QuickCheck -> probably ok. [] http://www.cs.york.ac.uk/fp/smallcheck/ http://www.cs.york.ac.uk/fp/smallcheck/ documentation
    • gtani 14y ago
      and the guarantees (both random and exhaustive testing) for GenCheck http://permalink.gmane.org/gmane.comp.lang.haskell.general/19371 http://permalink.gmane.org/gmane.comp.lang.haskell.general/1...
    • tikhonj 14y ago
      Quickcheck exists in a bunch of different languages, but Haskell's type system makes it easier to use and implement because it can rely on type information to figure out which generator to use for any given input.
• chj 14y ago
  Big take away: Love Driven Development Rules Them All.
• deleted 14y ago
  [deleted]
• nightski 14y ago
  Doesn't anyone view static typing as done in a language like Haskell as a form of documentation? I am not saying ALL Haskell code can be deciphered by its types - hell no. But a useful technique is to express the semantics of the program into the type system (as much as possible anyways) to communicate intent. This is a huge benefit over dynamic languages imho. So there is more too it than just verification, even if that is extremely nice.
  • tikhonj 14y ago
    This is actually a rather underrated property of good static type systems. Some types (like (a, b) -> a or a -> b -> a) are actually so constraining, they can only have one valid (e.g. not ⊥) implementation. There is actually a program that, given a type signature, can write the trivial function for you [1]. It's pretty awesome, but admittedly more a curio than anything practical. [1]: http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178 Happily, there are practical programs that take advantage of the types' expressiveness. My favorite example: Hoogle[2]. It's brilliant: a search engine that given a type signature gives you a list of functions either with that type (modulo renaming) or a similar type. The beauty is that it can work even if the function is more general than what you're looking for and has a weird name (so a normal search would not be very helpful). [2]: http://www.haskell.org/hoogle/ http://www.haskell.org/hoogle/ A perfect example: let's say you're looking for the equivalent of JavaScript's join method. It would have the type [String] -> String -> String. Now, this particular function does not actually exist in Haskell. Instead, there is a more general function called intercalate that works on any list. Moreover, intercalate's arguments are reversed: it's type is actually [a] -> [[a]] -> [a] (or String -> [String] -> String if made specific to String). And yet, if you search for [String] -> String -> String, the second result is intercalate! It's magical. In short: types are basically a form of self-documenting code, so you get a lot of cool stuff for free given a good type system.
  • stonemetal 14y ago
    In some way yes, but in general not really. (+),(-), (*) all have the type (Num a) a -> a -> a abs, signum both have the type (Num a) a-> a In the first case it works as documentation because I already know what they do. In the second case I read signum as sig num instead of sign num, and was left scratching my head as to what a signature number was, until I read the actual documentation. So I would say types make a good reference documentation but not a good learning documentation. Contrast this with python doc strings which can be both a good reference and a decent source of learning.
• cageface 14y ago
  Yep, there is no silver bullet. But that doesn't mean all bullets are created equal.
  • marknutter 14y ago
    Yes, but perhaps we it means we can stop bitching about each other's bullets of choice and get back to shooting.
    • cageface 14y ago
      I've got no time for bitching but I think serious attempts to study the pros and cons of different approaches are both welcome and needed in our profession.
      • marknutter 14y ago
        I'm indifferent, frankly. I think it's valuable to know the pros and cons of different approaches, but most of the time discussion around degrades into unproductive flame wars. It's understandable, though. Dedicating years to becoming good at one approach over another will make you defensive.
    • tikhonj 14y ago
      That would be great if I could just work by myself, happily use Haskell and not worry about bosses mandating something really annoying like Python or Java. In fact, that's one of the main reasons I'm working at a tiny startup right now. But I digress; my main point is simple: since chances are your choice of bullet affects others' choices, especially in corporate settings, it would be much better if it were a good choice.
      • marknutter 14y ago
        And "good choice" remains subjective. Round and round we go. Somebody stop this thing before I puke.
• qznc 14y ago
  You need formal machine-checked verification (Coq, Isabelle). Unfortunately, this is not enough. You need a consistent and complete specification, too.
  • skew 14y ago
    The first half is a bit easier - if you can show some implementation meets the specification it is at least consistent. The second isn't so clear, but sometimes you can get a bit more confidence by showing that other good properties are implied by the specification alone.
• buster 14y ago
  Doesn't matter because, what really matters is Think-before-you-code, all that static typing will save noone from bugs. Also: <3 Love Driven Development <3
• cpfohl 14y ago
  I'm really curious what Love Driven Development would look like. Is it kind of like TDD in that before you write a single line of code you write a sonnet about it?