Last one today, I expect: Literate Haskell with Markdown and Syntax Highlighting.
A nice interview discussing various aspects of the history and philosophy of Haskell. SPJ sees purity, monads, and type classes as Haskell’s key aspects, and mentions a number of interesting other ideas along the way (along with uniqueness typing as seen in Clean, and functional reactive animation, which I first came across back when I was investigating music in Haskell).
So I’m here to say that mindwarp #3 is discovering the function as the basic unit of abstraction. Jaw-droppingly beautiful abstractions and generalizations can be created out of just functions. You can rediscover the usefulness of partial functions and currying, which were techniques created in the 1800s. You can be in the direct lineage of Alan Turing, who used higher order functions in the 1930s to define his theoretical Turing Machine in his paper “On Computable Numbers, with an Application to the Entscheidungsproblem.” And you can finally understand recursion in a deep and intuitive way, and you’ll feel like you’ve looked into the abyss and somehow come back to tell everyone else about it. And maybe, just maybe, you can explain to me what a freakin’ monad is.
There are many, many reasons why you should never ever accept a job which involves programming in C++ [via TR].
Quite so: prototypes and real applications.
Your prototype needs to be written quickly and then it needs to change quickly. You’ll only be able to do that with a maintainable, flexible code base. In short, a well-written code base. You’re a proficient software engineer, you know how to do this. You probably do it without even thinking.
And at some level, everyone knows this. That’s why prototypes are created in languages like Python. A language that you can write quickly, but also write well, quickly.
C isn’t hard; programming in C is hard. On the other hand: Haskell is hard, but programming in Haskell is easy.
Monads and the meaning of imperative language — the delicious alpheccar does a lovely job of introducing denotational semantics without saying enough to scare you off, and shows how exceptions (or even assert) in imperative languages are, at bottom, the Maybe monad. This point generalises (apparently – I know enough to believe it could be true, but not enough to assert that it isn’t untrue) to “any formal description of control flow in an imperative language will be monadic in nature.” Gorgeous.
The stuff about defining domains (and that being the hard part) is resonating with me just now; I’ve spent the day nailing down definitions of sets describing a particular aspect of my pet specification language, CspCASL, and it’s not trivial. And this is the easy part: not proper “domains”, just sets without much internal structure. Markus does that, for the model semantics. Anyway, yay language design.
Formally describing languages is hard. That’s why it doesn’t happen much yet, which is one reason our current languages situation is so messy. My hand-waving prediction: it’s hard but not intractable, and we’re getting better and better at it; in time it’ll be a sufficiently managable problem, with sufficiently good tool support, that languages which aren’t formally described will stagnate in comparison to the new languages then appearing. Naturally, from where I’m standing I see the increasing convergance of computer languages (sounds like a dumbing-down term but I’m really just trying to cover both programming and specification) with full-blown mathematical logic in all its various and colourful forms. Mathematics is the language for describing things formally; a computer program is by necessity a formal description of something, therefore this convergance seems like it will be a good thing – again, from where I’m standing. Whether or not it appears that way because where I’m standing is a good place to get a view of what’s going on, or just because that’s all you can see from here, remains to be seen. ;-)
A couple of years ago I read and greatly enjoyed Bryan Ford’s 2004 paper “Parsing Expression Grammars: A Recognition-Based Syntactic Foundation” [PDF, 134Kb] (wow, it’s still on my desk, in fact); while to my disappointment it proved inapplicable to my research (I’m constrained in the parsing and language description technologies I can use by what I have to integrate with), it was clearly Cool Stuff.
At the end of Shu, what she sees is nothing but the rules — everything looks like the rules. At the end of Ha, what she sees is nothing like the rules. At the end of Ri, she doesn’t see but work with her mind.
Here’s a pretty clear explanation [reddit] of closures, which have hit the mindspace in a big way since Rails made Ruby the hot sauce of the day. When I say “clear”, I mean, perhaps, from a “traditionalist imperative” point of view — the discussion of stack frames and the funarg problems in particular. Of course, lambda-heads and category theorists probably have other criteria for “clear”. ;-)
(Within an hour or two of publishing this, it was pointed out to me that this talk is really about the IO monad rather than monads in general, and that in particular the assertion that a monad represents a computation which performs a side-effect is not, in general true. A nice example is the Maybe monad. So a better title for this talk is “A pragmatic look at monadic I/O in Haskell”.)
A pragmatic look at monads in Haskell (PDF, 293KB) – slides from a talk I gave last Friday in Swansea University’s Computer Science department, as part of our “No Grownups” series of non-research talks given for and by postgraduate students.
The aim of the talk was to explain monads to a non-expert (and, largely, non-Haskell-programming) audience: why do we have them, what problems do they solve, and how are they used? The approach is pragmatic in that the talk explicitly does not go into technical details, instead focusing on a broad understanding, and on some specific useful “rules of thumb” for programming with monads in Haskell. I don’t claim to be an expert on monads or to have produced a talk which is authoritative or even necessarily completely correct. I do hope to have produced something reasonably comprehensible and useful, however. I would welcome any feedback, comments, corrections, clarifications, etc.
The talk was filmed, but I don’t know if my delivery was good enough to warrant putting it online. :-) Let me know if you’re interested. The post-talk discussion was quite useful, so it might be worth it for that. In particular, there was a question about when exactly the “non-purity” happens – when does referential transparency go away? My answer was that it happens when it needs to (ie when the result is required) and that yes, obviously somewhere there is some code which isn’t pure Haskell and which is doing the impure operation – eg an operating system call. Markus opined that a big part of the point of monads is to give us a clear indication, in the type system, that an operation is impure and thus, in some sense, unsafe/not nice. I thought that was a good enough point that I’ve since added a bullet saying that to the talk – but that’s the only addition I’ve made before publishing.
Background/reference material: A History of Haskell: being lazy with class (historical context), monads @ wikibooks (the nuclear waste metaphor), IO inside: down the rabbit’s hole (probably the point where I started understanding monads), rules for Haskell I/O (not an influence, but something with a similar flavour which I saw when I’d nearly finished), do-notation considered harmful (desugaring), monads on the unix shell (just because the dirty string “dramatisation” is so great).
(I realise it’s gone very “theory of programming languages” round here lately. Don’t worry, I’m sure I’ll have something else to talk about soon.)
Church’s Thesis and Functional Programming, a lovely little paper by David Turner (he of SASL & Miranda fame). Like the Google Tech Talk I mentioned a couple of days ago, it’s big on unifying historical perspective, which is a welcome change from most of the papers I see on these topics, which seem to assume you’ve either read all the papers they reference (recursively), or you’re about to. ;-)
It’s a veritable concucopial tour of TPL: Church’s thesis; the equivalence of lambda-calculus, Turing machines, and recursive functions; how the halting problem fits into that; the lambda calculus; Church-Rosser; strict vs. non-strict; combinatory logic; typed lambda-calculi; implementation of lazy FP (exemplars Miranda & Haskell); domain theory; FP without general recursion; Curry-Howard; Martin-Lof; and a hint of abstract Stone duality (which always makes me think of Father Stone). Seriously, if you’re at all interested in theoretical computer science, you should definitely take a look at this. I started losing the thread in the final section, but loved the rest and, I think, learnt quite a bit – mainly how various bits fit together; like joining the dots on a map.
(Ooh. Strachey coined the term “syntactic sugar”.)
Great stuff: Parametric Polymorphism and the Girard-Reynolds Isomorphism [reddit] – a 30 minute Google Tech Talk by Phil Gossett. A really clear presentation covering a number of interesting topics, with a very convincing historical sweep. Certainly cleared a few things up for me, at least. His response to the last question is really more Hindley-Milner than Girard-Reynolds, mind. ;-)
A name I’ve come across in my work on hets is Grothendieck. In a great example of Wikipedia cascade, someone on #haskell this morning mentioned the programming language Joy (which looks pretty cool), which led to the page on monoids, which led to the page on Grothendieck groups, which led to the page on Grothendieck himself, who a) also looks cool, and b) “gave lectures on category theory in the forests surrounding Hanoi while the city was being bombed, to protest against the Vietnam war”. Respect.