6 ms·
Because it has nothing to do with safety, but with manipulating of specialized data-structures. "Instantiation of a value of a given type" in Haskell is what? C
by dschiptsov 12y ago
Because it has nothing to do with safety, but with manipulating of specialized data-structures. "Instantiation of a value of a given type" in Haskell is what? Calling a "type-constructor" which is just what? Constructor - a procedure which returns a data-structure.
Now, how CL style type-tagging is fundamentally different form what Haskell does
What Haskell does in no more "safer" than if I do tag-checking at runtime. (That's why CL is called a strong-typed language). So this is why it is a silly meme.
The idea that compile-time checks is much better than runtime checks is also not obvious (Java's and other commercial languages nonsense about type safety aside - Java is no more safe than CL).
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.)
I personally love Lisp and Erlang with "everything is a pointer to a tagged value" semantics.
- freyrs3 12y agoSafety as you're using is not the concept that Haskeller's refer to when they talk about the language. "Type safety" is a very precise term that refers to several proofs about the semantics of the language. See: http://jspha.com/posts/all_you_wanted_to_know_about_types_but_were_afraid_to_ask/#formal-terminology http://jspha.com/posts/all_you_wanted_to_know_about_types_bu...
- dschiptsov 12y agoOK. All I am trying to say is that there are different kinds of strong-typed languages, and neither one is "safer" or superior.
- the_af 12y agoI don't think that's true, though. There are "safer" languages (for the informal notion of safety we're discussing). You're free to argue that the safety you gain in one language is not worth the effort, but you cannot argue that every language is equally safe.
- dschiptsov 12y agoWhy no? The technical term "type safety" as described in the link above, implies that each value has a type, this type doesn't change during the evolution of a program, etc. How does it differ from the guarantees we have in so-called strong-typed languages? The fact that compiler is refusing to compile type-mismatching expression for a simple built-in types doesn't imply that it is "safer". Other languages, notably Lisp and Erlang will catch and signal the same error later, at runtime. I am not a Haskell guru, but what I see, especially in the case of Monads, is an implicit type-tagging with additional tag - name it State, or IO, or Safe and then type-checking against them. I cannot see the fundamental difference which gives that "extra safety".
- imanaccount247 12y ago>How does it differ from the guarantees we have in so-called strong-typed languages? If you mean "dynamically typed" languages, then it differs in that they do not have types. >The fact that compiler is refusing to compile type-mismatching expression for a simple built-in types doesn't imply that it is "safer" No, it does not imply that. It means that. >Other languages, notably Lisp and Erlang will catch and signal the same error later, at runtime. Precisely. So if that piece of code was not executed, you do not know that it is incorrect. If that branch is only followed rarely, your incorrect code is out there in production waiting to blow up when it finally does run that branch. >I am not a Haskell guru, but what I see, especially in the case of Monads, is an implicit type-tagging with additional tag The article in question does a good job of explaining monads.
- the_af 12y ago> The fact that compiler is refusing to compile type-mismatching expression for a simple built-in types doesn't imply that it is "safer". That's not all a statically typed language does. Regardless, they are safer. The usual counterargument goes that this safety is too much of a burden, or not worth it, etc. But nobody I know argues they are equally safe.
- freyrs3 12y agoBecause you've defined "safety" to encompass several orthogonal concepts and as such is meaningless. If you look at each axis on it's own ( type safety, memory safety, exceptional safety ) then Haskell will come out as safer than nearly any other available tool.
- zoomerang 12y ago> The idea that compile-time checks is much better than runtime checks is also not obvious (Java's and other commercial languages nonsense about type safety aside - Java is no more safe than CL). Runtime checks will only trip up if you happen to hit a code path the introduces an incorrect type. This may only occur in some extremely rare scenario that you never pick up in testing. Compile time type checking allows you to prove that your program is definitely type safe, with 100% certainty.
- dschiptsov 12y agoI am not sure that this assertion is true for user-defined ADTs, which is the essence of programming.
- zak_mc_kracken 12y agoIt's absolutely true for any code that's referentially transparent, regardless of whether it uses user-defined ADTs or any other construct.
- wyager 12y ago>I am not sure that this assertion is true for user-defined ADTs Depends what you mean. It's safe in the sense that you will never get a type error. In Haskell terms, it's possible to write a function that's not total (e.g. not implemented for all possible data constructors of a type), which can then crash or fail to terminate. For example, "head" will crash on an empty list (duh). However, this is easy to avoid, and type safety in Haskell always holds true, as do all the other guarantees the compiler makes (like referential transparency).
- dschiptsov 12y agoYes, the head of [] is the best example. That is what I mean. Thanks for a clarification. Absence of type errors is not safety, it is absence of type errors.)
- 12y ago
- 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.