What is a type error?

[David Hopwood]

Chris Smith wrote:
> At the same time, though, maybe I do want 
> the compiler to infer that tax cannot be negative (or maybe it can; I'm 
> not an accountant; I know my tax has never been negative), [...]

Tax can be negative, e.g. when a business is claiming back VAT (sales tax)
on its purchases, but the things it is selling have lower-rated or zero
VAT (or it is making a loss).

> Note that even without encapsulation, the kind of typing information 
> we're looking at can be very non-trivial in an imperative language.  For 
> example, I may need to express a method signature that is kind of like 
> this:
> 
> 1. The first parameter is an int, which is either between 4 and 8, or 
> between 11 and 17.
> 
> 2. The second parameter is a pointer to an object, whose 'foo' field is 
> an int between 0 and 5, and whose 'bar' field is a pointer to another 
> object with three fields 'a', 'b', and 'c', each of which has the full 
> range of an unconstrained IEEE double precision floating point number.
> 
> 3. After the method returns, it will be known that if this object 
> previously had its 'baz' field in the range m .. n, it is now in the 
> range (m - 5) .. (n + 1).
> 
> 4. After the method returns, it will be known that the object reached by 
> following the 'bar' field of the second parameter will be modified so 
> that the first two of its floating point numbers are guaranteed to be of 
> the opposite sign as they were before, and that if they were infinity, 
> they are now finite.
> 
> 5. After the method returns, the object referred to by the global 
> variable 'zab' has 0 as the value of its 'c' field.
> 
> Just expressing all of that in a method signature looks interesting 
> enough.  If we start adding abstraction to the type constraints on 
> objects to support encapsulation (as I think you'd have to do), then 
> things get even more interesting.

1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>