4 ms·
Thanks for your comments. There does seem to be three languages sure to engender disparate opinions: Lisp, Prolog, and Haskell. I suppose that their advocates c
by todd8 7y ago
Thanks for your comments. There does seem to be three languages sure to engender disparate opinions: Lisp, Prolog, and Haskell. I suppose that their advocates can be forgiven for their enthusiasm. They are all quite remarkable languages.
I am unqualified to assess the benefits of an advanced type system, after all, I've only worked through examples in a few Haskell books. I've never used Haskell professionally. Haskell is a lovely language. Its compiler is a remarkable achievement of computer science, mathematics, and engineering. Simon Payton Jones deserves the notable accolades and awards that he as received.
In my opinion, Haskell's most important contribution is in pushing the state of the art of programming languages forward. Is it practical? Yes, that too, but after all these years, it hasn't really become popular because being "practical" wasn't the main goal for Haskell. Haskell was designed to explore the non-strict functional landscape. Haskell's designers made good choices and were able to expand our understanding of non-strict functional programming (e.g. see Miranda [1]).
In the past I did years of research in program verification, so I'm naturally skeptical of the widely repeated claim that "Once your code compiles it usually works" (it's even on the haskell.org site). In what universe is this true? Verification that a program meets its specifications is quite difficult. In general, no compiler for Haskell can even verify that a program will terminate (the Halting Problem). I don't believe that real programmers are using Haskell's type system to formally verify total correctness (which includes freedom from deadlock, etc.) or even partial correctness (the weaker condition that if a program produces an answer that it is the correct answer).
I frequently write Python programs that work the first time; of course they are little scripts. It isn't dynamic typing that is keeping my programs from working more often. Consider the errors that I do make, syntax errors are caught by my IDE, I don't count those kinds of errors as real bugs. Next there are "type" errors, these aren't really troublesome even when I'm not using Haskell. I can find these almost immediately by testing or even using the REPL. (Every so often, I've heard of, say, a ruby program crashing once deployed because there is an untested path through the code that has a type mismatch between an argument and a function parameter. Haskell would catch this type of defect at compile time. That's good.) However, the really troublesome bugs are more subtle. Do the distributed parts have some kind of race condition? Am I handling the various spans of data within some vector correctly? Can an index touch memory outside of my memory segment? Is the floating point arithmetic doing what I think it should be doing? Have I translated the mathematics of wavelet compression correctly? Do I understand the Vandermonde matrix used in fast decoding of Reed-Solomon error correction codes--I don't! Haskell might be able to help with some of these harder bugs if the concepts can be properly represented in the type systems, but I believe that what mlthoughts2018 is saying is that this is often too hard to be worth it.
Haskell is a pioneering approach to programming, and the next frontier could be dependent types (see [2]). My own feeling is that someday programming will involve a dialog with a proof checker while coding. Writing proofs is hard, it seems harder to me than writing the program, so having an AI assistant that aids with the proof checking might make it more useful than simply struggling to encode a proof in the program's (dependent) types (see the Curry–Howard correspondence[3]).
[1] http://miranda.org.uk http://miranda.org.uk
[2] https://serokell.io/blog/why-dependent-haskell https://serokell.io/blog/why-dependent-haskell
[3] https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence
- ourlordcaffeine 7y agoMy two cents here. In my experience, dynamic typing has not caused unforseen bugs at run time. What it does do, is it causes large codebases to become extremely difficult to reason about, as you could get very little information about what types are needed or received where, and program flow, from the code. Where I work, the managers decided that everything shall be python or ruby. So we have some 10,000+ line codebases, which are very hard to reason about. Including industrial control programs. "garbage collection pauses? What are those?"
- mlthoughts2018 7y agoThis just happens in every programming language. I can tell you because the large Haskell systems I worked on were also incredibly hard to reason about. The analog of garbage collector pauses was accidental misuse of eager evaluation, but buried in misdirection through a sequence of specialized implementations that get called due to type class. Big codebases becoming ugly messes is sociological and pressured by bureaucracy. It is not something that stricter language designs can seriously mitigate, even a little. Meanwhile, very disciplined and experienced teams can avoid it in virtually any programming language. Some of the cleanest and safest huge software systems I’ve ever worked with were written in C, C++ or Python. Also some of the worst huge systems I’ve seen were written in C, C++ or Python.
- JanisL 7y agoI find getting as much tooling as possible that will tell you about types is pretty important with a large code base. For example in the Python code getting type annotations along with mypy up and running tends to be a big win.
- ourlordcaffeine 7y agoMypy certainly helps, but it is not that powerful, and completely falls flat if you use an old library