What is a type error?

[Marshall]

Chris Smith wrote:
> 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.

It's never been a strong point. Made worse now that my daughter
is one of those up-at-the-crack-of-dawn types, and not old enough
to understand why it's not nice to jump on mommy and daddy's
bed while they're still asleep. But aren't you actually a time zone
or two east of me?


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

The fields of an object/struct/what have you are often hidden behind
a method-based interface (sometimes callled "encapsulated") only
because we can't control their values otherwise. (The "exposing
the interface" issue is a non-issue, because we're exposing some
interface or another no matter what.) The issue is controlling the
values, and that is better handled with a declarative constraint
language. The specific value in the fields aren't known until
runtime.

However for a function, the "fields" are the in and out parameters.
The specific values in the relation that the function is aren't known
until runtime either, (and then only the subset for which we actually
perform computation.)

Did that make sense?


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

There's some significant questions in my mind about how much of
a constraint language would be static and how much would be
runtime checks. Over time, I'm starting to feel like it should be
mostly runtime, and only occasionally moving into compile time
at specific programmer request. The decidability issue comes up.

Anyone else?


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

There are certainly syntactic issues, but I believe these are amenable
to the usual approaches. The runtime/compile time question, and
decidability seem bigger issues to me.


Marshall