What is a type error?

[Joachim Durchholz]

Chris Smith schrieb:
> David Hopwood <david.nospam.hopwood at blueyonder.co.uk> wrote:
>> Chris Smith wrote:
>>> If checked by execution, yes.  In which case, I am trying to get my head 
>>> around how it's any more true to say that functional languages are 
>>> compilable postconditions than to say the same of imperative languages.
 >>
>> A postcondition must, by definition [*], be a (pure) assertion about the
>> values that relevant variables will take after the execution of a subprogram.
> 
> Okay, my objection was misplaced, then, as I misunderstood the original 
> statement.  I had understood it to mean that programs written in pure 
> functional languages carry no additional information except for their 
> postconditions.

Oh, but that's indeed correct for pure functional languages. (Well, they 
*might* carry additional information anyway, but it's not a requirement 
to make it a programming language.)

The answer that I have for your original objection may be partial, but 
here goes anyway:

Postconditions cannot easily capture all side effects.
E.g. assume there's a file-open routine but no way to test whether a 
given file handle was ever opened (callers are supposed to test the 
return code from the open() call).
In an imperative language, that's a perfectly valid (though possibly not 
very good) library design.
Now the postcondition would have to say something like "from now on, 
read() and write() are valid on the filehandle that I returned". I know 
of no assertion language that can express such temporal relationships, 
and even if there is (I'm pretty sure there is), I'm rather sceptical 
that programmers would be able to write correct assertions, or correctly 
interpret them - temporal logic offers several traps for the unwary. 
(The informal postcondition above certainly isn't complete, since it 
doesn't cover close(); I shunned the effort to get a wording that would 
correctly cover sequences like open()-close()-open(), or 
open()-close()-close()-open().)

Regards,
Jo