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.
See: http://jspha.com/posts/all_you_wanted_to_know_about_types_bu...
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".
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.
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.
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.
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.
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.
Haskell is also completely unsafe when it comes to resource usage, which is why it is not used often in say avionics.
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.
> 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".
In practice, there are a lot of other things going on in Haskell that work against formal verification in safety critical real time systems. When you need to know for sure, non-determinism (say in the form of lazy evaluation) is your enemy, and the type system itself becomes less useful because those paths have to be rigorously explored anyhow. Heck, at that point, you might even want to use assembly since even the compiler is suspect.
Thankfully, most of us don't write that kind of code.
Pedantic: runtime is a thing that runs your program while run-time is a phase.
That's a pretty non-standard view. It's as unhelpful as static typing proponents claiming dynamically typed languages such as Python are "unityped". As unhelpful as Simon Peyton Jones jokingly claiming that Haskell is the world's best imperative language :) Any of those claims may be technically true, but it doesn't help us understand, choose or use those languages. Other similarly unhelpful claims include the old "these languages are all Turing-complete anyway, so it doesn't which one you use."
So I disagree with you, philosophically, but since I acknowledge you're a very knowledgeable guy, let me ask you about your opinion:
- Would you say there is no advantage to using a statically typed language like Haskell/ML over a dynamically typed language?
- Or if you think there is an advantage, do you think the costs outweigh the benefits?
- If you were asked to develop a safety critical system, and given the choice of using Haskell (or ML if you dislike lazy evaluation by default, or OCaml if you prefer a more hybrid language) and Python (or a similar dynamic language of your choice), and every other analysis tool you can think of, static or run-time, which language would you pick? Assume you cannot pick anything else, you're given time to become proficient on the language you pick, and you cannot refuse the assignment. I know, this is a fantasy scenario, but indulge me.
Safety critical systems are generally real tine so Haskell is off the table. I'll also spend a lot of tine manually verifying the code, and using alot of external analysis and verification tools, so restricted C++ is fine in that case. Now, if you told me that the system was safety critical and nit real time, and the system wasn't important enough to merit lots of manual verification, then Haskell would be a great choice because its static type system is better than nothing.
Why do you think Haskell is fine as long as the system "isn't important enough to merit lots of manual verification"? That sounds puzzling to me. I'd say one thing complements the other: automatic and manual verification seems the best option.
Is lazy evaluation your biggest issue with Haskell? How about languages like ML or OCaml, which are arguably safer than "restricted C++" and do not default to lazy evaluation?
Or is GC your main problem with these languages? This would rule out most dynamically typed languages as well.
Anyways, you might want to read the stack overflow article on this subject:
http://stackoverflow.com/questions/243387/which-languages-ar...
Perform test in the operation:
(/) :: i -> i -> Maybe i
Require test before the operation:
nonzero :: i -> Maybe (NonZero i)
(/) :: i -> NonZero i -> i
What is your opinion of Idris?
This is part of what makes HoTT exciting, I believe, as it provides a formalized way of passing proofs and operations around over different types so long as there's a suitable homotopy.
So while Idris is a very exciting research direction, it's completely fair to state that they have a hefty set of barriers to overcome before they truly demonstrate the value of DT in some larger variety of usecases besides just theorem proving.
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.
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).
Absence of type errors is not safety, it is absence of type errors.)
There's no reason to throw the baby out with the bathwater though, since 90% safety is a hell of a lot better than 0% safety.
Personally I'm keen to see mainstream languages adopt better totality checking for that exact reason - my fantasy language would enforce that `main` is always a total function*
*(For this fantasy language, I'd probably allow infinite recursion to still exist, since the halting problem is theoretically impossible to solve without introducing a lot of pain to prove that your code will actually terminate, and that level of totality checking is often counter-productive for general-purpose code)
However, if you do get a pattern match failure, one of two things is true:
1. You can easily fix it by accounting for all patterns (or adding a default match)
2. Your program model is conceptually broken and you should probably find a new model that accounts for all possible patterns.
Much easier to deal with than a type error :)
Though these days I've been saying "Turing complete" is a bug, not a feature, provided you can accomplish your aims without it.
It does, although for Option and Result, there's .unwrap() which simply exits the program (through fail!()) on None/error. The fact that you can do this is practical, although could potentially train bad habits.
-xc (Only available when the program is compiled for profiling.) When an exception is raised in the program, this option causes a stack trace to be dumped to stderr. This can be particularly useful for debugging: if your program is complaining about a head [] error and you haven't got a clue which bit of code is causing it, compiling with -prof -fprof-auto and running with +RTS -xc -RTS will tell you exactly the call stack at the point the error was raised.
http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/runti...