[Haskell-cafe] Signature of a function

[Conor McBride]

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