Haskell Is Exceptionally Unsafe (2012)
existentialtype.wordpress.com
existentialtype.wordpress.com
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.)
So memoizing data structures, or a higher order function for memoizing, utilizes a "benign effect".
So, laziness is benign in total fragments.
Syntactically it's a bit different, but from a modularity POV it is much closer to ML than Swift, Rust or Hack.
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.
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.
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?!
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.
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.
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).
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.
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.
ocaML or even better F#?
http://mirror.ocamlcore.org/wiki.cocan.org/companies.html
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.
hsenv, cabal-dev, cabal sandboxes, nix, stackage ... or do you include everything in your repository (any tool to automate that)?
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.
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-...
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
> 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:
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
foo-1.1 depends on bar==1.1 and qux==1.6
bar-1.1 depends on baz==1.1 and qux==1.5
Now 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.
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...
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).
Really?
Even Java people have been perfectly fine without it. Sandboxing is just a hack around Cabal/GHC not having any workable version support.
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.
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)
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 can finally go and write some relevant code now.
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.
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.
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.
How is this dismissal overly simplified? What have I failed to take into account?
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.
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?
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.
What's the alternative? Failing to encapsulate all kinds of issues that can happen?
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.
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)
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.
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".
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".
In practice, however, it is only a theoretical disadvantage. The kind of "correct" programs that get rejected are not very useful.
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".
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.
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.
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.
For instance, Haskell does it in almost exactly these terms. If you have a type like
data Drums = Ba | Dum | Tish
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
play :: Drums -> String
play Ba = "Ba!"
play Dum = "Dum!"
play Tish = error "Impossible! I have no cymbal"
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...
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.
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!
As the audience of his posts widens though it's clear that the impact of those posts is changing.
Examples, please. (I like bright, shiny things.)
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".
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.
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...
Edit: I just wanted to add that if you do compiler-like tree transformation code it behooves you to explore uniplate/multiplate/plated.
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.
So if you do not use them (which I never do and it is recommended not to) then the problem is not relevant?
Lots of poorly-maintainable code is a good thing?