Proposal: Add readMaybe (and possibly readEither) to Prelude, make Haddocks for read more cautionary

[Andrew Butterfield]

> On 3 Jan 2017, at 21:38, Artyom <yom at artyom.me> wrote:
> 
 <stuff elided>
> My personally preferred outcome – i.e. what I want Haskell to be – is a language that is fun to use while still being *possible* to make safe if needed. Thus, I'm glad that newtypes exist and can be used without that much effort. I'm glad that alternative preludes that ban partial functions could be written. I'm glad that qualified imports exist, and I also think it would be good if there was a GHC flag banning unqualified imports. I'm glad that phantom types, type families, etc all exist and are helping people write safe code that they wouldn't be able to write otherwise.
> 
> Howevev, what I feel really strongly about is that such things should not be the default. It's good that a professional Haskeller (or a team of Haskellers, or a Haskell shop, etc) can enforce safety standards if they want to, and it's good that with Haskell it's easier than with other languages, but why should those standards be forced on *all* Haskellers? Contrary to what some might believe, safety is not an ultimate goal of every Haskeller (an example being myself). I'm fine with my code failing every now and then, because the alternative is that it might not get written at all as I get tired of fighting the compiler and the Prelude.

I couldn't agree more. Ironically my main research area is that of formal methods and formal semantics, for techniques to prove software (and system) correctness. I have written a number of Haskell programs to assist me - including a GUI-based equational reason theorem prover [1] and a form of "rapid theory prototyping" calculator [2]. For the former correctness is very important, but not the latter. The problem I have to solve is that of "debugging" semantic theories that I develop - as John Rushby of SRI said back in '93: "95% of theorems are false".

The rapid theory calculator has proved crucial to my recent work, where testing the theory by calculation was rapidly becoming intractable. However developing the calculator itself was only itself  feasible because I could play fast and loose with my code. Just like Artyom, if I had had to fight the compiler and Prelude, I would have lost the will to live....

Perhaps I'm an outlier too ?  ;-)

[1] https://arxiv.org/abs/1410.8216v1 <https://arxiv.org/abs/1410.8216v1>
[2] https://www.scss.tcd.ie/andrew.butterfield/DRAFTS/preprints/UTPCalc-UTP2016-MAIN.pdf <https://www.scss.tcd.ie/andrew.butterfield/DRAFTS/preprints/UTPCalc-UTP2016-MAIN.pdf>
  (to appear in LNCS 10134, Feb 2017

Andrew Butterfield
School of Computer Science & Statistics
Trinity College
Dublin 2, Ireland



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170104/e0715f1c/attachment.html>