Pay no attention to the Dijkstra behind the green curtain

…And so, as we can see, with sufficiently powerful type constraints, the implementation practically writes itself!

Neat!

I know, right??

…although didn’t you just write the whole function inside the type declaration?

THE IMPLEMENTATION PRACTICALLY WRITES ITSELF!!

21 comments

  1. I’m reminded of an instructor I had in a COBOL class back around 1980 who was in the habit of ripping the DATA DIVISION out of the program written by Student A in his class for one JC, and giving it to Student B in his class at the other JC (with different assignments, obviously), with the challenge “write a program that is functionally identical to the original”. The thinking apparently was that “hey, this language has the reputation of computer-programming-as-Russian-novel, but given a bit of foresight, even catastrophic accidents (such as losing a box or six of punched cards, or otherwise having them become unavailable), are recoverable”. I think that experience twisted me for life. 🙂

    1. I attended a training thing at work once all about xUML and how it meant you’d never write code again (so long as you wrote the code to map the code to the code so that you could code while you weren’t coding).

      1. Yeah, I remember when Rational Rose was going to “revolutionise the industry” and “free us from writing code” by creating endlessly baroque diagrams that looked great on PHB managers’ walls but, as far as delivering actual, usable value, were simply baroquen.

        That was actually the second time in my career that the Big Firms were going to market their way to endless software sales and consulting gigs; the first (in my experience) was Computer-Aided Software Engineering in the mid ’80s to early ’90s. I’ve no doubt that such lock-in had been peddled previously; one has only to look at the infrastructure required for Smalltalk and Lisp machines to see that someone was looking for a way to print money. The biggest screw-ups are always about money grabs.

  2. I went to a workshop on Idris last month. While getting the types right does take some effort sometimes, I wouldn’t say that the code was in the type constraints, and the type constraints weren’t super-complicated. But I was actually quite impressed at the compiler/editor’s ability to infer the code in most cases. And I’m not easily impressed. He wasn’t touting that as a major benefit of the type system, just a nice little side effect. The other thing that impressed me was that the language is actually a subset of Turing complete that can be proven to terminate.

    1. I went to an Eric Meijer talk once where he said more or less what I quoted above. In the code in question, the implementation of the function pretty much just reiterated the type declaration. I think the type declaration was actually longer. This repetition was apparently considered a feature.

      1. Erik Meijer says many things. That’s all I’ll say about that.

        Meanwhile, here’s a recent conversation opener (rather than conversation ender) about when or when not to write down types: http://pchiusano.github.io/2015-10-28/top-down.html

        Idris is cool, but I think the future lies in refinement typing, such that contracts can be written “naturally” rather than encoded directly, and the system then munges the type definitions for you. A good start in this direction is Liquid Haskell.

        1. At Strange Loop this year, Andreas Stefik gave a talk about empirical studies of programming language features. He said that there’s evidence that adding types to method signatures is helpful to developers of all levels. But there’s no evidence that requiring types anywhere else (i.e. variables) is helpful. I’m pretty sure all of those studies were with more mainstream languages though, with simple type systems — no dependent types or refinement types.

          I like the suggestion of compromising by having the editor (with the help of the compiler) do the type inference. So you could type out the code, have the editor figure out the types, and create the type signature. And hopefully you could still implement something like Idris’s code inference, so you could start from either direction.

  3. Not sure why my comment was removed. What am I supposed to be looking at? I think it’s a code snippet, but I can’t see it.

      1. I don’t see a link anywhere either. Do you mean the post itself on this page? You say, “as we can see”, and I’m just confused as to what I’m supposed to be seeing.

          1. It sounds like the first character is showing the second one something really cool, but we don’t get to peek enough into their conversation to really understand it (unless you already know about the subject at hand).

  4. Yes. Like many technical jokes, it assumes some context. As you can see from other comments, a number of people are familiar with that context. Not everyone will be, and that’s OK.

    If you would like to become familiar with this joke’s context, I suggest studying statically typed purely functional programming languages for a while. As well as the work of their principal proponents, such as Eric Meijer.

    1. An important correction: this has nothing to do with functional programming, and nothing to do with pure functional programming, but everything to do with types (which are orthogonal to both). You will see this attitude among many in the C++, D, Rust worlds also: the attempt to make maximum use of compile-time type-level programming. Also, Erik Meijer is considered a troll by many (including myself) in the community he purports to be a part of.

    2. I would say, as a general rule of thumb it is not very useful to pay too much attention on the most extreme trollish statements of a few loudmouths here or there, even if they are accomplished people. Whether it’s Linus and his opinions on the value of monolithic kernels, or DHH from Ruby or the uselessness of TDD, or Uncle Bob Martin from Clojure on any number of topics, I respect them all, but note that they are individuals with opinions, and outliers rather than representative of the invisible majority who quietly go about their work (often without even knowing what the big shots do or say).

      1. Some people are hard to ignore. In particular, I’ve noticed that a remarkably large number of people credit Meijer and his courses as their introduction to the FP world.

        1. That’s interesting. For various reasons, I do not recommend his MOOC. However, I should note that in his latest offering (going on right now), Meijer took a controversial stand that I have mixed feelings about but respect. Because the latest version of GHC for Haskell has incorporated more generic types into the standard library imported by default (which had stood untouched for 17 years), Meijer felt that as of this year, 2015, Haskell has gone too far into type land, has rebranded his course as a course on FP while removing the word Haskell from its title, and mandated the use of an ancient Haskell interpreter Hugs98 for the course, the rationale being that pedagogically, today’s Haskell has too much type stuff that get in the way of learning about FP (as opposed to learning about modern Haskell). So he has taken a stand against type oversophistication for a first intro to FP. The way he did this, I don’t like (I hurried up to provide a working build of Hugs98 for Mac from source to help out Mac users), but I agree with him that a course on FP should focus on FP, not on the type system idiosyncrasies of a language that has accumulated a lot of changes in the past two decades.

          I do not recommend the use of Haskell as a first experience of FP. In my recent local presentation “Gentle conceptual introduction to FP for humans”, I barely mention Haskell, show FP patterns in JavaScript and Python, and have been promoting Elm lately as one path toward using types and purity for immediate practical use, for those who are interested in that side of FP.

    3. Thanks, I will do that now. I’m actually already trying to get my head round Haskell, so I hope to understand this in time.

Leave a Reply to Avdi Grimm Cancel reply

Your email address will not be published. Required fields are marked *