Haskell Is Exceptionally Unsafe (2012)
existentialtype.wordpress.comAs others have said, it's not nearly as bad anymore as It was when Bob wrote that post, but I would say, please do not take that as a reason to not take what he says very seriously. I use haskell because it is a very practical tool, (bona fides: I am an experienced haskell developer and I actually use it full time for my job---not an armchair evangelist) but it has become very clear to me that the next great thing will be more like ML than like Haskell. There are of course many important lessons to be learned from Haskell though!
Could you expand on why you think the next "great thing" will be more like ML than like Haskell?
1. Call-by-value gives us both the ability reason by induction. It also typically results in the presence of non-pointed types, whereas Haskell only has pointed types.
2. Call-by-value gives us the ability to safely interleave effects. Now, I know you all think we should not be doing that at all, but I would say that this is only true in some cases. The point of reifying an effect in a monad is not because "effects are icky"; it is because we have written a non-extensional operation using effects, and we want it to be an extensional function. Wrapping it up in the monad "completes" the operation as such. However, there are plenty of extensional functions which may be written using computational effects (such as memoization): these should not be wrapped up in the monad. (FYI, it's the effects that preserve extensionality which is what Bob calls "benign effects", to the consternation of Haskell developers everywhere.) ML gives us the fine-grainedness to make these choices, at the cost of some reasoning facilities: more proofs must be done on paper, or in an external logical framework. I tend to think that the latter is inevitable, but some disagree.
I am hoping for a middle-ground then: something like ML, in that effects are fundamental and not just bolted onto the language with a stack of monads; something like Haskell, where we can tell what effects are being used by a piece of code.
The story hasn't been fully written on this, but I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.
3. Modularity is something which Haskell people simply do not take seriously, even with the new "backpack" package-level module system they are building. One of the most-loved reasoning facilities present in Haskell depends, believe it or not, on global scope, and is therefore inherently anti-modular (this is the uniqueness of type class instances). As a result, you can never add modularity to Haskell, but we may be able to back-port some of the more beloved aspects of Haskell to a new nephew in the ML family.
(Confusingly, laziness advocates often say that their brand of functional programming has better "modularity" than strict, because of the way that you can compose lazy algorithms to get more lazy algorithms that don't totally blow up in complexity. I would say that lazy languages are more "compositional", not more "modular"—I prefer to use the latter term for modularity at the level of architecture and systems design, not algorithms.)
> I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.
I would be very interested to hear why you think that, or just have some links on the subject. In particular it's not clear to me how CBPV helps us reason about effects.
It might help to read Levy's thesis, which is source on CBPV. Also read the literature on Conor McBride's Frank, which is based on a variant of CBPV.
Could you expand on effects which preserve extensionality some more? I'm fairly sure I understand it, but I've never quite follows what Harper's "benign effects" meant in detail and I'd like to see how it all connects.
The most benign effect of them all is laziness. Haskell uses this in lieu of all other effects, basically.
So memoizing data structures, or a higher order function for memoizing, utilizes a "benign effect".
So extensionally equal simply means that there is a model with and without the effect such that extensionally, according to some model of observation, we cannot discern the existence of the effect?
So, laziness is benign in total fragments.
I wasn't thinking about models, but perhaps you could? I just mean that you get the same results for equal inputs; laziness is fine in this respect (but not in the presence of some other effects).
The best argument for John's thesis is the proliferation of ML derivatives in industry: Swift, Rust and Facebook's Hack. I'm really looking to Facebook's Flow which adds an ML style type system to Javascript.
I would be very cautious about saying "popularity" or "proliferation" suggest that something is good. The ML family happens to have proliferated very nicely, but this is not why it is good.
I'd probably add Scala, too.
Syntactically it's a bit different, but from a modularity POV it is much closer to ML than Swift, Rust or Hack.
I would love to see a "practical" CBPV language.
Likewise, mostly because it would probably help me understand what CBPV actually is!
It's remarkably easy to understand if you're already used to monads. Levy's thesis is a bit opaque from that POV, but not unpleasant to read.
Hmm, really? I just read a couple of papers linked from his website, but I'm still not feeling enlightened.
I may write a blog post. Hm.
That would be great! I'm currently reading "Bridging the gulf: a common intermediate language for ML and Haskell" (Peyton Jones, Shields, Launchbury, Tolmach) which was one of Paul Levy's references for CBPV and it seems likely it was a main inspiration.
I usually think of Filinski's Declarative Continuations and Categorical Duality... but it's such a dense paper I can't recommend it offhand.
I would also appreciate a clear introduction.
> Modularity is something which Haskell people simply do not take seriously
Plus, the build/module/packaging/dependency resolution story, even when doing all the recommended best practices involving sandboxing Cabal and leveraging Nix are just plain embarrassing.
There are so many smart Haskell people. I don't understand how any of them could consider this clusterf*ck to be remotely acceptable.
When using python I use virtualenv. When using Haskell I use cabal sandbox. I rarely have any problems, why is it a clusterf*ck?
In Haskell, sandboxes usually force you to rebuild stuff which you have already built over and over.
Anyway, sandboxes are pointless hacks which wouldn't be necessary if things had been done properly from the beginning.
They are like Node.JS ... yes, it enables you to develop with JavaScript on the server, but how the hell did you end up with using JavaScript in the first place?!
Sandboxes aren't pointless hacks which shouldn't be necessary. It's a lot more difficult for static languages to get right, and solutions like Maven have had tons of work put into them.
You say "if things had been done properly from the beginning" implying you know some mistakes that were made. What mistakes were made in the beginning?
Do you have any ideas how the problems cabal has could have been avoided? There are very intelligent people working on this problem and it is well known that dependency resolution isn't an easy problem.
> solutions like Maven have had tons of work put into them
Maven required tons of work because it's written in Java, not because the ideas behind it are advanced in any sense.
It's sounds absurd because it's so simple, but the issue is that Cabal/GHC doesn't deal with versioning. Different versions of the same library are not properly treated as different artifacts. That's why everything breaks if you install it into a global namespace.
"Great, let's just multiply our namespaces!" is the obvious knee-jerk reaction, but not a great solution.
> There are very intelligent people working on this problem
That sounds great! Because until now I have mostly seen "very intelligent people" who have been busily in denial that a problem even exists.
"the next great thing will be more like ML"
ocaML or even better F#?
I wonder if Ocaml is actually much more practical than Haskell. Ocaml has been proven to be well usable in industry while Haskell seems to be suitable for research areas like math and language design.
http://mirror.ocamlcore.org/wiki.cocan.org/companies.html
I'm learning F# right now, it's flipping excellent! From what I understand it's similar to Ocaml, but has some other features that give it the edge (for me at least).
I did try to learn Ocaml at one point, but I was put off by the standard library variation (the default one apparently has numerous shortcomings, Batteries project extends it and Core project aims to replace it, but neither one is the clear winner) and the lack of extensive parallel processing support (coming soon... https://www.youtube.com/watch?v=FzmQTC_X5R4 ).
F# comes with a sensible default library (including Unicode support as default), some nice syntactic sugar (the pipe forward operator is especially useful, and to be fair it has made it into Ocaml now too... http://stackoverflow.com/questions/8986010/is-it-possible-to... ), seamless interoperability with all .NET libraries, and parallel processing is made comparatively easy (for example, if performing a map operation over a list, can just change the List.map function to Parallel.map to get the parallel version).
This is probably the F# introduction I would recommend the most (it's a video, which I know isn't ideal, but it's a good one): http://channel9.msdn.com/Blogs/pdc2008/TL11
Oh and type providers in F# blew my mind! I can't really summarise them yet, but imagine being able to mix Python or R or many other data sources in with F#. If anyone has a good introductory post on type providers, please feel free to share.
Thanks a lot for these infos! Unfortunately F# is .NET only. Linux requires Mono for installation which means a lot of dependencies. I prefer small efficient solutions (Nimrod for instance). OCaml works out of the box on my system.
OCaml is nice too, it's just not for me. If you like OCaml you should definitely check out Mirage OS, it will fit into your small efficient systems ethos nicely... http://www.openmirage.org/
Rare language has both .Net and JVM support, probably only Clojure now. On the upside you can build iOS and Android apps using F# plus many other gaming platforms.
Clojure is far from the only language that supports both the JVM and CLR. I had a long reply ready, but I lost it. Off the top of my head the languages that have support on both (aside from Clojure) are; Python, Ruby, JavaScript, Java (though J# is being depreciated), Scheme, Common Lisp, PHP, Perl 6, Prolog, Pascal, Ada. I might be missing some.
That's impressive, but I kind of dismissed some of them as scripting languages.
No, that's the weird mythology that gets passed around by people who haven't used both languages. I used ocaml for 4 years and switched to haskell precisely because it is more practical.
Since there aren't a lot of full time Haskell developers, I'm curious to know what do you use to setup your projects and handle dependencies:
hsenv, cabal-dev, cabal sandboxes, nix, stackage ... or do you include everything in your repository (any tool to automate that)?
Full-timer here. I use cabal sandboxes heavily and recommend you do so.
Nix is great but you have to take some time to set it up and learn it - sandboxes are pretty standard and work as you would expect with ghc-mod (not that Nix doesn't I just had more time invested in getting it and the tooling setup to use it as a "dev environment" - cabal sandboxes are much simpler).
Stackage is great too, btw.
Thanks. Since we got the ball rolling (I planned to ask it on some mailing list, but I kept procrastinating to write a semi-formal mail).
Do you know of any way to use multiple stackage repositories? (for now it's not a problem, but I envision a future when I'll have dozens of projects, and updating everyone of them to use the same library versions might not be feasible)
I know that I can `cabal --config-file=/path/to/cabal.config` but I'm wondering if there's an easier way and/or any convention
I'm especially worried of forgetting something (like reusing the same ~/.cabal for multiple stackage-cabal configs)
I haven't actually tried to use multiple Stackage repos. I only think it's great because I helped a friend get started in Haskell and chose to see if Stackage would help with his cabal hell woes (it did and made the experience more pleasant).
In general though, I think stuff like Stackage is a community smell and has the potential for creating a schism and confusion in the community. If it's community infrastructure I also feel like it should be controlled by haskell.org and not a for-profit company.
I know I know, money and man-power are all issues but other OSS languages have successfully figured it out and I think Haskell can too.
I personally use Nix for everyday development.
I would love to use Haskell as a practical tool (I honestly tried that) but the very fact that the Haskell community was not yet able to implement a simple practical thing like a convenient working package manager reveals that Haskell is not so practical after all. We need sandboxes, nix oder even a new OS (NixOS) just for the purpose of developing Haskell software? Come on!
You got very misinformed.
Haskell is actually late to the sandbox party - up to recently you couldn't use them at all, and currently they are completely optional. But now that you can, it would be stupid to start a big project without them, like in any other language.
Haskell package manager is called Cabal. Nix and NixOS are two completely unrelated projects, that not even be recommendable in a development environment.
You have misunderstood me.
I know cabal - with and without sandbox. I said am amazed that sandboxes or nix tools are necessary in Haskell _at all_ while every other language which uses a package manager has one that works out of the box without any hassle and without any sandbox tricks.
> Nix and NixOS are two completely unrelated projects, that not even be recommendable in a development environment.
Other Haskell developers don't agree. They prefer nix even over cabal sandboxes. Quote: "Nix helps me avoid Cabal hell" and "Nix is much better than cabal sandbox".
https://ocharles.org.uk/blog/posts/2014-02-04-how-i-develop-...
I have programmed professionally with C, C++, Go, Haskell, Java, Javascript, Python, and Ruby. While this is not "every other language", I feel it's a sufficient cross-section to be useful for the purposes of this thread.> every other language which uses a package manager has > one that works out of the box without any hassle and > without any sandbox tricks.Trying to do any sort of open-source development without a library sandbox, in any language, is madness. OS package managers are completely unable to deal with multi-version dependency graphs. NixOS is no different, unless you want to install the cartesian product of the possible combinations -- how much SSD space do you have?
---
My experience with Haskell leads me to believe that "Cabal hell" is an artifact of certain library developers' API versioning philosophies. Namely, they release numerous libraries all depending on each other with tight version bounds, and change the API regularly. This behavior is fundamentally incompatible with dependency resolution in a compiled language.
Say you have four libraries:
Then tomorrow you want to release an API-incompatible version of qux and use those new features in foo:foo-1.0 depends on bar==3.8 and qux==1.5 bar-3.8 depends on baz==0.2 and qux==1.5 baz-0.2 has no dependencies qux-1.5 has no dependencies
What do you do here? There's no good choice. Two versions of qux can't be linked into the same binary, and the tight API versioning prevents Cabal from being able to construct a coherent package set.foo-1.1 depends on bar==1.1 and qux==1.6 bar-1.1 depends on baz==1.1 and qux==1.5Now imagine that instead of four libraries, it's O(50), and they're all changing regularly.
Writing lots of tooling and writing manifestos against Cabal sort of helps, for a bit, but it's a lot of work and is deeply unsatisfying for the kind of person who likes to make progress on other goals.
IMO the only practical solution is to loosen the dependency version bounds, and commit to maintaining API compatibility for several releases. I have never encountered Cabal hell when using packages with reasonable versioning philosophies.
> Trying to do any sort of open-source development without a library sandbox, in any language, is madness.
I agree, but there're some interesting differences in how different language tools implement a sandbox.
Python and Haskell (with Virtualenv and Cabal-dev/sandbox) have separate local repo/caches in which packages are installed (this is useful if you want packages in a reliable location to install executables)
Ruby and Clojure (with Bundler and Leiningen) have a common repo/cache with multiple libraries version, and the version resolution is handled inside the project itself (e.g. when you need to whip up a repl or build the project)
(I'm not mentioning rbenv or the like, since that doesn't handle version graphs by itself... but obviously it can be used just like Virtualenv)
IMHO, the second approach is better suited for a language (implementation) that has an explicit compilation step in which an artifact/binary is built, just like for Haskell/GHC
(then again, something like the first approach is still useful for executables and maybe also to try out different compiler versions)
> Two versions of qux can't be linked into the same binary
It might be possible, but yes... it's a world of pain
http://stackoverflow.com/questions/3232822/linking-with-mult...
I think a big part of the issue is that - because of the way Haskell's cross-module inlining works - you need to generate different artifacts not just for each version you use but for each set of dependencies chosen for each set of flags set for version you use. I think this strips away much of the benefit of the second approach.
This sounds like something Backpack might be able to help with! (I don't actually know. I'm speculating. And hoping ...)
Interesting. I hope you're right. I've been waiting for the finished version to pay Backpack much attention, so I also don't know whether you are.
Part of the benefit of backpack seems to be that you can compile modules separately from their dependencies and if this is correct it should go some way to addressing the issue you raise.
That does sound promising.
> What do you do here?
Pick a language where developers are not so cavalier with backward compatibility?
Java has Maven which allows you to exclude transitive dependencies for such situations, and in more than a decade of developing with the language, I've only had to use this functionality a handful of times.
Developers sometimes mess up and break backward compatibility but this should be an extremely rare event. That or the compiler itself is terribly implemented and creating incompatible binaries just by bumping up versions (looking at you Scala).
Thanks for your detailed answer. I think you are right in recommending a way of less tight version bounds.
If you need it, cabal takes an option --allow-newer which can selectively or globally ignore upper bounds, in case the package owner specified too tight a bound
> Trying to do any sort of open-source development without a library sandbox, in any language, is madness.
Really?
Even Java people have been perfectly fine without it. Sandboxing is just a hack around Cabal/GHC not having any workable version support.
To be fair other languages need sandboxes as well: Virtualenv in Python and Bundler in Ruby fill the role
But in a language like Haskell, a sandbox is definitely a subpar solution (glacial compilation times and huge artifacts sizes inside ~/.cabal: 1GB on my machine, compared to the few hundred MB of my ~/.m2). Unless we find a way to bootstrap a sandbox from a vetted/trusted base one that contains things like Yesod (but vetting packages is a job better handled by stackage and/or nix ).
I use Nix, but I'm not comfortable yet in using it with Haskell... to try things quickly I'd need to whip up a nix-shell. But I'm more used to simply have easy access to a ghci repl at my fingertip. And if I install both things, I have to keep care at not trying to cabal install things onto the nix-installed ghc, nor to do the quick-and-dirty thing (go back to install things in ~/.cabal)
Something like lein-try [1] plus Nix might cover my use cases. But Stackage seems simpler and closer to the workflow most haskell developers are accustomed with (and it could be useful also for platforms that don't have Nix available)... if only it'd have more adoption
After a year or so of near constant dependency hell problems with Haskell, I stabilized all my setups on GHC7.8.3 and the associated Stackage inclusive, and it all... just... works...
I can finally go and write some relevant code now.
Where do you work? What has your experience been using Haskell "in the RealWorld"? I'd love to know more about this. My email address is michael.o.church at Google's email service.
I got seriously into Haskell a few months ago, but I've used ML in algorithmic trading and was a major fan.
I feel like it does us a disservice to complain about Haskell's (admittedly, warty) Exception system or "cabal hell" when what is actually going on is that we're holding the language to a higher standard. I agree that functions like head, fail, and possibly non-strict foldl, are warty; but these issues are downright minuscule when you consider what Haskell (language and community) brings to the table. (Also, every other language has warts.) The fact that our complaints about Haskell are minor annoyances compared to other languages' drawbacks, to me, signifies that the language got the major things right.
I've just finished a stint running a team building a start up in Haskell and clojurescript. It's been an amazing year, and for me has completely vindicated my view that not only is Haskell fine for real world use, but for a number of reasons that it's a superior tool to use. I'm ben <at> perurbis <dot> com if you'd like me to expand on that a bit (I don't want to hijack this thread too much).
The exception system that Harper was complaining about really was terrifically bad. It's all based on a form of limited reflection, but previously was implemented in a way that let you pretty regularly and possibly accidentally lie to the compiler. Nasty stuff, now gone.
Yeah... I would say that Haskell's exceptions are still far worse than ML's, but I am not aware that they are unsafe anymore.
Haskell belongs to the ML language family.
I'd bet that he knows that already.
And C++ belongs to the C language family, but one could still say something like "the next great thing would come from a C rather than a C++ like language" (I'm not judging if this is true here, just that it's quite clear what it means).
No, because you can have other ML derived languages that are also lazy and strict, without being necessarily based on Haskell.
He's probably saying that he things the next big thing will be strict by default and feature a neat module system.
Yes, that's close! I also think that we'll need a better treatment of effects than either ML or Haskell can give us, but I hope to have something that has been carefully thought about, rather than bolted on like Haskell's effects.
It sounds like call-by-push-value gives a nice unifying approach to CBN/CBV and also effects. I am hoping that something interesting will come out of that work.
It's been about 15 years since CBPV was proposed. Has there been any work on actually making a practical language along those lines?
Conor McBride & friends have been working on Frank (here's a recent draft paper: http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-...).
Frank's basically based on an extension of the CBPV calculus. As far as I know, Conor's also working on extending the core Frank calculus to the dependently-typed case, though this might take a bit.
I'd like to point out that the example at the end of the blog post is only runnable in GHC 7.6 and Older. As of GHC 7.8, you can't define your own custom typeable methods, you can only ask GHC to derive a typeable instance
>The most blatant violation is the all too necessary, but aptly named, unsafePerformIO
The only time it's necessary is when you're using the FFI or working with language internals, at which point there's really no way for the type checker to work anyway.
One should avoid using exceptions in pure code. This is well established. Instead, use any of the many type-safe exception mechanisms, like Maybe or Either. Having written probably in the high thousands or low tens of thousands of LoC of Haskell, I've never once used a user-defined exception or undefined.
The point of this article seems to be "If your code breaks, it's no longer type safe.". I don't think this is news to anyone.
It's the kind of unhelpful, overly simplified dismissal that HN is known for.
You should recognize that your opinions about how people should use your favorite programming language are not "more or less objectively true".
Context: the post I'm replying to used to end with a complaint that people would downvote something that's "more or less objectively true", and a request that people should explain why. I can't downvote, but I can explain.
The fact that people should use good coding style is "more or less objectively true". I'm surprised that is the part you take issue with.
How is this dismissal overly simplified? What have I failed to take into account?
> Having written probably in the high thousands or low tens of thousands of LoC of Haskell, I've never once used a user-defined exception or undefined.
Good for you, I guess. You'll find plenty of libraries which have no qualms about using exceptions in the real world, though. Not to mention asynchronous exceptions, obviously. Personally, I find both exceptions and type-safe error handling unsatisfactory. The former is unsafe, the latter results usually in a "god error type" which breaks modularity.
>plenty of libraries which have no qualms about using exceptions in the real world
I haven't run into too many (particularly when compared to the popularity of exceptions in other languages).
>the latter results usually in a "god error type" which breaks modularity.
Have you tried using Either with a sum error type and/or an error typeclass?
> I haven't run into too many (particularly when compared to the popularity of exceptions in other languages).
This doesn't mean much if you take a language like Java where it is the idiomatic way of handling errors. But take something vaguely complex like http-client (formerly http-conduit) and you get exceptions.
> Have you tried using Either with a sum error type and/or an error typeclass?
Well, even with sum types you get "god errors" which encapsulate all kinds of issues that can happen in your exception, because it's the path of least resistance. I haven't tried Either with a typeclass, though, but it sounds vaguely abusive.
>Well, even with sum types you get "god errors" which encapsulate all kinds of issues that can happen in your exception,
What's the alternative? Failing to encapsulate all kinds of issues that can happen?
Well, what I'd really want is something more flexible, where you can use inheritance (errors are one of the few areas where inheritance is actually useful - this lets you say that "FileNotFoundError" is a kind of "IOError", add "DimensionGateConnectionError" in the same hierarchy without tweaking any code, and test if the the IOError you got is because you didn't manage to open the dimensional gate. And on top of this, I'd also like this to compose without problems, I'm not interested in creating IOOrFormatError because there is a function which may throw IOError or FormatError. It's a problem that sum types really don't tackle well. As for type classes, it's also not ideal. You can't capture all the necessary information in the interface you expose (IOError doesn't need a filePath field, but FileNotFoundError, which is a kind of IOError does).
There was some discussion on this topic a while back which I remember. For convenience, it is linked here: https://news.ycombinator.com/item?id=4380900
I want to question the importance of soundness in type systems. Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs. Correct meaning, the program runs and returns the correct answer.
Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them.
The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.
This happens absolutely all the time.
For instance, Haskell does it in almost exactly these terms. If you have a type like
and you have a function that consumes drumsdata Drums = Ba | Dum | Tish
you've left out the Tish. Possibly because you don't have a cymbal. You know this, but the compiler doesn't. This is considered to be an incomplete pattern match and would raise some eyebrows.play :: Drums -> String play Ba = "Ba!" play Dum = "Dum!"But often it just means there's an invariant which you know and the type system does not. In Haskell -Wall will stop you dead here, but you can relax it to say "ehhhh, I know what I'm doing".
More generally, you can also write
This 'error' is a misleadingly named function. It's more like 'assert' and indicates that this is a completely impossible program state (much like running into an unbalanced tree deep inside a library function which knows that tree balance is maintained). It's outside of the reach of the programmer to fix. It's not an exception, it's an assurance to the compiler that even though there's something missing in the type safety things will be OK.play :: Drums -> String play Ba = "Ba!" play Dum = "Dum!" play Tish = error "Impossible! I have no cymbal"There is always idea of Gradual Typing [1] which has been implemented with varying degrees of success. There are also a large set of static analysis theories/tools which can help here.
It is also worth noting that if you dont want (global) type inference, you can get far in a language with permissive casting, type annotations and local inference. The results aren't a panacea though.
> Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing.
I am not quite sure what you mean by this. Care to elaborate? (In general, with inference systems, missing type information is hard(ish) to localize. So pointing out where exactly a type error occurred is non-trivial)
I'm thinking of a system with valueset inference where valuesets are not necessarily disjoint. So the system may infer that a return value is the disjunction {INTEGER | REAL}.
In order to get precision in checking, a lot of computation needs to be done so the compiler relaxes the precision when facing large disjunctions (networks) of constraints.
Dynamic checks are inserted as necessary but a system that relaxes when things get hairy can't guarantee that it will find all errors at compile time.
The idea is similar to Soft Typing of Cartwright and others, but they were thinking of an interactive system, some kind of programmer's aid. If I recall they ran into problems giving reasonable error messages.
The problem with this idea, at least compared with current implementations of Haskell and OCaml, is that it requires runtime type information. Right now, Haskell and OCaml both perform erasure, and the only kind of runtime type information used is for the GC, but if you have two ADTs with identical structure (number of branches, payloads) but different names (i.e. they are different types), they will be encoded in the same way. So, in order to tell them apart, you would need some additional type information, which would require changes to compilers and would probably performance characteristics.
> Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them.
It's entirely possible - I believe Dylan implements something on these lines. IMO it's harder to reason about than a consistent type system with "escape hatches" like unsafePerformIO, and about equivalent in usability.
> The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.
I have yet to find a piece of "good code" that I couldn't implement in a typesafe way. I've occasionally found code that worked but couldn't be made typesafe (e.g. the "big global Map<String, Object>" antipattern), but it's always been code that I would have wanted to rewrite for readability and sanity anyway.
>I want to question the importance of soundness in type systems
Why? The most common and popular opinion is already that it is not important.
>Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs.
That doesn't make sense. That's like saying suppose we had a system of math that gave the right answer 99% of the time. How would doing the wrong thing 1% of the time give you the benefit of accepting all correct programs?
>The restrictive nature of static type systems today is legendary
Mythological. Legends are supposed to have some historical root.
>If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.
What does that even mean? That's like saying "if you can't make your idea work with classes or inheritance, chances are good that there's no way to get it to compile and you have to write functions in longhand".
Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated. Mathematics would suffer overall.
Compiler enforced static typing rejects many correct programs, which is a disadvantage.
> Compiler enforced static typing rejects many correct programs, which is a disadvantage.
Only if you care about these programs. It is entirely possible many of these 'correct programs' are not useful at all, or arguably useful, or are outside the domain criteria, and rejecting them is fine. This is often a leading motivator behind the design of things like domain specific languages, or designs like MISRA C - many things by design cannot be done, but often those aren't the things we care about, use, or wish to discuss anyway.
On the flip side, there are things type systems enable that I do not think can be actually accomplished in an untyped language - but really, this isn't very interesting aside from being a minor technical factoid, IMO. It's very far removed from the more interesting question of whether or not it's useful to consider these things at all. And it's completely legitimate to say "No, these things aren't worth considering".
> Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated.
Is that true? Is there a difference between the things which can be proven true in the sense used in mathematics and the set of things which are computable? The limits of proof (e.g., Goedel's incompleteness theorems) and computability (e.g., the halting problem) are at least deeply related, and I'm not at all convinced that your premise here is true.
> Compiler enforced static typing rejects many correct programs, which is a disadvantage.
In practice, however, it is only a theoretical disadvantage. The kind of "correct" programs that get rejected are not very useful.
> Compiler enforced static typing rejects many correct programs,
Do you have any examples of programs that would be actually useful? I don't necessarily doubt that they exist, but it's not an interesting point if the argument is basically "they exist, but I don't know of anyone in particular".
I think millstone is exaggerating a bit as most programs people write normally can be rewritten without too much pain in a static language with a rich type system. That said, there are some examples of times where your program asks for clever type system features (that are not always enabled by default or add to the learning curve) or where different type system features don't play nice together (so its hard to have both features in a single static language, but in a dynamic language you can use one style of programming at a time and never notice the problem).
In the first category, one example is programs requiring higher-rank polymorphism. They are always allowed in untyped languages but in Haskell this feature is hidden behind a language pragma to keep type inference simpler by default.
On the second category, an example I like is parametric polymorphism vs subtyping. The type system gets really tricky if you try to use both at the same time so most static languages either limit the polymorphism or don't allow subtyping. ON the other hand, in a dynamic language you can use both styles if you want, although you have to do so at your own risk.
The problem is that your supposition is just made up. There's nothing to support it. Saying "suppose some thing that isn't true" does not support an argument about reality.
Harper's an accomplished person in CS and has done great work, but he's not putting a good argument forward here.
I've talked to Harper about this post and his opposition to Haskell before. I mentioned that it was leading people to believe they could ignore typed FP, not redirecting to an ML derivative. Harper expressed dismay at this.
There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff.
First: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loos... (This isn't a throw-away reference, informal reasoning has worked extremely well in practice. Yes, I'm making that argument as a user of a pure, typed FP language.)
unsafePerformIO is primarily used to change thunk-memoization behavior [1]. Also, it says unsafe right on the tin. Nobody uses it in practice in ordinary code. It's not something you have to incorporate when reasoning about code.
Giving up reasoning about your Haskell code as if there were semantics-violating unsafePerformIOs lurking in the depths is similar to giving up reasoning about any code because a cosmic ray might flip a bit.
Lets consider the rather remarkable backflips Standard ML and OCaml had to perform in order to make FP work with strictness and impurity.
You can ignore unsafePerformIO because very very few people ever need it and you'll almost never have a reason to use it. Just don't use it.
Similarly, writing total functions is the cultural default in Haskell. The compiler warns on incomplete pattern matches which you can -Werror as well.
You can't define your own Typeable instances as of GHC 7.8 - only derive them, so that soundness issue is gone. Typeable itself is not popularly used, particularly as SYB has fallen out of favor. One critical aspect of why I like Haskell and the community around it is the willingness to fix mistakes. Meanwhile, ML implementations still use the value restriction.
>the example once again calls into question the dogma
Oh please. Haskell is an ensemble, multi-paradigm language with the right defaults (purity, types, immutability, expressions-only) and escape hatches for when you need them.
Haskellers appreciate the value of modules a la ML, but typeclasses and polymorphism by default have proven more compelling in the majority of use-cases. There are still some situations where modules (fibration) would be preferred without resorting to explicit records of functions. For those cases, Backpack [3] is in the works. It won't likely satisfy serious ML users, but should hopefully clean up gaps Haskell users have identified on their own.
Harper's case is over-stated, outdated, and not graced with an understanding of how Haskell code is written. Informal reasoning works if the foundations (purity, types, FP) are solid.
[1]: https://github.com/bitemyapp/blacktip/blob/master/src/Databa...
[2]: http://caml.inria.fr/pub/papers/garrigue-value_restriction-f...
Having read numerous rants by Harper against Haskell, it really just seems like he's upset Haskell turned out to be the "popular" language.
He is an accomplished computer scientist and a major contributor to Standard ML (i.e. understandably biased), but his Haskell rants read like (type-safe) schoolyard banter.
Perhaps there are some sour grapes, but I think more than that he's just hoping for more. Harper clearly has an executes on a grand vision for what PLs should be—he regularly states that there is only one PL and we're just working to slowly uncover it. Haskell fits it in some ways, and now those ways aren't worth talking about any further, and misses it in others. Harper, I believe, writes to galvanize people to move toward his grand vision of unified PL.
ML is better than Haskell in many ways. This should drive Haskell to improve as much as it drives people to check out ML. And it has!
That makes sense. I wish he'd stop writing obviously linkbait titles like "Haskell is Exceptionally Unsafe" when what he means is that there are some really obscure safety implications for typeable exceptions. I completely agree with bjterry that it has probably caused more people to not look at Haskell to begin with, than people to look at ML.
I think, honestly, Harper has recently discovered his platform is larger than he once expected. There was certainly a time that incendiary, link-Barry titles were useful for, say, getting Haskell's exception system to be more safe (which he absolutely played a part in).
As the audience of his posts widens though it's clear that the impact of those posts is changing.
Usually Andreas Rossberger has written a good rebuttal in the comments.
> Lets consider the rather remarkable backflips Standard ML and OCaml had to perform in order to make FP work with strictness and impurity.
What backflips are these?
Apart from the value restriction (which is a real albeit minor inconvenience; I find it about as annoying in practice as Haskell's monomorphism restriction, and each can be removed in principle, at the cost of making it harder to reason about the semantics/cost of using a variable), I'm honestly not sure what you have in mind.
On a tangent, I'm not sure when statically-enforced purity (as opposed to purity-by-default) and pervasive laziness (as opposed to laziness-as-a-tool) became culturally defining features of FP. The original FP language, Lisp (and even its "this FP stuff is great, let's have some more" cousin Scheme) is impure and strict. I'm grateful to Haskell for trying to answer the question "just how far can we push these purity and laziness ideas", but I don't think that complete purity or laziness are necessary features for FP. They're just tools in its toolbox. But then, I have always been inclined to pluralism.
"There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff."
Examples, please. (I like bright, shiny things.)
The principal thing I push learners towards after Haskell would be things like Coq and Agda. Coq has better learning materials, Agda has Haskell integration.
The usual sequence is [1] followed by [2].
Augment with [3] and [4] as needed.
One negative thing about Coq/Agda/Idris is they don't have a satisfactory encoding of typeclasses [5]. This is a problem in general with all dependently typed languages. Proof obligations get "churned" by changing code and the only tool to address that is extremely general proof terms combined with proof search. The best proof search is Coq, but the code extraction is heartburn-inducing for Haskell users.
Whereas in Haskell, we get extremely lightweight and type-safe code refactoring because of the way in which we leverage typeclasses and parametricity. This turns out to be very valuable as your projects get more serious.
That said, still entirely worthwhile to learn Coq or Agda.
By the way, this [6] is how I teach Haskell. Working on a book as well.
[1]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
[2]: http://adam.chlipala.net/cpdt/
[3]: http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf
[4]: http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05...
[5]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...
Perhaps Coq, Agda, Idris, and other such dependently-typed languages are to be considered, at least in some dimensions, "more advanced" than Haskell.
I wouldn't say full-blown theorem provers (Coq, Agda) are really in the same category as Idris, which is supposed to be more practical.
Why not? I'd say that Agda/Idris/Coq are substantially the same languages with variation arising only in the kind of styles of coding they emphasize.
But isn't this a variant on the old "but it's Turing-complete, therefore you can do anything" fallacy? Sure, their type system may be similar, but the question is, which one will let you write, say, a robust, maintainable HTTP client with the least amount of pain?
I suppose that's true. I guess in my eyes DTs are such a meteoric difference that Idris is not sufficiently more interesting than the others yet. But time will tell if they manage to build a better way to manage proofs, for instance, they could really change the game.
That there is no game-plan for doing anything any better than Coq presently does is why I'm a bit skeptical. The trimmings are nicer - nothing else as of yet.
The elephant in the room in these discussions is that the cost of bringing a function compiler to fruition is so high that too much of the discussion gets muddled in the semantics of these hypothetical Haskell-successor languages while no one is actually working on said language. Academia simply isn't set up to incentivize large engineering projects, and industry would never invest in building such a thing either since there's no profit in language dev sadly.
The blunt truth is that at the end of the day Haskell works today, period, and until someone actually forks or starts writing a new language very little of these criticisms of Haskell actually matter if the answer to "what should I use for my project at work" is "well it doesn't exist yet, but it has modules and extensionality and a magical pony that shits money".
This is more or less where I stand as well. Haskell has an efficient RTS, well designed compiler, best-in-industry concurrency, good-enough type-safety that is light-years ahead of even things like Scala, and a good library ecosystem.
It's ready now and I'd like to begin work with Haskell in the hopes that industry wakes up to the utility of future successors to Haskell by seeing Haskell itself in action.
I'm curious what your objections to the value restriction? It's a tradeoff for allowing impurity, which is of debatable use (I like it), but it's not totally off the wall.
As an intermediate Haskeller I'm curious, what's the replacement for SYB? I've worked in haskell primarily on compiler-like tree tranformation code and SYB seems to fit the bill perfectly.
The direct equivalent and replacement is GHC http://www.haskell.org/haskellwiki/Generics.
Edit: I just wanted to add that if you do compiler-like tree transformation code it behooves you to explore uniplate/multiplate/plated.
Sick, thank you for the reply and pointer to uniplate and associated tools!
IIRC, the thing about Uniplate is that the API makes it easy to build traversal functions like "get a list of all X nodes in this tree" while SYB provides some folding operators that are a bit harder to work with.
There's http://www.haskell.org/haskellwiki/Template_Haskell, for one
TH isn't really the same functionality as SYB.
So basically it is "unsafePerformIO" and "error" that is the problem?
So if you do not use them (which I never do and it is recommended not to) then the problem is not relevant?
I think the main problem here is that it's not just you, but also your transitive dependencies.
It seems to me that it would also be any function you import that uses these. Unfortunately, there are a lot of very commonly used functions that use `error`.
Here the reddit thread about this article, from 2 years ago: http://www.reddit.com/r/haskell/comments/y74vn/robert_harper...
Being unsafe never stopped Ruby or PHP, while Ada is still nowhere.
Tell that next time you get on the plane.
This misses the point. Statically typed functional languages. Safety is the selling point here.
"never stopped Ruby or PHP"
Lots of poorly-maintainable code is a good thing?