What is a type error?

[Marshall]

Chris Smith wrote:
> Marshall <marshall.spight at gmail.com> wrote:
> > Chris Smith wrote:
> > > Darren New <dnew at san.rr.com> wrote:
> > > > Chris Smith wrote:
> > > > > Unless I'm missing your point, I disagree with your disagreement.
> > > > > Mutability only makes sense because of object identity (in the generic
> > > > > sense; no OO going on here).
> > > >
> > > > Depends what you mean by "object".
> > > >
> > > > int x = 6; int y = 5; x = y;
> > > >
> > > > I'd say x was mutable, with no "identity" problems involved?
> > >
> > > The variable x definitely has identity that's independent of its value.
> >
> > I'm not sure what you mean by that.
>
> I mean, simply, that when you can assign a value to a variable, then you
> care that it is that variable and not a different one.  That's identity
> in the normal sense of the word.

I guess it is, now that you mention it.


> The code elsewhere in the procedure is
> able to access the value of 'x', and that has meaning even though you
> don't know what value 'x' has.  This has definite implications, and is a
> useful concept; for example, it means that the pure lambda calculus no
> longer sufficient to express the semantics of the programming language,
> but instead something else is required.
>
> What you are asking for is some subset of identity, and I've not yet
> succeeded in understanding exactly what it is or what its limits are...
> except that so far, it seems to have everything to do with pointers or
> aliasing.

Perhaps it is specifically first-class identity, rather than identity
per se.


> > >  I also see, though, that the majority (so far, I'd
> > > say all) of the potential uses for which it's worth introducing mutation
> > > into an otherwise mutation-free language allow the possibility of
> > > aliasing, which sorta makes me wonder whether this problem is worth
> > > solving.
> >
> > What about my example of SQL? Mutation, no pointers, no aliasing.
> > Yet: useful.
>
> I'm not yet convinced that this is any different from a language with
> standard pointer aliasing.  If I have two tables A and B, and a foreign
> key from A into B, then I run into the same problems with enforcing
> constraints that I would see with a pointer model... when I update a
> relation, I need to potentially check every other relation that contains
> a foreign key into it, in order to ensure that its constraints are not
> violated by that constraint.  That's the same thing that is being
> pointed out as a negative consequence of aliasing in other languages.

No, that's not the same thing. What you are describing here is
not an aliasing issue, but simply the consequences of allowing
constraints to mention more than one variable.

In our i-and-j example above, suppose there was a constraint
such that i < j. We have to re-check this constraint if we
update either i or j. That's not the same thing as saying
that i and j are aliased.

A foreign key constraint is a multi-variable constraint.
Specifically, a foreign key from table A, attribute a
to table B, attribute b is the constraint:

forall a in A, exists b in B such that a = b.

Note that two variables, A and B, are referenced in
the constraint. In general, any constraint on two
variables will have to be rechecked upon update
to either.


> For example, executing:
>
>     UPDATE P SET x = 5 WHERE y = 43;
>
> may result in the database having to re-evaluate the constraint that
> says that for all P(x, y, z), x must be less than 4 when z = 17.

I don't see any aliasing in this example either.

But consider how much worse this problem is if real aliasing
is possible. We have some pointer variable, and initialize
it with the return value from some function. We don't know
anything about what variable is involved. We update through
the pointer. What constraints must we recheck? Apparently
all of them; unless we have perfect alias analysis, we can't
tell what variables are affected by our update.


> One
> difference is that while in general purpose programming languages this
> appears to be a daunting task, databases are set up to do these kinds of
> things all the time and contain optimizations for it... but the problem
> is still the same, and it would still present the same difficulties in
> doing formal proofs that running the above UPDATE statement doesn't
> violate any invariants.
>
> (If I'm wrong about that, please let me know; I'd very interested if
> that's so.)

I'm interested to hear your reply.


Marshall