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

[totherme.livejournal.com]

Except, in all the above cases, it screws up. It turns out that you really need dynamic memory a lot of the time...

I think it's worth trying to imagine what it would mean to not screw up. Is there an underlying assumption here, that there exists a holy-grail language, which can precisely and elegantly describe everything in the universe? Is it possible that the languages mentioned work well enough in their own domains, only to require hacks and/or extensions when you try to use them for something unexpected?

TBH - most of the time, I write pure, not extended regular expressions (I use macros, like \w \W and \s - but these fall well within the theory - being equivalent to pure regexps like [a..zA..Z0..9], etc). When I want to do more complex things, I tend to use different tools...

If we resign ourselves for a moment to working with a language that comes short of being the holy grail, then perhaps the interesting question is about the shape of the domain of that language?

Of course, most "general purpose" programming languages have quite funny shapes... I certainly think that there's a huge number of problems which can be more elegantly solved in haskell (using the wonderful guarantees it gives us) than in any other common current language...

[stronae.livejournal.com]

I think you're on to something with your theory about wanting guarantees over expressivity. I'm no Haskell expert by any stretch, but it really pains me when one of my advanced students has to dive fully into monad land in order to do something that's otherwise painfully basic in most other languages. (Like, roll a die.) Certainly he's getting a lot out of the type system, in that he'll be able to structure his thoughts more clearly, but lately I'm wondering if it's worth it.

[totherme.livejournal.com]

...having had a night's sleep/think:

I think that when you say "haskellers prefer guarantees over expressiveness", it shows you're thinking roughly the right thing - haskellers certainly like guarantees.

OTOH, I'm not sure that this is the best way to say it to the world at large - because most haskellers would argue that through those guarantees you get more expressiveness out of your programming system than you would with a more naively expressive language. Haskellers don't want the guarantees because they like guarantees - they want them because they make writing cool code so much easier.

It's actually a really tricky thing to communicate, I think. At least - it is to someone who's already set themselves up to think in a very dynamic programming kind of way... It's really easy to teach haskell to non-coders ;)

[beelsebob.livejournal.com]

I think really you've hit the "use the right language for the job" barrier. I've been using Haskell for all my code for many years now, and never once hit a need to use any form of fancy type system (hey my code compiles in nhc for gods sake)... For my purposes, Haskell provides me with really tight guarentees and enough expressivity. For you it seems it doesn't provide enough expressivity, my suggestion is use a language that does. In fact, my suggestion is use the language that provides the most guarentees for your required level of expressivity. This is why I am a Haskell programmer.

Bob

Number-parameterized types

[greg-buchholz.livejournal.com]

Number-parameterized types (http://okmij.org/ftp/Haskell/number-parameterized-types.html)

[jemfinch.livejournal.com]

You can have integer-parameterized types in a plain old Hindley-Milner typesystem. Matthias Blume did so in order to map C arrays with size into the typesystem of SML. His work is available in this paper:

http://ttic.uchicago.edu/~blume/papers/nlffi.pdf

Jeremy

Bad Code Here

[(Anonymous)]

[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?]

You can! Check out Control.Monad.ST, Data.Array.ST, Data.STRef these all allow for mutable arrays and references in isolated code :)

unsafePerformIO, unsafeIterleaveIO, and more.. allow you to run IO actions that you can guarantee are safe yourself. Using an "unsafe" function is simply declares that the compiler need not worry about what you are doing, that you did the check yourself and it is safe!

[ryani.livejournal.com]

[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?]

Actually, you can do this. If all you need is internally stateful data that uses the heap and doesn't persist between calls, you can use the ST monad:

import Control.Monad.ST

incST :: STRef s Int -> ST s ()
incST xref = do x <- readSTRef xref
                writeSTRef xref (x+1)
mySTAdd5 :: Int -> ST s Int
mySTAdd5 x = do xref <- newSTRef x
                sequence_ [incST x | _ <- [1..5]]
                readSTRef xref

add5 :: Int -> Int
add5 = runST . mySTAdd5

Note that this is an internally stateful algorithm that presents a pure interface.

If you want more power (and correspondingly more ways to shoot yourself in the foot) you can use unsafePerformIO :: IO a -> a. Evaluating (unsafePerformIO action) represents an assertion on your part that the stuff in the action is actually purely functional. A helpful function that I've used while testing code:

import System.IO.Unsafe
import System.IO

constFile :: FilePath -> String
constFile path = unsafePerformIO $ do
    h <- openFile path ReadMode
    s <- hGetContents h
    length s `seq` return () -- force the whole file to get read in right now
    hClose h
    return s

By calling constFile, you're asserting that the contents of the file won't change during the execution of the program. The compiler is free to order and evaluate the file read however it wants, even duplicating it. In practice this doesn't seem to happen and it works reasonably predictably. You can play around with {-# NOINLINE #-} pragmas to make it even more predictable, but that's getting into compiler black magic which I try to avoid.

I've been meaning to write memoize :: (Ord a) => (a -> b) -> (a -> b) which would use unsafePerformIO and Data.Map to do exactly what its name suggests. The tools are there to write "Bad code" as you put it; it's up to you to prove that the code really does present a pure interface to the caller.