Haskell, guarantees and pusillanimity

[pozorvlak]

Many times in the course of my Haskell apprenticeship, I've had conversations of the following form:

Me: I want to do X in Haskell, but the obvious thing doesn't work. How do I do it?
Sensei (usually Duncan or totherme): Oh no, you can't do that! If you could do that, then you could have a transperambic Papadopolous twisted asiatic sine-curve freezeglargle Windhoek chromium bebop.
Me: Er, come again?
Sensei: well, [note of horror creeps into voice] it would be really bad! You could get [thing that doesn't sound all that bad, really].
Me: But that's a good thing/Nah, that would never happen/would never happen in real-world code/that's a price I'd gladly pay.

The classic example being, of course:

Me: I want integer-parametrized types for this code I'm writing. Doing without requires you to either write infinitely many lines of code, or write your own run-time type-checking code. This is bad and ugly.
Duncan: But if you did that, your type language wouldn't be computable!
Me: Er, so?
Duncan: Well, it would be Turing-complete.
Me: That's a good thing, surely?
Duncan: No! [note of horror] It would suffer from the halting problem! You could have compilations that would never finish!
Me: [see above responses]

Edit: Duncan denies having said this. To be fair, it was in 2003, so I may have misremembered.
Further edit: I've remembered a better example.

As I've mentioned a few dozen times, I'm coming from a language community that positively embraces ambiguity and irregularity; furthermore, I've been heavily influenced by Paul Graham and his "expressiveness and power above all!" doctrine of language design (and as it turns out, non-terminating compilations are a rare but not unknown problem with Lisp macros, which Lispers accept as a price worth paying). Now, acquiring a new way of thinking about programming is a major part of the reason I'm learning Haskell in the first place, but the frequency with which I'd butt up against some daft-seeming restriction, and the frequency with which I'd be told that this was to prevent something that either seemed harmless or which I knew to be useful, has led me to occasionally lose the humility appropriate to one of my experience.

Previously, I could only think of three reasons for this phenomenon:

1. Sheer endemic pusillanimity on the part of the entire Haskell community.
2. Sheer ignorance on the part of same (not very likely, really)
3. (More charitably) Haskell development is mostly in the hands of academics: hence, language features that allow you to write cool compilers get prioritized over those that allow you to write cool programs.

Now, I think 3) is part of it, but recently totherme sent me a link to a couple of articles that suggests a more interesting possibility: Haskell users prefer guarantees to expressivity. This is reasonably clear in the case of (say) the type system, or referential transparency, but I think it reflects a deeper attitude, that maybe isn't widely understood explicitly.

Here are the links: Does Haskell need macros?
Haskell, bondage-and-discipline and separation-of-concerns programming.

The first article says that Haskell doesn't need macros, because it can already do most of what they provide and the pain they cause outweighs the additional gain. He undermines himself somewhat by ignoring the fact that Haskell already has not one but two macro systems (Template Haskell and cpp, which is used heavily in a lot of Haskell library code), and by seriously underestimating the power of macros. But I digress. His conclusion is revealing: "Macros are quite a painful cost to a language, they reduce the assumptions that people can make and require people to play hunt the macro. Haskell really doesn't need them!"

The second article supports my thesis even more clearly: it's a discussion of the kind of things that can be done once you can guarantee that your language has laziness, referential transparency, etc. Another revealing quotation:

The second thing that purity affords us is that entire programs are mathematical structures themselves and can be manipulated not only in the sense above but also in that theorems satisfied by specific functions can be employed to optimize code — not anymore in the heuristic-working-in-the-dark sense of ordinary optimizing compilers, but in the sense of understanding the actual structure to be done.

This is in particular reference to the functoriality of the List datatype: we know that (map f).(map g) = map (f.g), and so we can apply this transformation wherever we like, reducing two loops into one. Undeniably cool stuff, and Haskell's performance in the Great Computer Language Shootout provides further ammunition. While one could do this kind of thing for imperative languages, Haskell's comparatively simple mathematical structure allows us to prove many more theorems with human-sized brains, and to implement them with compilers more simply. As the author puts it: "giving up destructive updates becomes closer to a doctor advising you to give up trans fats in the name of your health and all the other fun things you can do with a healthy life."

I've heard Haskell described in the following way:

<skew> Besides, don't think aircraft carrier, think mecha. The type system is a great amplifier of careful reasoning and propagator of intent. If somebody starts muttering about bondage, just tell them "those straps are there so the servos can follow *me*".

I haven't yet found this to be true, but maybe the second article could be summarized as "You can't move your legs more than twenty degrees because we needed the room for the flight system. Stop complaining that you can't walk properly, because we've used the extra space afforded to give you something better."

This approach to language design has been tried before (albeit sometimes by accident). For instance, Fortran's lack of dynamic memory allows for some crazy optimising compilers: speed of the order of ten times that of gcc-produced code is not unknown. SQL's basis in relational algebra allows for some nifty query optimisation (and rhetoric very similar to that which you hear from Haskellites). The theory of regular expressions is rooted in the mathematical theory of automata, and many implementations have used this.

Except, in all the above cases, it screws up. It turns out that you really need dynamic memory a lot of the time, so Fortran hackers just declare a big array and use it as a heap, with indexes as pointers. SQL turns out to be extremely painful for some surprisingly common operations. Vanilla regular expressions turn out not to be useful enough, and need extending. In most cases, you end up with something worse than if you'd just written a less restrictive language in the first place.

Haskellers are no doubt at this point jumping up and down and saying "But we have monads! Monads allow you to circumvent the restrictions in a controlled and type-safe way!" Well, some of the time. They don't, for instance, provide any help with the problem I mentioned at the beginning of this rant. Yes, monads are cool (hey, I'm a category theorist, I find it simply wonderful that a categorical tool invented for universal algebra has real-world applications in programming), and yes, they provide an elegant solution to the problem of isolating Naughty Code in Haskell, but no, they're not a solution to everything.

[Here's something that frequently bugs me: why can't you detect Bad Code when compiling, and then mark the code and anything that calls it as Bad unless the programmer has put in a "Badness ends here" marker? I'm thinking of code that presents a referentially transparent interface, but does state-y stuff internally. Is this fundamentally incompatible with first-class functions? Would it slow down compilation too much?]

So, Haskellers: am I right? More importantly, is this widely known? Is it explicitly written down anywhere? (The second article comes very close, but I don't think it gets there in full generality). Because it strikes me that it would be a good thing to tell newbies as early as possible, and also a good thing to have it explicit so it can be appealed to, or (better) debated.

Comments

Types

[cgibbard.livejournal.com]

Types are things which will be checked at compile time. You're saying that you're coming from a language like Perl which is mostly untyped (okay, dynamically typed) -- so you ought to be used to not using types to get those compile time guarantees. If some aspect of the type system doesn't seem expressive enough to you, you can usually just not express those things as types. For instance, use an integer at the value, rather than the type level, and turn the thing into a runtime error rather than a compile time one. Sure, it's not as good, but in dynamically typed languages, you generally don't have those compile-time guarantees at all. Take them where you can get them, and if they're really getting in the way, then do things at the value level and avoid the type system.

Of course, it's been pointed out that you really can get integers at the type level, and do all sorts of interesting prolog-esque programming too. For more on that, I recommend looking at HList ((http://homepages.cwi.nl/~ralf/HList/) and OOHaskell (http://homepages.cwi.nl/~ralf/OOHaskell/), both of which abuse multiparameter typeclasses and functional dependencies to no end in order to do some pretty sophisticated things at compile time. (It uses type-level naturals all over the place to index into these heterogeneous collections)

However, there's a price to pay for doing such computation at the type level. It certainly leaves the impression that the people who designed the features you're using didn't expect you to use them in this way. It's very probable that future iterations of Haskell will make type level programming simpler and perhaps even more like ordinary functional programming. (Indeed, many other research languages are looking at this sort of thing.) However, there are lots of tradeoffs to be made, and it's not really clear which ones are the right way to go.

So far, the Haskell research community (and notably SPJ) have taken the approach of trying to extend HM in useful ways while retaining type inference. One of the biggest problems with moving to more expressive (let alone Turing complete) type systems is that type inference gets blown out of the water, and you end up having to add type signatures everywhere. The general approach has been to try to allow fancy types in ways that allow the fanciness to be completely localised -- that is, you have additional explicit type signatures only on those values whose types are fancy (i.e. extensions over HM), and hopefully not so much in places where those values are just used. Getting even that level of inference can be hard, but progress is being made. Look at the stuff on GADTs (http://research.microsoft.com/~simonpj/papers/gadt/index.htm) and impredicativity (http://research.microsoft.com/~simonpj/papers/boxy/) which are in the newer GHCs for nice examples. We've also had higher-rank types for a while, and of course, typeclasses.

All of these things add expressivity to HM in ways that mostly preserve inference (though they all damage it somewhat), because it's not really enough just to have super-expressive types. Types really have to be convenient so that people will actually use them to express constraints on software. If using fancier types will require adding lots of expression-level type signatures, people will tend to avoid doing it, and those systems will go to waste.

Re: Types

[pozorvlak.livejournal.com]

Hello again! :-)

I need to think a bit about how to reply to this, but I wanted to say thanks - that's a really informative response, and I look forward to checking out those links. "try[ing] to allow fancy types in ways that allow the fanciness to be completely localised -- that is, you have additional explicit type signatures only on those values whose types are fancy" sounds like the best solution - if you're doing serious type hackery you probably won't mind too much about having to put the odd type signature in.

Have you read Alexandrescu's Modern C++ Design (http://www.amazon.com/Modern-C%2B%2B-Design-Programming-Patterns/dp/0201704315/sr=8-1/qid=1169935681/ref=pd_bbs_sr_1/102-8745197-6163322?ie=UTF8&s=books)? It's about some of the extremely cool things you can do with template metaprogramming - dimension checking of physical units, compile-time assertions, all sorts. Highly recommended.

Re: Types

[pozorvlak.livejournal.com]

For instance, use an integer at the value, rather than the type level, and turn the thing into a runtime error rather than a compile time one.
Sure, and if I'd been writing in Perl, I would have done exactly that (or just not bothered, and relied on myself to either not write code that added incompatible things, or detect it in testing). But as I was writing in Haskell, and had the World's Most Advanced Type System (TM) around, and the constraints I was dealing with were clearly type-like, it was rather annoying that I couldn't express them using the type system :-) I think in the end I wrote a Perl script to generate the code for each integer I needed (this was before I learned Template Haskell). Then I graduated, got a job, and lost interest for a while.