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...

[pozorvlak.livejournal.com]

I think it's worth trying to imagine what it would mean to not screw up.

That's an interesting question! And to be honest, I don't really know the answer. I guess by "screw up" I meant "the restrictions you enforce condemn the language to an excessively narrow niche, and make things that ought to be easy hard". So yeah, you could argue (as Duncan does, in fact) that Fortran is a great domain language for very fast numeric algorithms that don't need dynamic memory, and that we should only use it as an embedded DSL in some general-purpose language. But that's not how it actually gets used, most of the time. My comments about regexps are a bit dodgy, in that the only proof I know that Perl regexps have been extended is that you can embed arbitrary Perl code into a regexp :-) Do lookahead/lookbehind assertions fit the framework? The case I really wanted to talk about is Prolog, where you spend half your time second-guessing the optimizer and the other half the time writing Yet Another meta-interpreter (from my admittedly limited experience). Or think about SQL - surely you've had that experience where, no matter how far round you twist your brain, you can't write the query you're thinking of, but you can describe it in a simple sentence, and could write it straightforwardly in a more conventional language?

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...
Quite possibly - I'm still trying to decide that :-) It seems that in many cases (Laziness? Referential transparency?) "guarantees over expressivity" gives the right (or at least a good) choice - the leverage you get outweighs the restrictions. But I'm really just trying to isolate the general design principle. Because I'm not convinced that it's such a great idea as a general principle, if your goal is to design a usable language. In the limit case, of course, it leads you to prefer the guarantee of program termination to the expressiveness of Turing-equivalence :-)

[totherme.livejournal.com]

SQL:

Peronally, the problems I think I've had most with SQL don't stem from its lack of expressivity as from its poor integration with the rest of the programming system... Getting no compile time checking over SQL which was all in strings in a java programme really sucked. Also, dumping java data into BLOBs, which are totally inaccessible to SQL queries was annoying....

The usual complaint about SQL is that you can't search for a substring, or a regex within a value. This is annoying, it's true - I don't understand what the reason for those original restrictions were and it's probably the case by now that a database could provide this functionality and still provide the guarantees that make the database worth using - but let's pretend for a moment that they couldn't. In that case, you have to pull everything out of the DB, and do the substring check in your general purpose langauge. Would you be better off without the database? If so, why are you using a database in the first place? It seems likely to me that you're actually gaining a lot from having the DB there, probably as a result of some guarantees it can give you (about concurrency, or guarantees allowing performance optimisations or whatever) - otherwise you wouldn't be using it. If that's the case, then you're not complaining that SQL restricts what you can do (relative to your general purpose language), you're complaining that it doesn't extend what you can do far enough. If the language can be made more expressive without sacrificing those guarantees, then that's great. But if allowing a substring match meant that concurrency didn't work any more, and the database was as slow and memory hungry as your general purpose language - what would be the point?

In the limit case, of course, it leads you to prefer the guarantee of program termination to the expressiveness of Turing-equivalence :-)

If the scale we're thinking of is the one that stretches from 0 guarantees to infinite guarantees (presumably some kind of constant statement, or something?), then I don't think limit case analysis is particularly useful. If guarantees were all I cared about, I'd bury the computer in my back garden - possibly after burning all the bits that would burn. Then I'd be absolutely sure that no bad things were going to happen. If I wanted no guarantees at all, I'd programme with "cat /dev/random > a.out"

The interesting thing about language design is finding sweet spots, where you have the guarantees you want, and the expressiveness you want (and it's not necessarily always a simple trade off between the two).

[pozorvlak.livejournal.com]

"Poor integration with the rest of the programming language" is definitely a problem with SQL. I've told you about the pain we had with schema mismatches between the (constantly-changing) database and the (permanently a few days behind) C++ layer when I was working on [classified]? I did suggest autogenerating the whole object-relational mapping layer, in the way that Ruby on Rails or Maypole do, but this was felt to be too much work :-(

I've been having a look, and can't find the specific problem that I'm thinking of - it was some feature that Mat wanted to add to Moblog (I think it was "Comments posted on (posts that you've commented on) since you last logged in") that we found we simply couldn't do in SQL. He had to set up a cron job to create an intermediate table. Possibly this was just a problem with MySQL (which at the time didn't support nested subqueries), but it was pretty lame.

[sethg]

Consider for a moment HTML. As a programming language, it's, well, not. But because the bulk of the Web is "written in" HTML (in the sense that HTML is what's exposed to the browser or other client), browsers can do start rendering a page before they've even read all of it, spiders can get useful information off the Web without having to embed a Turing-complete language interpreter, and pages written by newbies might look ugly but they communicate more or less what their authors intended and are very unlikely to crash your browser.

IIRC one of Richard Gabriel's complaints about Common Lisp is that because the standard allowed programmers so much flexibility, it was very difficult to write an optimizing Lisp implementation--which meant that novice-to-intermediate Lisp programmer would get lousy performance until they learned the optimization tricks of their particular implementation.

So I think that in general, constraints on the language end permit optimizations on the implementation end, and when a language user is doing things that don't continually bump into those constraints, that leads to happiness on the user end.

The proper way to accommodate users that do run into those constraints, IMHO, is to provide escape hatches to other languages: SCRIPT tags, the Haskell foreign function interface, PostgreSQL "createlang", etc.

[pozorvlak.livejournal.com]

Interesting, particularly about Common Lisp (does Scheme have this problem?). I wasn't for a moment trying to claim that "guarantees over expressivity" is never a good idea, I'm more trying to isolate the general principle so we can think about it - saying that it's always a good idea is probably just as stupid as saying it's never a good idea. As totherme says above, it's about finding the sweet spots.

And welcome! How did you find me?

[elvum.livejournal.com]

Is there an underlying assumption here, that there exists a holy-grail language, which can precisely and elegantly describe everything in the universe?

The lack of such a language is (as I believe you know), a source of continuing annoyance to me. Although you could argue that it could only exist in a universe where humans were capable of describing things precisely and elegantly in the first place. I expect it's all quantum.

[pozorvlak.livejournal.com]

Have you read Paul Graham's essay The Hundred-Year Language (http://paulgraham.com/hundred.html)? His basic contentions are that

1. While we can't program in the language they'll use in 100 years, we can try to predict its features, and this provides a useful heuristic for choosing languages to use or designing new languages
2. More powerful computers will demand languages that can provide a greater range of efficiencies: highly optimized for crypto/image rendering/etc, highly expressive but possibly highly inefficient for most stuff
3. "The desire for speed is so deeply engrained in us, with our puny computers, that it will take a conscious effort to overcome it. In language design, we should be consciously seeking out situations where we can trade efficiency for even the smallest increase in convenience."

... and a bunch of other stuff, most of it interesting.

Basically, he thinks that in a hundred years time, most people will be using a descendent of Lisp :-) But it's an interesting idea: if you're trying to design languages now, you should aim for the holy-grail language: even if you don't succeed, you're likely to get something better than if you'd just tried to write a slightly better Fortran (http://sig9.com/node/199).

[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.

[pozorvlak.livejournal.com]

Yes, I know exactly what you mean, and that's a great example :-)

[totherme.livejournal.com]

I know what you mean - monads look really scary, particularly if you're used to imperative programming. But I don't think it's nearly so bad as you think:

    main = print =<< randomRIO(1, 6)

or if you prefer: main = randomRIO(1, 6) >>= print - or even main = do x <- randomRIO(1, 6) ; print x

how is that any worse than main() { x := random(1,6) ; print(x); } ?

The thing is, I think imperative programmers are in monad land all the time. Functional programming offers a way of diving out ;)

[totherme.livejournal.com]

...actually - I was just talking to surfnscubadiver about monads earlier today (he was a coder in the 80s, but not since). The thing that occurred to me during that conversation was:

Understanding your car (the engine, all the accompanying electrics and gubbins that keep it doing what you want, the transmission, etc) is Hard. But you can still drive.

Understanding Monads is Hard. You have be conversant in the most abstract, weird branch of mathematics I'm aware of. I think using them is deceptively easy - if you just concentrate on using them, and not understanding them. Accept that you can do sequencing (and things that rely on sequencing) inside the moand, but not outside. Trust it the same way you trust the compiler to write better assembly than you can, and concentrate on understanding more interesting things - like the meaning of your programme.

[michiexile]

Pfah!

There are a lot much weirder and more abstract branches of mathematics than Monadland. Those are still somewhat decent.

Now, parts of my workgroup are doing research on the ringstructure you could put on subcategories of kG-Mod by assigning addition to ⊕ and multiplication to ⊗_k, with k as the multiplicative identity, and the {0} as the additive identity.

The first PhD thesis was on calculating the prime ideals for this beastie for a few small examples.

[pozorvlak.livejournal.com]

Eeek. That sounds scary... and actually slightly wrongheaded. Typically, quotienting out by isomorphisms to get an actual (monoid, ring, whatever) from a (monoidal, ring, etc) category (is this what they're doing?) either loses lots of information (what happens to the morphisms?) or gives you something ill-defined. If you look at the proof that every weak monoidal category is equivalent to a strict one, the strict one constructed is actually much larger than the category you started with. Are they aware of Laplaza's paper on rig (semiring) categories? It might give them a start on sensible ways of categorifying the notion of rings, or at least provide a useful thing to cite.

This may be irrelevant to what they're doing, though - could you send me a link? I'd be interested to learn more, as this whole area of algebraic-structures-on-categories is my area.

Monadland is a lot less weird than many branches of mathematics - number theory and dynamical systems spring to mind - but I think there aren't many that are more abstract. Model theory and topos theory, maybe. Monad theory is deep magic (http://catb.org/~esr/jargon/html/D/deep-magic.html) rather than heavy wizardry (http://catb.org/~esr/jargon/html/H/heavy-wizardry.html). Once you grok it, it's simple, and all the definitions and theorems involved are straightforward, but the conceptual leap required to understand them is nontrivial - I remember with pleasure the deep "Aha!" moment a couple of years ago when it clicked :-)

[totherme.livejournal.com]

Actually, I was thinking of category theory as a whole when I said that... ;)

[stronae.livejournal.com]

Well, let me introduce myself. I'm stronae, and I'm a Scheme programmer. :) I came to Haskell via its functional core and its type system, so that's how I relate to it. You don't need to convince me about Haskell's virtues; I already believe, but my problem is that doing easy things is harder in Haskell. For example:

I agree that the things you provide above are no worse than each other, but consider: both are way worse than

(random 6)

which requires no knowledge whatsoever.

Maybe most people who learn Haskell get subject to Monads vs. Functionality early, so whipping out a side-effect is effortless to them. When I first learned about Monads, they were quirky, and alien, and despite looking high and low on the web, there really wasn't anything out there to get me functional enough (if you'll pardon the pun) to do everyday things. Nevermind that most of the tutorials have you attempt to learn about the Monad At Large, and only after you've digested that, you could then proceed to the IO monad, which is what I was (apparently) interested in in the first place. Suffice it to say, it's a painful way to go. (If you happen to know of a sane and rational tutorial, feel free to mention it. :))

I would agree with the thread below, where you state that it's easier to just not understand them so much and just use them. But to 'just use' requires a certain knowledge of the syntax, when x <- (f 5) is required versus x = (f 5), that an if/then command is available but you have to provide your semicolon, and so on. Not a big deal in the long run, but to a novice user, it's nontrivial.

[totherme.livejournal.com]

Hey :) I'm totherme, good to meet you :)

I guess I learned haskell the Bird way - which isn't the way I think many hackers learn to code. We started with calculating interesting things, rather than with doing interesting things. It was quite a while before we bothered with monads at all, because there was plenty of other interesting stuff to do. This isn't a very "practical" way of doing things, of course - since pretty well all practical programmes require IO. Having said that, I think it's a good way of learning how functions work.

You're certainly right when you say that most haskell docs about monads try to teach you about monads in general. I think you're probably right when you suggest that this is suboptimal for a large percentage of people. I also think it's understandable - monads are a really cool abstraction, and most of the community are bursting with a joyous desire to share them with the world :)

(I've heard people suggest that they could be as ubiquitous as Objects in OO lanugages - a cool way of chopping stuff up, to be used everywhere - not just a weird hack to let you do IO)

From this point of view, I really like sigfpe's tutorial: You Could Have Invented Monads.

Having said that, it's probably as freaky to learn about monads this way as it is to learn about Objects for the first time... You remember learning/teaching that concept? Trying to understand/get across the difference between a class and an object, the meaning of instantiation, of inheritance, static things that live in all objects of a class at once, the "is a" relationship that inheritance should model... It's complex stuff - and a lot of people just want to write short, simple things. These are folk that don't need monads any more than they need a full object system. This is why languages like python and ruby allow you to write simple scripts, despite being OO languages.

From that point of view, the tutorial I like is dons' Programming Haskell series. He pretty well just tells you how to do things - in real contrast to the way I was taught. It looks like good stuff to me - but I'm not the target audience any more, and I haven't tried that tute out on any novices yet.

Now - those two links are both for someone who's doing their own thing, and needs to learn IO or monads in haskell - they're not full tutorials for teaching haskell. I'd feel wrong if I didn't at least mention YAHT. Where the above links are fairly to the point, YAHT is comprehensive. If someone asks me "What should I read to learn haskell?" - that's what I point them at. It's probably not relevant to this thread, but I like linking to it :)

As for the issue of haskell's syntax being different from most imperative languages - yeah, it is. This certainly does make it tougher to switch from imperative programming to haskell programming. I think the syntax is quite reasonable, and find that people who've never coded before don't have any problem with it. I've also heard some maths types (usually who've done little or no other coding) comment how easy it is to translate maths syntax into haskell syntax... So I guess those are the target audiences for the syntax: new coders and old mathematicians ;) For existing coders, I guess the best option is to point at the tour of the syntax, and hope it's user friendly enough :S

[pozorvlak.livejournal.com]

Have you seen Monads as Containers (http://www.haskell.org/haskellwiki/Monads_as_Containers)? Or is that the kind of thing you're complaining about - starting with monads in general and then specialising to IO? IO isn't the easiest one to start with if you want to understand the concept in general, I think.

Do you know about the use of monads in algebra, and in particular things like the "free group" monad? For me, a lot of enlightenment came from comparing the Haskell definition with the categorical one, and the rest came from thinking about algebraic examples.

Monad transformers, on the other hand, I still don't really get. Just Doing It will help, for sure, but it would really help if I knew what they were meant to be mathematically. Distributive laws?

[stronae.livejournal.com]

Have you seen Monads as Containers? Or is that the kind of thing you're complaining about - starting with monads in general and then specialising to IO? IO isn't the easiest one to start with if you want to understand the concept in general, I think.

Haven't seen it yet, no. But you guessed it: I tend to believe that I shouldn't have to learn a whole body of theory (up front) just to print something to screen. :) I'm happy to learn the theory later, when I'm more conversant with the syntax and aware of what I should be looking for, but don't make me pull out my hair for "hello world" on Day One.

I guess, in the end, every tutorial out there is perfect for exactly one person: the person who wrote it. Each will be "good enough" for more people, but it's hard to find the right tutorial for the things you're missing, and what's good for one person (or class) might not work well with another person.

Do you know about the use of monads in algebra, and in particular things like the "free group" monad? For me, a lot of enlightenment came from comparing the Haskell definition with the categorical one, and the rest came from thinking about algebraic examples.

I'm in a Homological Algebra course now, so we'll eventually get to categories. If we touch upon what you mention, I'm sure I'll be doing the comparisons implicitly. :)

[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 ;)

[pozorvlak.livejournal.com]

I was deliberately using the word "expressiveness" to avoid the connotations of the word "power". Hmmm. For the definition of the word "expressive" I'm thinking of, Perl and Lisp are very expressive languages. Vanilla Pascal is a very unexpressive language. Cobol is a very unexpressive language.

[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

[pozorvlak.livejournal.com]

I dunno... maybe it's because I'm doing mostly mathematical stuff (the integer-parametrized types problem originally arose while I was writing code for manipulating polynomials over finite fields), maybe it's because I'm coming from a highly dynamic language (Perl) or maybe it's just the kind of person I am, but I seem to run up against some problem of this sort almost every time I pick up a Haskell compiler :-) It could also be because I'm still at the stage of playing with the language and hence keep trying to poke it in funny ways to see what it does...

[beelsebob.livejournal.com]

Strange -- I seem to do some fairly similar things, in fact I wrote some code to manipulate polynomials a few weeks ago and didn't hit any problems at all, on the other hand, I'm quite possibly not doing things as complex as you. What representation are you using for your polynomials?

I don't know what you need to use IPTs for, but as far as I've seen IPTs and DTs tend to be used to make type constraints tighter rather than making the type system more expressive. Can you explain the particular problem you need them for?

Bob

[pozorvlak.livejournal.com]

The polynomials concerned had coefficients in finite fields, ie all arithmetic was modulo some prime p. I took the view that it didn't make much sense to add (3 mod 7) to (5 mod 11), and wanted the type system to handle that bit for me. I wasn't doing anything particularly complicated other than that.

I want to have a go at it using the library greg_buchholz linked to now :-)

[greg-buchholz.livejournal.com]

I took the view that it didn't make much sense to add (3 mod 7) to (5 mod 11), and wanted the type system to handle that bit for me.

In that case you might also like: Implicit configurations -- or, type classes reflect the values of types (http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf) (Section 3). And if you are new to computing with types in Haskell, I'd suggest Fun with Functional Dependencies or Types as Values in Static Computations in Haskell (http://www.cs.chalmers.se/~hallgren/Papers/wm01.html) to get you started.

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.

Number-parameterized types

[greg-buchholz.livejournal.com]

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

Re: Number-parameterized types

[pozorvlak.livejournal.com]

Dude. Thanks! I'll check that out...

I'd wondered if it were possible to represent numbers as types, but decided it probably wasn't.

[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

[pozorvlak.livejournal.com]

Excellent. I shall be sure to point and laugh at Duncan next time I see him :-)

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.

[ryani.livejournal.com]

Heh, teach me not to read all the comments before replying :)

[pozorvlak.livejournal.com]

On the other hand, your comment was more detailed and thus more useful :-)