5 ms·
> What Haskell does in no more "safer" than if I do tag-checking at runtime. No. Haskell checks at runtime which tag a value has. But, crucially, the compile-t
by thinkpad20 12y ago
> What Haskell does in no more "safer" than if I do tag-checking at runtime.
No. Haskell checks at runtime which tag a value has. But, crucially, the compile-time check guarantees that these tags will always be valid. Assuming you have handled every possible variant of a type (e.g. `Just ...` and `Nothing` for the `Maybe` type), you are guaranteed that you are "covered". Unlike in, say, python, where you might get passed a string, or None, or...?
> The idea that compile-time checks is much better than runtime checks is also not obvious
Dynamic languages have their place, but there's no contest whatsoever when it comes to safety. What's better: discovering an error before the code has run, or discovering the same error while the code is running, possibly in production? In the huge majority of cases, the former is preferable.
> What is better - to clutter the code with explicit type annotation or clutter the code with explicit type-tag checking in the runtime code is another question.
With type inference, you get the best of both worlds :) Most Haskell code doesn't need any type annotations, and most of what's out there only has explicit type annotations for top-level expressions, for purposes of documentation.
- seanmcdirmid 12y agoIt depends on what definition of safety you are using. If it's "won't segfault" or "allow access to a user's private data" then dynamic solutions can be as safe as static solutions. If you define safety as a lack of faults at run-time, then by definition static solutions are safer. If you want to define safety broadly, then both static (upfront analysis, type checking) and run time solutions (hyper visors, tag checks, monitoring) are necessary to achieve it.
- mercurial 12y agoI don't know why you're getting downvoted. Obviously, Haskell can buy you a number of guarantees, but just like the fact that your program type-checks isn't proof against logical errors, it also doesn't mean you wrote the stop condition for this recursive function correctly, or that you are not going to run out of memory at runtime. In practice, and it has also been my experience, as long as you leverage the type system, the debug time necessary to get a correctly-working program in a statically, strongly typed language tends to be significantly shorter than with a dynamic language (or with a statically typed language with a more primitive type system). The size of the code is often comparable as well.
- seanmcdirmid 12y agoProductivity is a different metric from safety. It is more reasonable to argue that haskell allows you to write correct code faster than it is to argue that haskell allows you to write "more correct/safe" code.
- mercurial 12y agoThat's a good way to think about it. Any code can be made correct (for most use cases) with the right amount of man-hours. It's more a question of how many man-hours that is (and how many of them are needed to ensure that correctness is not lost when the code evolves).
- the_af 12y agoAgreed. But note that "faults at run-time", even with recovery procedures, can be very costly in some critical systems.
- seanmcdirmid 12y agoRun-time faults would happen even in a static language however, as those aren't just about tag match errors or NPEs. A really heavy-duty (dependant) type system is needed to get rid of resource (out of memory) and arithmetic faults (divide by zero), so those safety critical systems are more likely to be formally verified instead. Haskell is also completely unsafe when it comes to resource usage, which is why it is not used often in say avionics.
- dllthomas 12y agoYou can get rid of divide by zero without anything sophisticated. The key is that you cannot expose normal division. There are two reasonable solutions: Perform test in the operation: (/) :: i -> i -> Maybe i Require test before the operation: nonzero :: i -> Maybe (NonZero i) (/) :: i -> NonZero i -> i Both of these come at a cost, of course, of making some arithmetic expressions look less natural - which dependent types could probably help with.
- the_af 12y agoYes, runtime faults can happen in a static language as well. However, I don't buy the usual argument that follows up (not saying you are saying this now, but I'm sure you've heard it): "therefore, you're not better off using a statically typed language, therefore just use a dynamically typed language". Just because a statically typed language cannot rule out every kind of runtime flaw is not a good reason to stop using them. Statically typed languages rule out some errors that dynamically typed languages don't. In both cases you also need to perform additional checks, and in both cases, safety critical systems should be formally verified. Not "instead", but "in addition to". A statically typed language is an additional, automatic safety net on top of everything else. Every bit of safety counts. You don't need to formally verify your generic list algorithm isn't going to try adding two elements (and throw an exception when the elements cannot be meaningfully added) because it can't by definition. That's one less formal verification you need to do.