What is a type error?

[Chris Smith]

Marshall <marshall.spight at gmail.com> wrote:
> Chris Smith wrote:
> >
> > But this starts to look bad, because we used to have this nice property
> > called encapsulation.  To work around that, we'd need to make one of a
> > few choices: (a) give up encapsulation, which isn't too happy; (b) rely
> > on type inference for this kind of stuff, and consider it okay if the
> > type inference system breaks encapsulation; or (c) invent some kind of
> > generic constraint language so that constraints like this could be
> > expressed without exposing field names.  Choice (b) is incomplete, as
> > there will often be times when I need to ascribe a type to a parameter
> > or some such thing, and the lack of ability to express the complete type
> > system will be rather limiting.  Choice (c), though, looks a little
> > daunting.
> 
> Damn the torpedoes, give me choice c!

You and I both need to figure out when to go to sleep.  :)  Work's gonna 
suck tomorrow.

> I've been saying for a few years now that encapsulation is only
> a hack to get around the lack of a decent declarative constraint
> language.

Choice (c) was meant to preserve encapsulation, actually.  I think 
there's something fundamentally important about information hiding that 
can't be given up.  Hypothetically, say I'm writing an accounting 
package and I've decided to encapsulate details of the tax code into one 
module of the application.  Now, it may be that the compiler can perform 
sufficient type inference on my program to know that it's impossible for 
my taxes to be greater than 75% of my annual income.  So if my income is 
stored in a variable of type decimal{0..100000}, then the return type of 
getTotalTax may be of type decimal{0..75000}.  Type inference could do 
that.

But the point here is that I don't WANT the compiler to be able to infer 
that, because it's a transient consequence of this year's tax code.  I 
want the compiler to make sure my code works no matter what the tax code 
is.  The last thing I need to to go fixing a bunch of bugs during the 
time between the release of next year's tax code and the released 
deadline for my tax software.  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), and that it 
can't be a complex number (I'm pretty sure about that one).  I call that 
encapsulation, and I don't think that it's necessary for lack of 
anything; but rather because that's how the problem breaks down.

----

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

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation