1. 8

    So, I am confused. I mixed up several versions of this article, and the version that was online when I submitted this story was not the good one; in particular, it was lacking several changes I made after receiving feedbacks from Mastodon.

    I apologise for the inconvenience, this is fixed now. In particular:

    1. No more confusion between ReturnT and ResultT, the correct name (ResultT) is used everywhere now
    2. I have added several footnotes to actually give pointers to read, related to some GHC pragmas I am using
    3. ResultT is an alternative to EitherT, not to mtl or Eff
    1. 3

      Note there’s a Rust devroom

      1. 2

        This is a bit out of scope, but does anyone know what the colour code means?

        1. 1

          I used to run a devroom there… AFAIK, it’s just that you can easier map the table to the timeline, no specific meaning.

      1. 1

        If you highlight the REDACTED “black rectangles” in the text, you can see the name of the city.

        So author is actually using the name of the city. Uh, oh.

        1. 6

          At the very end there’s also a button to un-redact those, so the author obviously doesn’t really think there’s an issue using the name.

          1. 3

            However, the chance that the city will actually go against a civilian for his usage of the city’s name still seems a little ridiculous, doesn’t it?

            Except, this actually happened to an owner of a Facebook page with ~14k page

            And, yes, there is a button, along with:

            Since this decision defies all logic, and since I have already broken this decision unintentionally a lot of times, I have decided to add a button on the bottom of this article. By clicking on it, this article will no longer be censored, which will make me break the city’s decision exactly 38 times.

            Completely aware of the possible legal consequences of me mentioning the word […], I encourage you to click that button. After doing so, this article will stop being censured.

            Therefore, I think the author there is an issue with the law, and defies it at his scale.

        1. -2

          What I find “ridiculous” is the use of the term “ridiculously” in the title; I put it in the same level as “blazingly,” a term that has been used very lightly in the past years and means nothing anymore.

          1. -1

            ridiculously, adv. so as to invite mockery or derision.

            I guess that means it’s actually really slow?

          1. 4

            Aha, glad to see more people thinking of replacing prelude, especially Snoyman!

            The Foundation project aims towards the same goal, but I guess having a FP-complete backed alternative cannot hurt!

            [edit] Right, posted this comment too soon! This is a different approach, they plan to actually reuse the existing libraries. This is definitely nice, hopefully the prelude problem will definitely be fixed in 2~3 years from now.

            1. 3

              What “Prelude problem” ?

              1. 5

                The project README more or less states the problem:

                The RIO module works as a prelude replacement, providing more functionality and types out of the box than the standard prelude (such as common data types like ByteString and Text), as well as removing common “gotchas”, like partial functions and lazy I/O. The guiding principle here is:

                • If something is safe to use in general and has no expected naming conflicts, expose it from RIO
                • If something should not always be used, or has naming conflicts, expose it from another module in the RIO. hierarchy.

                Snoyman and FP-complete are trying to move Haskell more in the direction of a batteries-included solution for software development. The Haskell Foundation project mentioned by @NinjaTrappeur above is attempting the same thing.

                Many of the changes RIO makes as a Prelude replacement solve problems beginners don’t know they have until they’ve been coding a while in Haskell. Using String rather than Text or ByteString is one of the most common mistakes beginners make. And why shouldn’t they? It’s right there in the “base” of the language. And then you learn, often after months of coding, String performance is a disaster.

                Whether RIO is the right solution, time will tell. That it’s a step in the right direction, is beyond doubt.

                1. 5

                  I personally use Protolude. The problems it solves (for my projects, on my computer, for my use cases) are:

                  • head :: [a] -> a becomes head :: [a] -> Maybe a (and all the other partial functions that throw error "message", like tail and so on…)
                  • everything is Text
                  • convenience functions that I used to copy in all my project, for example: toS which convert from any string-like (Text, String, ByteString, …) to any other string-like.
                  • foldl, head, … are on traversable not just lists
                  • a lot of other stuff, that I’m missing at the top of my head
                  1. 2

                    afaik, it’s the issues connected with the standard prelude, either concerning inefficient data structures (String is defined as [Char], ie. a linked list) or simple lack of utilities, which are then afterwards commonly installed by many uses (eg. Data.Vector). Many other “alternative” preludes have tried to replace the standard, but most of them can’t manage to get any significant adoption.

                    That’s at least what I understand when someone says “Prelude problem”.

                    1. 2

                      The Foundation README gives some information about this “problem”, RIO gives other arguments. The two main issues people have with Prelude is partial functions and Lazy IO, as fas as I can tell.

                      1. 1

                        @akpoff, @zge and @lthms pretty much summed up the problem.

                        I would also come up with another problem class: “legacy semantics”.

                        [EDIT] The following statement is wrong.

                        The most notable offender is the Monad typeclass. As it is defined in base (prelude is re-exporting parts of the base library), Applicative is not a superclass of monad. Those two typeclasses are actually completely unrelated as it’s implemented. In other terms, you could end up with a Monad not being an Applicative. Some people are trying to fix that directly in base, some are trying to fix that in external libraries such as Foundation.

                        In the end, it is not such of a big deal for an intermediate/experienced developer; however, it is quite confusing for newcomers. Not knowing what you can safely use from the standard library is not a really nice user experience in my opinion.

                        [Edit] As a side note, I am saddened to see that the return keyword is preferred over pure. This keyword has a totally different meaning in procedural languages (ie. 90% of the languages), using it in this context is just a constant source of confusion for newcomers…

                        1. 1

                          Applicative has been a superclass of Monad for quite some time in GHC base. I disagree with the change (breaks compatibility) but understand why they did it.

                          1. 1

                            Oh yes, you’re right, my bad!

                            See monoid and semigroup, the problem is quite similar.

                    1. 6

                      I really like the idea behind the theme and the general feel.

                      For my personal taste, as a text editor theme, the background is a little too light and the comments are barely visible. And I say that as someone who uses Solarized.

                      These things are highly subjective of course, and also depend on what room you’re in, what time of day, and what display.

                      1. 2

                        For my personal taste, as a text editor theme, the background is a little too light and the comments are barely visible.

                        The emacs theme deals with this by adding nord-comment-brightness.

                        I think I’m finally going to replace Zenburn (my previous all-time favourite theme)!

                        1. 1

                          Personally, I’ve tweaked my nofrils-like theme for emacs using these colors.

                      1. 2

                        I am still a bit confused by the Nix vs. Guix thing. Not that I am against having two similar projects per se, but I don’t know.

                        1. 11

                          Guix took parts of the Nix package manager and retooled them to use Scheme instead of the Nix language. This works because the Nix build process is based off a representation of the build instructions (“derivations”) and has nothing to do with the Nix language. Guix is also committed to being fully FOSS, whereas the Nix ecosystem will accept packages for any software we can legally package.

                          1. 9

                            Also there is of course accumulated divergence as people with some particular idea happen to be in the one community and not the other.

                            Nix has NixOps and Disnix, but there still is no GuixOps.

                            On the other hand I believe the guix service definitions are richer, and guix has more importers from programming-language-specific package managers, but then on the third hand the tooling for Haskell and Node in particular is better in nix.

                            Nix supports OSX, FreeBSD and cygwin, guix supports the Hurd.

                        1. 2

                          Great article!

                          Also, a heads up that the two local links at the beginning of the post are broken.

                          1. 2

                            Thanks! I will fix that as soon as I can.

                          1. 2

                            The Management Engine (ME) in x86-based computers just rids myself of any desire to study the security of this architecture anymore. I mean, what is the point, if you play against the hardware designer?

                            1. 2

                              Protecting a massive amount of people and companies that are using x86. In case of legacy systems, they’re doing it possibly against their will since they can’t justify the risk of crashing the whole business totally changing all their internal systems and processes. So, a percentage of the security field works on x86-based solutions to mitigate what they can of that with another set doing monitoring and recovery solutions to pick up where first set leaves off.

                              Same for mainframe-based stuff. Same for ARM TrustZone now even though it’s already been quite broken based on a link I just submitted.


                            1. 3

                              Of course there is an emacs mode for X!

                              1. 2

                                Thanks a lot for sharing that! I didn’t know about TypesApplication and was using Proxy myself to deal with this matter. Using the pragma, my code is now much more readable.

                                1. 30

                                  Do not attempt to compete with Pinboard. —maciej on June 01, 2017

                                  Gotta give the man credit for a healthy ego :) Pinboard does rock though. Been a happy user for years.

                                  (Though I’m still waiting for my ‘Fetch Title’ button on the web UI :) )

                                  1. 12

                                    Maybe I’m giving Maciej too much credit, but my reading of that was that he wrote it with his tongue firmly in his cheek. :o)

                                    1. 5

                                      Oh absolutely! I think Maciej should get all the credit in the world :)

                                      Honestly, things like Pinboard are niche services mostly for us uber-geeks and others who care enough to want to wrangle huge bodies of articles and maintain essentially random access to all of it.

                                    2. 5

                                      That date sure helped. For an entire minute, this blog post sounded like something you’d post on April 01.

                                      1. 1

                                        I don’t know the guy, so I have to say, when I first read the post, this particular sentence caught my attention!

                                      1. 2

                                        can one actually generate running code from Coq? I’ve never quite understood how one writes programs in the conventional sense with Coq.

                                        1. 4

                                          can one actually generate running code from Coq?

                                          You can extract Haskell or OCaml programs from Coq:


                                          This was done for example when XMonad was partially verified using Coq:


                                          I’ve never quite understood how one writes programs in the conventional sense with Coq.

                                          Most of the time you don’t really. Proof extraction doesn’t always result in the best code. Sometimes there’s performance problems or integration problems. It’s possible, but Coq is often used to prove code then it’s ported to other platforms.

                                          Maybe this will change in the future. Some recent ideas are going around at the moment:

                                          In addition to using Conal’s work in Haskell, I’m also working on a Coq rendering of his idea, which I hope will give me a more principled way to extract Coq programs into Haskell, by way of their categorical representation.

                                          1. 1

                                            So most usage of Coq is really about writing proofs?

                                            I’ve always been a bit interested in playing around with the language but I don’t really know what the use of the proofs are if the implementations can diverge from the proofs.

                                            1. 3

                                              So most usage of Coq is really about writing proofs?

                                              I’d say so IMO. It’s been almost a decade but a huge breakthrough for Coq in the 2000s was Gonthier’s proof of the four color theorem in 2004. Many regard this as the most readable version proof of the four color theorem, even though it still requires trusting a computer to validate 663 cases.

                                              People talk about validating the classification of finite abelian groups as one of the long term goals of this stuff, since the shear length of the proof makes some mathematicians wonder about its correctness.

                                              A lot of people are attracted to Coq because of its use of dependent type theory. Idris may provide a compelling alternative, however it may not be as mature as a proof assistant.

                                              Personally, I use a proof assistant in my spare time to explore some of my ideas in mathematics. I use Isabelle/HOL rather than Coq. This is because I’ve found Isabelle/HOL has syntax closer to conventional mathematics than Coq, which makes adapting arguments from papers and books easier for me. It also has more convenience features for non-constructive proofs than Coq last time I checked, as well as better integration with third party theorem proves like E and Z3 which makes it easier to quickly find automated proofs.

                                              Exploring proofs in pure mathematics is all the utility I’ve found for computer proof assistants. If you are trying to solve an obscure integral or deal with symbolic z-transforms and their roots, I’ve had more luck with Mathematica. Whenever I try code generation for anything, I write unit tests. For real world correctness I think you are best served by generative testing and finding simple mathematical invariants to check (ie. left-right inverse functions).

                                              That being said, if you love Aigner et al.’s Proofs From the Book, programming and trying out your own proofs then a computer proof assistant can be fun.

                                              1. 2

                                                Coq has a feature call the code extraction. Basically, all the Prop world goes away while the Gallina code is turned into either Ocaml, Haskell or Scheme. The one important thing to know is the extraction algorithm is not itself certified. There is no equivalence proof (similar to CompCert one) between the Coq semantic and the Ocaml semantic for instance.

                                                So, the extractor is part of the TCB and, indeed, the proof link is broken between the “model” and the “concrete machine”. However, one can argue it raises the level of confidence anyway.

                                                One thing to know and which Coq manuals and tutorials never stress out (imo) is that the code extraction is not straightforward. It is hard to extract a code in a safe and efficient manner. For instance, just consider the nat type. You really do not want to use the nat type in most of your program because it is highly inefficient. Yet, all the algorithmic proofs you can do in Coq have a great chance to rely on nat.

                                                Also, having a readable extracted code is not that simple. Most of the time, it goes well. But sometimes, not so much. For instance, I had some trouble with dependent type, once.

                                          1. 2

                                            I really want to give pijul a try, but unfortunately I cannot install it using cargo ): (I get an error when it tries to compile sanakirja)

                                            1. 3

                                              You may have to use the nightly builds of rust. I was able to install pijul with cargo.

                                              $ rustc --version 
                                              rustc 1.17.0-nightly (b1e31766d 2017-03-03)
                                              1. 2

                                                It does not actually require nightly.

                                                1. 1

                                                  It appears I had previously built and installed rust manually, so… my mistake, sorry. And thanks for the hint!

                                              1. 1

                                                Thanks for sharing. I found this reading very interesting! Last time I checked, there was still no software patents in Europe. I wonder if it is still the case and how long it can last…

                                                1. 11

                                                  Meh. I have entries in robots because they are redundant views and mostly a waste of time. Scrape it if you like, but that just means you’re more likely to miss important content. Whatevs. It’s your archive.

                                                  1. 7

                                                    I had a similar thought. robot.txt is fine if it is here to improve the robots work, rather than “hiding something from the rest of the word.”

                                                    1. 8

                                                      I think that’s how most people treat it. Not as a cloaking device but as “hey Googlebot here’s me explicitly telling you these URLs are low value scutwork not worth your time and which would add 30k trash pages to my index”. Google essentially rewards you for doing that by lowering your ranking if you have a large volume of “low value” pages in your index.

                                                  1. 13

                                                    At work, I often can hear the two sides of the story, with some coworkers that dispite everything systemd is or tries to be, and other that are convinced it is indeed a huge improvement over what Linux used to have. I myself still am able not to care very much about it. My system boots just fine and works the way I expected to, so I am happy with it.

                                                    1. 4

                                                      This could be your experience even if e.g. 5% of people found that systemd made their system unbootable after an OS update. At the same time, you’d understand why that 5% would hate it so much.

                                                    1. 1

                                                      I was complaining recently about the lack of strong types in Elixir (which runs on the Erlang VM). I love purescript, so I would love to give this a try.

                                                      1. 1

                                                        This might be a naive question, but have you looked into or used Dialyzer? It’s a tool that does type analysis and it ships with Erlang–can be used easily with Elixir. While it’s not as air-tight as a statically typed language could offer, Dialyzer can help your type-checking conscience rest a little easier.

                                                        1. 1

                                                          As I said in another story, I have a strange bug with Dialyzer so I was not able to test it out yet, unfortunately.

                                                      1. 1

                                                        ❤.rust-lang.org, seriously? Well… why not, after all.

                                                        1. 2

                                                          You can use internationalized domain names to get a domain name with arbitrary unicode. I think it would be fun to buy the λ domain on one of the new TLDs.

                                                        1. 2

                                                          It sounds like tags for repos so you can explore similar projects. There’s a recommendation engine to help you pick tags. I guess this is an enhancement, but I can’t help but feel it’s a boondoggle. Oh well, maybe it will lead to some interesting statistics or help users to make unexpected discoveries. My excitement for this feature is low, but I’ve been wrong about the usefulness of these sorts of things before.

                                                          1. 2

                                                            It is exactly tags for repos as far as I’m concerned. Therefore, it is funny to see that they introduce their new tag feature without writting the word “tag” even once.

                                                            That being said, I look forward to see how it will be adopted by the community; being able to tweak a search in the github database is always a good thing, as one might find some useful example with it. At least, trying to find similar code that the one I am trying to write (e.g. when I use a new language or a new feature) is my number one use case for github global research engine.

                                                            1. 1

                                                              Oh well, maybe it will lead to some interesting statistics or help users to make unexpected discoveries.

                                                              As soon as I see a tag cloud, I’ll know it’s jumped the shark.