Simon Peyton-Jones: Escape from the ivory tower: the Haskell journey

Yes, I didn't include the papers below in my parent response because, “just read these dense academic papers to understand what monads are and why Haskell has them” doesn't tend to be good advice for Haskell beginners. But learning why monads came to be included in Haskell is useful if you want to dive deeper into this stuff: Philip Wadler's original paper on Comprehending Monads [PDF]: [link] Philip Wadler and Simon Peyton-Jones' paper on Imperative Functional Programming [PDF]: [link] Simon Peyton-Jones mentions both papers and talks about why monads came to be part of Haskell in his talk on the history of Haskell here, with examples that are a little more accessible than the above papers: [this video] [introduction to purity and then monads starts around 30:07] It's a funny talk and it's worth watching in full, but here's a nice soundbite: “So what did we do for IO? Well, we just didn't have any. [audience laughs] So the joy of being an academic, right, is you can design a language — in 1990, I beg to inform you — that had no input/output. A Haskell program was simply a function from string to string. That was what it was. … But this was a bit embarrassing…” He goes on to talk about other ideas they explored to create effects, why they settled on monads, and why he wishes now they had called them something like “workflows” (as F# later did[1]) to make them sound less intimidating. (Simon and Philip will both be at Haskell Exchange 2019 in London this coming week if anyone else,

Unsound typesystems are not necessarily a problem, but consider the problem the other way around: given a sound typesystem, how do we improve this in such a way that a) the average Joe will understand it b) it decreases the overhead of writing the types c) the type system helps the programmer write better programs Haskells approach to this keeps the constraint of soundness: [this video] The whole video is very interesting even if you know nothing about Haskell, but are just interested in language design in general. To summarize the part of the video I just linked: Their approach so far has been to try and design the type system in such a way that you reduce programmer pain while not sacrificing soundness at all. It is a painful constraint for language designers, but it allows you to gradually add functionality to the type system from observing real world examples. The goal can be described as: Design a typesystem such that every working program can be typed in both a sound and correct way, while minimizing the amount of programs that can be typed, but are not working as intended.

> An example is not being able to prove the termination of executing arbitrary programs The theorem states that you cannot prove a program's termination any faster than running it. You're not violating any theorems. > So, Im wanting it peer reviewed. But it has been peer reviewed. Here is the publication [link] in this journal [link] > So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. First, I think you're misinterpreting (and exaggerating) what has actually been achieved. Looking at Hyper-V[1], 30KLOC of (preexisting and tested) C code have been verified in a year (out of a total of just 100KLOC), but only function-by-function, rather than global correctness properties. They wrote some global invariants, but didn't verify them. As I understand, such similar verification of various layers has been done, but no global end-to-end work. Whether low-level or high-level, there has been no composition across abstraction layers. Second, such methods would not allow us to go "upward", because there's a reason why people concentrate on the lower level. The state space is smaller there. Finally, I think you're also misinterpreting DeepSpec's work. It is at the forefront of verification of a certain kind, but if you look at their papers, when they talk about end-to-end verification, they're discussing programs that are 3KLOC C. These programs are smaller than many JavaScript libraries. Also, Coq is not

That's because Haskell is like the programming language equivalent of The Gig That Changed The World[0], although I guess Algol60 also has a strong claim to that title. Let me explain by quoting these paragraphs Roger Ebert's review[1] of 24h party people: > As the film opens, Wilson is attending the first, legendary Sex Pistols concert in Manchester, England. (...) Wilson is transfixed by the Pistols as they sing "Anarchy in the U.K." and sneer at British tradition. He tells the camera that everyone in the audience will leave the room transformed and inspired, and then the camera pans to show a total of 42 people, two or three of them half-heartedly dancing in the aisles. Sounds like the average language designer entranced and inspired by their first time grokking Haskell. > Wilson features the Pistols and other bands on his Manchester TV show. Because of a ban by London TV, his show becomes the only venue for punk rock. Turns out he was right about the Pistols. They let loose something that changed rock music. And they did it in the only way that Wilson could respect, by thoroughly screwing up everything they did, and ending in bankruptcy and failure, followed by Sid Vicious' spectacular murder-suicide flameout. The Sex Pistols became successful because they failed; if they had succeeded, they would have sold out, or become diluted or commercial. I saw Johnny Rotten a few years ago at Sundance, still failing, and it made me feel proud of him. I could rephrase that last sent