What is a type error?

[Marshall]

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>

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.)


> > 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


>  > 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.


Marshall