[Haskell] Re: Impredicative Types?

[Conor McBride]

Hi

> Ben Rudiak-Gould wrote:
> 
> > ... we can't even determine the meaning of a correct
> > program without looking at explicit type signatures.
> 
Johannes Waldmann wrote:

> So what? Can we do this in other languages?
> Do we want it? I think not.
> 
> The Haskell design (of type inference rather than type checking)
> has the strange feeling of "our types are so strong that
> you can completely avoid (writing) them".
> To me, this seems contrary to sound software engineering.

To a large extent, I would agree with this remark. It seems to
me that

(1) We should write types when we are telling the compiler
      what the plan is.
(2) We should not need to write types (or at least not often)
      to convince the compiler that we are following the
      plan.

Indeed, if one replaces `compiler' in the above by `editor',
one begins to discover that the writing of an explicit
type signature can assist us in determining not merely
the meaning of a correct program, but the program itself.

The writing of explicit type signatures (and in particular,
class constraints) serves more than the practical necessity
of helping a dim computer to cope and more than the moral
purpose of disciplined documentation. It gives programmers
a very compact language for describing a great deal of
tedious plumbing. That's really good.

Types are not and should not be regarded as passive things
which machines check and programmers try to ignore. One only
needs to look at what, in toto, Haskell compilers actually
do with types (let alone what editors could do), to see that
writing a type can be a highly effective act of programming,
and hence that reading types can be a very efficient means
of program comprehension.

It's not types we should be not reading or not writing: it's
the boring bits of programs.

Cheers

Conor