What is a type error?

[Joachim Durchholz]

Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> Now, I'm not fully up to speed on DBC. The contract specifications,
>>> these are specified statically, but checked dynamically, is that
>>> right?
>> That's how it's done in Eiffel, yes.
>>
>>  > In other words, we can consider contracts in light of
>>> inheritance, but the actual verification and checking happens
>>> at runtime, yes?
>> Sure. Though, while DbC gives rules for inheritance (actually subtypes),
>> these are irrelevant to the current discussion; DbC-minus-subtyping can
>> still be usefully applied.
> 
> Yes, subtyping. Of course I meant to say subtyping.<blush>

No need to blush for that, it's perfectly OK in the Eiffel context, 
where a subclass ist always assumed to be a subtype. (This assumption 
isn't always true, which is why Eiffel has some serious holes in the 
type system. The DbC ideas are still useful though, saying "subtype" 
instead of "subclass" just makes the concept applicable outside of OO 
languages.)

> I can certainly see how DbC would be useful without subtyping.
> But would there still be a reason to separate preconditions
> from postconditions? I've never been clear on the point
> of differentiating them (beyond the fact that one's covariant
> and the other is contravariant.)

There is indeed.
The rules about covariance and contravariance are just consequences of 
the notion of having a subtype (albeit important ones when it comes to 
designing concrete interfaces).

For example, if a precondition fails, something is wrong about the 
things that the subroutine assumes about its environment, so it 
shouldn't have been called. This means the error is in the caller, not 
in the subroutine that carries the precondition.

The less important consequence is that this should be reflected in the 
error messages.

The more important consequences apply when integrating software.
If you have a well-tested library, it makes sense to switch off 
postcondition checking for the library routines, but not their 
precondition checking.
This applies not just for run-time checking: Ideally, with compile-time 
inference, all postconditions can be inferred from the function's 
preconditions and their code. The results of that inference can easily 
be stored in the precompiled libraries.
Preconditions, on the other hand, can only be verified by checking all 
places where the functions are called.

>>> Wouldn't it be possible to do them at compile time? (Although
>>> this raises decidability issues.)
>> Exactly, and that's why you'd either uses a restricted assertion
>> language (and essentially get something that's somewhere between a type
>> system and traditional assertion); or you'd use some inference system
>> and try to help it along (not a simple thing either - the components of
>> such a system exist, but I'm not aware of any system that was designed
>> for the average programmer).
> 
> As to the average programmer, I heard this recently on
> comp.databases.theory:
> 
> "Don't blame me for the fact that competent programming, as I view it
> as an intellectual possibility, will be too difficult for "the
> average programmer"  -you must not fall into the trap of rejecting
> a surgical technique because it is beyond the capabilities of the
> barber in his shop around the corner."   -- EWD512

Given the fact that we have far more need for competently-written 
programs than for competent surgery, I don't think that we'll be able to 
follow that idea.

>>> Mightn't it also be possible to
>>> leave it up to the programmer whether a given contract
>>> was compile-time or runtime?
>> I'd agree with that, but I'm not sure how well that would hold up in
>> practice.
> 
> I want to try it and see what it's like.

So do I :-)

Regards,
Jo