Hi folks The main thing I like about type signatures is that they help the computer write the boring bits of my programs for me. I've said it before and I'll say it again, no doubt: when we talk about 'type inference', we should distinguish two aspects: (1) the machine doesn't know your plan and tries to guess it (let-rule style, ie finding the abstraction) (2) the machine does know your plan and is fleshing out the details (var-rule style, ie finding the instantiation) You can only make (1) fully automatic at the cost of compulsory ignorance, dumbing down the collection of possible plans to those which are guessable by a machine. I find this unpleasantly restrictive. I at least want a manual override, which Haskell pretty much provides. But as types get more expressive, it's often the case that you can give your programs much more useful types than the machine is ever going to guess. Possibly even a type which explains what a function's output has to do with its input. You can make (2) very powerful indeed. Even in the conventional batch mode of edit-then-compile, you can use overloading to shift the burden of programming from a large amount of tedious plumbing in the program text to a smaller class constraint in the signature. I often find myself using newtypes to explain which structure of my data I want to exploit, then leaving instance inference to exploit it in the 'obvious' way. There are better reasons to write type signatures than that the compiler is too dumb or that the nuns will whip us if we don't. Type signatures enable chunks of program inference, which is much more useful than aspect (1) of type inference. Types can be seen as a highly expressive and compact language of design statements for both humans and machines to read: this design statement determines the space of essential choices for the programmer, and programming can, if we choose, consist of navigating that space. Machines can map that space out for us, and they can fill in all the no-choice bits and pieces once we decide which way to go. I'm not advocating compulsory refinement editing. I'm saying that type signatures currently feel ephemeral only because today's program-construction tools fail to take positive advantage of the fact that machines can manipulate programs in a typed way. Cheers Conor -- http://www.cs.nott.ac.uk/~ctm