What is a type error?

java-programmer, What is a type error? Marshall <email***@***.com> wrote:
> David Hopwood wrote:
> > Marshall wrote:

> > > Mightn't it also be possible to
> > > leave it up to the programmer whether a given contract
> > > was compile-time or runtime?
> >
> > That would be possible, but IMHO a better option would be for an IDE to give
> > an indication (by highlighting, for example), which contracts are dynamically
> > checked and which are static.
> >
> > This property is, after all, not something that the program should depend on.
> > It is determined by how good the static checker currently is, and we want to be
> > able to improve checkers (and perhaps even allow them to regress slightly in
> > order to simplify them) without changing programs.
>
> Hmmm. I have heard that argument before and I'm conflicted.
>
> I can think of more reasons than just runtime safety for which I'd
> want proofs. Termination for example, in highly critical code;
> not something for which a runtime check will suffice. On the
> other hand the points you raise are good ones, and affect
> the usability of the language.

There doesn't seem to be a point of disagreement here. Programmers
often need to require certain properties to be checked at compile-time.
Others could go either way. There is no property that a program would
rationally desire to *require* be checked at runtime; that would only
occur because the compiler doesn't know how to check it at compile time.

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

java-programmer >> What is a type error? Marshall <email***@***.com> wrote:
> David Hopwood wrote:
> > Marshall wrote:

> > > Mightn't it also be possible to
> > > leave it up to the programmer whether a given contract
> > > was compile-time or runtime?
> >
> > That would be possible, but IMHO a better option would be for an IDE to give
> > an indication (by highlighting, for example), which contracts are dynamically
> > checked and which are static.
> >
> > This property is, after all, not something that the program should depend on.
> > It is determined by how good the static checker currently is, and we want to be
> > able to improve checkers (and perhaps even allow them to regress slightly in
> > order to simplify them) without changing programs.
>
> Hmmm. I have heard that argument before and I'm conflicted.
>
> I can think of more reasons than just runtime safety for which I'd
> want proofs. Termination for example, in highly critical code;
> not something for which a runtime check will suffice. On the
> other hand the points you raise are good ones, and affect
> the usability of the language.

There doesn't seem to be a point of disagreement here. Programmers
often need to require certain properties to be checked at compile-time.
Others could go either way. There is no property that a program would
rationally desire to *require* be checked at runtime; that would only
occur because the compiler doesn't know how to check it at compile time.

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

java-programmer >> What is a type error? Marshall wrote:
>
> Okay, sure. But for the problem you describe, both imperativeness
> and the presence of pointers is each necessary but not sufficient;
> it is the two together that causes the problem. So it strikes
> me (again, a very minor point) as inaccurate to describe this as
> a problem with imperative languages per se.
>
> [...]
>
> Right. To me the response to this clear: give up pointers. Imperative
> operations are too useful to give up; indeed they are a requirement
> for certain problems. Pointers on the other hand add nothing except
> efficiency and a lot of confusion. They should be considered an
> implementation technique only, hidden behind some pointerless
> computational model.

Don't get yourself distracted by the low-level notion of "pointer". The
problem *really* is mutability and the associated notion of identity,
which explicit pointers just exhibit on a very low level.

When you have a language with mutable types (e.g. mutable arrays) then
objects of these types have identity, which is observable through
assignment. This is regardless of whether identity is an explicit
concept (like it becomes with pointers and comparison of pointer values,
i.e. addresses).

Consequently, you cannot possibly get rid of aliasing issues without
getting rid of (unrestricted) mutability. Mutability implies object
identity implies aliasing problems.

On the other hand, pointers are totally a futile concept without
mutability: if everything is immutable, it is useless to distinguish
between an object and a pointer to it.

In other words, pointers are essentially just an *aspect* of mutability
in lower-level languages. On a sufficiently high level of abstraction,
it does not make much sense to differentiate between both concepts -
pointers are just mutable objects holding other mutable objects
(immutable pointer types exist, but are only interesting if you also
have pointer arithmetics - which, however, is largely equivalent to
arrays, i.e. not particularly relevant either).

- Andreas

java-programmer >> What is a type error? Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> Joachim Durchholz wrote:
>>>> Marshall schrieb:
>>>>> I can see the lack of a formal model being an issue, but is the
>>>>> imperative bit really all that much of an obstacle? How hard
>>>>> is it really to deal with assignment? Or does the issue have
>>>>> more to do with pointers, aliasing, etc.?
>>>> Actually aliasing is *the* hard issue.
>>> Okay, sure. Nice explanation.
>>>
>>> But one minor point: you describe this as an issue with "imperative"
>>> languages. But aliasing is a problem associated with pointers,
>>> not with assignment.
>> Aliasing is not a problem if the aliased data is immutable.
>
> Okay, sure. But for the problem you describe, both imperativeness
> and the presence of pointers is each necessary but not sufficient;
> it is the two together that causes the problem. So it strikes
> me (again, a very minor point) as inaccurate to describe this as
> a problem with imperative languages per se.

Sure.
It's just that I know that it's viable to give up destructive updates.
Giving up pointers is a far more massive restriction.

> Right. To me the response to this clear: give up pointers. Imperative
> operations are too useful to give up; indeed they are a requirement
> for certain problems.

I don't know any.
In some cases, you need an additional level of conceptual indirection -
instead of *doing* the updates, you write a function that *describes* them.

> Pointers on the other hand add nothing except
> efficiency and a lot of confusion. They should be considered an
> implementation technique only, hidden behind some pointerless
> computational model.
>
> I recognize that this is likely to be a controversial opinion.

Indeed.

In fact "modes" are a way to restrict pointer aliasing.

> I heartily support immutability as the default, for these and other
> reasons.

OK, then we're in agreement here.

>> Some functional languages restrict assignment so that there can exist at
>> most a single reference to any mutable data structure. That way, there's
>> still no aliasing problems, but you can still update in place where it's
>> really, really necessary.
>
> Are we speaking of uniqueness types now? I haven't read much about
> them, but it certainly seems like an intriguing concept.

Yup.
It's called "modes" in some other languages (Mercury or Clean IIRC).

>> I know of no professional language that doesn't have references of some
>> kind.
>
> Ah, well. I suppose I could mention prolog or mercury, but then
> you used that troublesome word "professional." So I will instead
> mention a language which, if one goes by number of search results
> on hotjobs.com for "xxx progammer" for different value of xxx, is
> more popular than Java and twice as popular as C++. It lacks
> pointers (although I understand they are beginning to creep in
> in the latest version of the standard.) It also posesses a quite
> sophisticated set of facilities for declarative integrity constraints.
> Yet for some reason it is typically ignored by language designers.
>
> http://hotjobs.yahoo.com/jobseeker/jobsearch/search_results.html?keywords_all=sql+programmer

Oh, right. SQL is an interesting case of getting all the problems of
pointers without having them ;-)

Actually SQL has references - they are called "primary keys", but they
are references nevertheless. (Some SQL dialects also offer synthetic
"ID" fields that are guaranteed to remain stable over the lifetime of a
record. Seems like SQL is imperative enough that programmers want this,
else the SQL vendors wouldn't have added the feature...)
SQL also has updates.
The result: updates with undefined semantics. E.g. if you have a numeric
key field, UPDATE commands that increment the key by 1 will fail or work
depending on the (unspecified) order in which UPDATE touches the
records. You can have even more fun with updatable views.
With a "repeatable read" isolation level, you actually return to a
declarative view of the database: whatever you do with it, you won't see
it until you commit the transaction. (As soon as you commit, the
declarative peace is over and you better watch out that your data
doesn't become inconsistent due to aliasing.)

Aliasing isn't really related to specific programming practices. If two
accountants chat, and one talks about the hot blonde secretaire and the
other about his adorable wife, you can imagine the awkwardness that
ensues as soon as they find out they're talking about the same person!
The only thing that can really be done about it is not adding it
artificially into a program. In those cases where aliasing is part of
the modelled domain, you really have to carefully inspect all
interactions and never, never, never dream about abstracting it away.

Regards,
Jo

java-programmer >> What is a type error? Darren New schrieb:
> Joachim Durchholz wrote:
>> Actually, in a functional programming language (FPL), you write just
>> the postconditions and let the compiler generate the code for you.
>
> Certainly. And my point is that the postcondition describing "all valid
> chess boards reachable from this one" is pretty much going to be as big
> as an implementation for generating it, yes?

Yes. It's a classical case where the postcondition and the code that
fulfils it are essentially the same.

> The postcondition will
> still have to contain all the rules of chess in it, for example. At best
> you've replaced loops with some sort of universal quanitifier with a
> "such that" phrase.

Correct.

OTOH, isn't that the grail that many people have been searching for:
programming by simply declaring the results that they want to see?

> Anyway, I expect you could prove you can't do this in the general case.
> Otherwise, you could just write a postcondition that asserts the output
> of your function is machine code that when run generates the same
> outputs as the input string would. I.e., you'd have a compiler that can
> write other compilers, generated automatically from a description of the
> semantics of the input stream and the semantics of the machine the code
> is to run on. I'm pretty sure we're not there yet, and I'm pretty sure
> you start running into the limits of computability if you do that.

No, FPLs are actually just that: compilable postconditions.
Computability issues aren't more or less a factor than with other kinds
of compilers: they do limit what you can do, but these limits are loose
enough that you can do really useful stuff within them (in particular,
express all algorithms).

Regards,
Jo

java-programmer >> What is a type error? Marshall schrieb:
> David Hopwood wrote:
>> This property is, after all, not something that the program should depend on.
>> It is determined by how good the static checker currently is, and we want to be
>> able to improve checkers (and perhaps even allow them to regress slightly in
>> order to simplify them) without changing programs.
>
> Hmmm. I have heard that argument before and I'm conflicted.

I'd want several things.

A way for me to indicate what assertions must be proven statically.
Highlighting (be it compiler messages or flashing colors in an IDE) that
marks assertions that *will* break.
And highlighting for assertions that *may* break.
In the language, a (possibly) simplicistic inference engine definition
that gives me minimum guarantees about the things that it will be able
to prove; if something is out of the reach of the engine, a
straightforward way to add intermediate assertions until the inference
succeeds.

(Plus diagnostics that tell me where the actual error may be, whether
it's a bug in the code or an omission in the assertions. That's probably
the hardest part of it all.)

Regards,
Jo

java-programmer >> What is a type error? Andreas Rossberg wrote:
> Marshall wrote:
> >
> > Okay, sure. But for the problem you describe, both imperativeness
> > and the presence of pointers is each necessary but not sufficient;
> > it is the two together that causes the problem. So it strikes
> > me (again, a very minor point) as inaccurate to describe this as
> > a problem with imperative languages per se.
> >
> > [...]
> >
> > Right. To me the response to this clear: give up pointers. Imperative
> > operations are too useful to give up; indeed they are a requirement
> > for certain problems. Pointers on the other hand add nothing except
> > efficiency and a lot of confusion. They should be considered an
> > implementation technique only, hidden behind some pointerless
> > computational model.
>
> Don't get yourself distracted by the low-level notion of "pointer". The
> problem *really* is mutability and the associated notion of identity,
> which explicit pointers just exhibit on a very low level.
>
> When you have a language with mutable types (e.g. mutable arrays) then
> objects of these types have identity, which is observable through
> assignment. This is regardless of whether identity is an explicit
> concept (like it becomes with pointers and comparison of pointer values,
> i.e. addresses).

Hmmm, well, I cannot agree. You've defined away the pointers
but then slipped them back in again by assumption ("objects
of these types have identity".)

First let me say that the terminology is somewhat problematic.
For the specific issue being discussed here, pointers, identity,
and objects are all the same concept. (I agree that "pointer"
connotes a low-level construct, however.) Sometimes I think
of this issue as being one with first class variables. An object
with mutable fields is a variable, and if we have pointers or
references or any way to have two different pathways to
that object/those variables, then we run in to the aliasing problem.

However if the mutable types are not first class, then there
is no way to have the aliasing. Thus, if we do not have pointers
or objects or identity but retain mutability, there is no aliasing
problem.

> Consequently, you cannot possibly get rid of aliasing issues without
> getting rid of (unrestricted) mutability. Mutability implies object
> identity implies aliasing problems.

Mutability by itself does not imply identity. I agree that mutability
plus
identity implies aliasing problems, however.

> On the other hand, pointers are totally a futile concept without
> mutability: if everything is immutable, it is useless to distinguish
> between an object and a pointer to it.

Agreed.

> In other words, pointers are essentially just an *aspect* of mutability
> in lower-level languages.

Again, I disagree: it is posible to have mutability without
pointers/identity/objects.

Marshall

java-programmer >> What is a type error? Marshall wrote:
>
> However if the mutable types are not first class, then there
> is no way to have the aliasing. Thus, if we do not have pointers
> or objects or identity but retain mutability, there is no aliasing
> problem.

Yes, technically you are right. But this makes a pretty weak notion of
mutability. All stateful data structures had to stay within their
lexical scope, and could never be passed to a function. For example,
this essentially precludes object-oriented programming, because you
could not have objects with state (the alternative, second class
objects, would be even less "objective").

Generally, second-classness is an ad-hoc restriction that can work
around all kinds of problems, but rarely with satisfactory results. So I
would tend to say that this is not an overly interesting point in the
design space. But YMMV.

>>In other words, pointers are essentially just an *aspect* of mutability
>>in lower-level languages.
>
> Again, I disagree: it is posible to have mutability without
> pointers/identity/objects.

OK, if you prefer: it is an aspect of first-class mutability - which is
present in almost all imperative languages I know. :-)

- Andreas

--
Andreas Rossberg, email***@***.com

java-programmer >> What is a type error? Joachim Durchholz wrote:
> Marshall schrieb:
> > Joachim Durchholz wrote:
> >> Marshall schrieb:
> >>> Joachim Durchholz wrote:
> >>>> Marshall schrieb:
> >>>>> I can see the lack of a formal model being an issue, but is the
> >>>>> imperative bit really all that much of an obstacle? How hard
> >>>>> is it really to deal with assignment? Or does the issue have
> >>>>> more to do with pointers, aliasing, etc.?
> >>>> Actually aliasing is *the* hard issue.
> >>> Okay, sure. Nice explanation.
> >>>
> >>> But one minor point: you describe this as an issue with "imperative"
> >>> languages. But aliasing is a problem associated with pointers,
> >>> not with assignment.
> >> Aliasing is not a problem if the aliased data is immutable.
> >
> > Okay, sure. But for the problem you describe, both imperativeness
> > and the presence of pointers is each necessary but not sufficient;
> > it is the two together that causes the problem. So it strikes
> > me (again, a very minor point) as inaccurate to describe this as
> > a problem with imperative languages per se.
>
> Sure.
> It's just that I know that it's viable to give up destructive updates.
> Giving up pointers is a far more massive restriction.

Oddly, I feel the opposite. While it's true there are many domains
for which purely functional programming is a fine choice, there
are some domains for which it is insufficient. Any kind of data
managament, for example, requires that you be able to update
the information.

On the other hand, there is no problem domain for which pointers
are a requirement. I agree they are deucedly convenient, though.

> > Right. To me the response to this clear: give up pointers. Imperative
> > operations are too useful to give up; indeed they are a requirement
> > for certain problems.
>
> I don't know any.
> In some cases, you need an additional level of conceptual indirection -
> instead of *doing* the updates, you write a function that *describes* them.

But then what do you do with that function? Let's say I have an
employee database. John Smith just got hired on 1/1/2006 with
a salary of $10,000. I need to record this fact somewhere. How
do I do that without variables? Current-employees is a variable.
Even if I have the space to keep all historical data, so I'm not
deleting anything, I still have to have a variable for the latest
version of the accumulated data. I can solve this without
pointers, but I can't solve it without variables.

> > Pointers on the other hand add nothing except
> > efficiency and a lot of confusion. They should be considered an
> > implementation technique only, hidden behind some pointerless
> > computational model.
> >
> > I recognize that this is likely to be a controversial opinion.
>
> Indeed.
>
> In fact "modes" are a way to restrict pointer aliasing.

I should like to learn more about these. I have some vague
perception of the existence of linear logic, but not much
else. However, I also already have an excellent solution
to the pointer aliasing problem, so I'm less motivated.

> > I heartily support immutability as the default, for these and other
> > reasons.
>
> OK, then we're in agreement here.
>
> >> Some functional languages restrict assignment so that there can exist at
> >> most a single reference to any mutable data structure. That way, there's
> >> still no aliasing problems, but you can still update in place where it's
> >> really, really necessary.
> >
> > Are we speaking of uniqueness types now? I haven't read much about
> > them, but it certainly seems like an intriguing concept.
>
> Yup.
> It's called "modes" in some other languages (Mercury or Clean IIRC).

Cool.

> >> I know of no professional language that doesn't have references of some
> >> kind.
> >
> > Ah, well. I suppose I could mention prolog or mercury, but then
> > you used that troublesome word "professional." So I will instead
> > mention a language which, if one goes by number of search results
> > on hotjobs.com for "xxx progammer" for different value of xxx, is
> > more popular than Java and twice as popular as C++. It lacks
> > pointers (although I understand they are beginning to creep in
> > in the latest version of the standard.) It also posesses a quite
> > sophisticated set of facilities for declarative integrity constraints.
> > Yet for some reason it is typically ignored by language designers.
> >
> > http://hotjobs.yahoo.com/jobseeker/jobsearch/search_results.html?keywords_all=sql+programmer
>
> Oh, right. SQL is an interesting case of getting all the problems of
> pointers without having them ;-)

Oh, pooh. SQL has plenty of problems, sure, but the problems
of pointers are not among its faults.

> Actually SQL has references - they are called "primary keys", but they
> are references nevertheless.

I strongly object; this is quite incorrect. I grant you that from the
50,000 foot level they appear identical, but they are not. To
qualify as a reference, there need to be reference and dereference
operations on the reference datatype; there is no such operation
is SQL.

Would you say the relational algebra has references?

Or, consider the classic prolog ancestor query. Let's say we're
setting up as follows

father(bob, joe).
father(joe, john).

Is "joe" a reference, here? After all, when we do the ancestor
query for john, we'll see his father is joe and then use that to
find joe's father. Keys in SQL are isomorphic to joe in the
above prolog.

> (Some SQL dialects also offer synthetic
> "ID" fields that are guaranteed to remain stable over the lifetime of a
> record.

Primary keys are updatable; there is nothing special about them.

> Seems like SQL is imperative enough that programmers want this,
> else the SQL vendors wouldn't have added the feature...)

I believe you are making a statement about the general level of
education among the user base of data base management systems,
and not a statement about the nature of the relational algebra.

> SQL also has updates.

Yes; SQL is imperative. But no pointers and thus no aliasing.
Plenty of *other* problems, though; no argument there!

> The result: updates with undefined semantics. E.g. if you have a numeric
> key field, UPDATE commands that increment the key by 1 will fail or work
> depending on the (unspecified) order in which UPDATE touches the
> records.

This does not sound correct to me, and in any event does not
appear to illustrate anything about aliasing.

> You can have even more fun with updatable views.

I suppose. Views are something for which the practice has
rushed ahead of the theoretical foundation out of need. The
"right" way to do views is not yet known. Again: plenty of
problems with SQL, but no aliasing. (Actually, there probably
is aliasing with SQL99, since IIUC they've gone ahead and
introduced reference types. (Cue Charlton Heston on the beach
saying "You Maniacs! You blew it up! Ah, damn you!"))

> With a "repeatable read" isolation level, you actually return to a
> declarative view of the database: whatever you do with it, you won't see
> it until you commit the transaction. (As soon as you commit, the
> declarative peace is over and you better watch out that your data
> doesn't become inconsistent due to aliasing.)

Alas, transaction isolation levels are a performance hack.
I cannot defend them on any logical basis. (Aside: did you mean
serializable, rather than repeatable read?)

> Aliasing isn't really related to specific programming practices. If two
> accountants chat, and one talks about the hot blonde secretaire and the
> other about his adorable wife, you can imagine the awkwardness that
> ensues as soon as they find out they're talking about the same person!

Heh, that's not aliasing. That's the undecidability of intentional
function equivalence. <joke>

> The only thing that can really be done about it is not adding it
> artificially into a program. In those cases where aliasing is part of
> the modelled domain, you really have to carefully inspect all
> interactions and never, never, never dream about abstracting it away.

Yes, aliasing introduces a lot of problems. This is one reason
why closures make me nervous.

Marshall

java-programmer >> What is a type error? Andreas Rossberg wrote:
> Yes, technically you are right. But this makes a pretty weak notion of
> mutability. All stateful data structures had to stay within their
> lexical scope, and could never be passed to a function.

Not really. The way Hermes handles this is with destructive assignment.
Each variable holds a value, and you (almost) cannot have multiple
variables referring to the same value.

If you want to assign Y to X, you use
X := Y
after which Y is considered to be uninitialized. If you want X and Y to
have the same value, you use
X := copy of Y
after which X and Y have the same value but are otherwise unrelated, and
changes to one don't affect the other.

(As almost an aside, the non-scalar data structures were very similar to
SQL data tables.)

If you declare (the equivalent to) a function, you can indicate whether
the paramters matching the arguments are passed destructively, or are
read-only, or are copy-in-copy-out. So you could declare a function, for
example, that you pass a table into, and if it's marked as a read-only
parameter, the compiler ensures the callee does not modify the table and
the compiler generates code to pass a pointer. One could also mark a
variable (for example) as uninitialized on entry, intialized on return,
and uninitalized on the throw of an exception, and this could be used
(for example) for the read-a-line-from-a-socket routine.

The only value that came close to being shared is an outgoing connection
to a procedure; the equivalent of the client side of a socket. For
these, you could make copies, and each copy would point to the same
receiver. The receiving process could change over time, by passing its
end of the socket in a message to some other process (live code
upgrading, for example).

Since everything could be passed as part of a message, including code,
procedures, tables, and "inports" and "outports" (the ends of sockets),
I don't see that it had any problems with first classness.

> OK, if you prefer: it is an aspect of first-class mutability - which is
> present in almost all imperative languages I know. :-)

I disagree. It's entirely possible to make sophisticated imperitive
languages with assignment and without aliasing.

--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.

java-programmer >> What is a type error? Joachim Durchholz <email***@***.com> wrote:
> OTOH, isn't that the grail that many people have been searching for:
> programming by simply declaring the results that they want to see?

Possibly.

> No, FPLs are actually just that: compilable postconditions.

This seems to me a bit misleading. Perhaps someone will explain why I
should stop thinking this way; but currently I classify statements like
this in the "well, sort of" slot of my mind. If functional programming
were really just compilable postconditions, then functional programmers
would be able to skip a good bit of stuff that they really can't. For
example, time and space complexity of code is still entirely relevant
for functional programming. I can't simply write:

(define fib
(lambda (x) (if (< x 2) 1 (+ (fib (- x 1)) (fib (- x 2))))))

and expect the compiler to create an efficient algorithm for me. This
is true even though the above is (the LISP transcription of) the most
natural way to describe the fibonacci sequence from a mathematical
standpoint. It still runs in exponential time, and it still matters
that it runs in exponential time; and LISP programmers adapt their so-
called declarative code to improve time bounds all the time. This makes
it harder for me to call it declarative (or "compilable postconditions")
and feel entirely honest.

(Yes, I realize that the above could be optimized in a language that
does normal order evaluation with common subexpression elimination. and
become linear-time. However, that's not true of algorithms in general.
It is not the case that all that's needed to find an efficient algorithm
for something is to plug it into a Haskell compiler and observe what
happens. Or, if that is the case, there are a few CS professors I know
who would be quite interested in hearing so.)

> Computability issues aren't more or less a factor than with other kinds
> of compilers: they do limit what you can do, but these limits are loose
> enough that you can do really useful stuff within them (in particular,
> express all algorithms).

Is it really consistent to say that postconditions allow you to express
algorithms?

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

java-programmer >> What is a type error? Marshall schrieb:
> Mutability by itself does not imply identity.

Well, the implication certainly holds from identity to mutability.
The only definition of identity that I found to hold up for all kinds of
references (pointers, shared-memory identifiers, URLs etc.) is this:

Two pieces of data are identical if and only if:
a) they are equal
b) they stay equal after applying an arbitrary operation to one of them.

This means that for immutable objects, there's no observable difference
between equality and identity (which I think it just fine).

For the implicaton from mutability to identity, I'm not sure whether
talking about mutation still makes sense without some kind of identity.
For example, you need to establish that the object after the mutation is
still "the same" in some sense, and this "the same" concept is exactly
identity.

> I agree that mutability
> plus identity implies aliasing problems, however.

Then we're agreeing about the most important point anyway.

>> In other words, pointers are essentially just an *aspect* of mutability
>> in lower-level languages.
>
> Again, I disagree: it is posible to have mutability without
> pointers/identity/objects.

I'm sceptical.
Any examples?

Regards,
Jo

java-programmer >> What is a type error? Marshall <email***@***.com> wrote:
> Hmmm, well, I cannot agree. You've defined away the pointers
> but then slipped them back in again by assumption ("objects
> of these types have identity".)
>
> First let me say that the terminology is somewhat problematic.
> For the specific issue being discussed here, pointers, identity,
> and objects are all the same concept. (I agree that "pointer"
> connotes a low-level construct, however.)

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). Without object identities, mutability is
useless. What's the use of changing something if you're not sure you'll
ever be able to find it again?

You may limit the scope of object identity arbitrarily, even to the
point that aliasing is impossible (though with lexical closure, that
gets even more limiting than it may first appear)... but you're just
trading off power for simplicity, and the really interesting uses of
mutations are those that allow access to specific objects from any
number different bits of code, on a program-wide or at least module-wide
scope. Most mediocre programmers could replace assignment with
recursion if that assignment is limited to local variables of a single
subroutine. I don't necessarily agree that the result will be a better
program despite others' conviction on the matter; however, the
difference certainly isn't worth complicating the language with mutation
unless you're willing to allow the interesting uses of mutation as well.

> Mutability by itself does not imply identity. I agree that mutability
> plus identity implies aliasing problems, however.

We might have a terminological issue, then. I'd tend to say that
mutability definitely does imply identity, but identity doesn't imply
aliasing. Same difference.

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

java-programmer >> What is a type error? 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?

Why is it problematic that variables have identity and are mutable?
Certainly I can later "find" whatever value I put into x.

--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.

java-programmer >> What is a type error?
Marshall wrote:
>
> Again, I disagree: it is posible to have mutability without
> pointers/identity/objects.

I think you are wrong, but before I make a complete ass out of myself,
I have to ask what you mean by `mutability'. (And
pointers/identity/objects, for that matter.)

Alan Bawden discusses the phenomenon of `state' in his Ph.D.
dissertation "Implementing Distributed Systems Using Linear Naming".
MIT AI Lab Technical Report AITR-1627. March 1993 He makes a
persuasive argument that `state' is associated with cycles in naming.

java-programmer >> What is a type error? Marshall wrote:
> David Hopwood wrote:
>>Marshall wrote:
>>
>>>Wouldn't it be possible to do them at compile time? (Although
>>>this raises decidability issues.)
>>
>>It is certainly possible to prove statically that some assertions cannot fail.
>>
>>The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/docs.html)
>>tool for JML (http://www.cs.iastate.edu/~leavens/JML/) is one system that does
>>this -- although some limitations and usability problems are described in
>><http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/papers/CASSIS2004.pdf>.
>
> I look forward to reading this. I read a paper on JML a while ago and
> found it quite interesting.
>
>>>Mightn't it also be possible to
>>>leave it up to the programmer whether a given contract
>>>was compile-time or runtime?
>>
>>That would be possible, but IMHO a better option would be for an IDE to give
>>an indication (by highlighting, for example), which contracts are dynamically
>>checked and which are static.
>>
>>This property is, after all, not something that the program should depend on.
>>It is determined by how good the static checker currently is, and we want to be
>>able to improve checkers (and perhaps even allow them to regress slightly in
>>order to simplify them

.. or improve their performance ..

> ) without changing programs.
>
> Hmmm. I have heard that argument before and I'm conflicted.
>
> I can think of more reasons than just runtime safety for which I'd
> want proofs. Termination for example, in highly critical code;
> not something for which a runtime check will suffice.

It is true that some properties cannot be verified directly by a runtime check,
but that does not mean that runtime checks are not indirectly useful in verifying
them.

For example, we can check at runtime that a loop variant is strictly decreasing
with each iteration. Then, given that each iteration of the loop body terminates,
it is guaranteed that the loop terminates, *either* because the runtime check
fails, or because the variant goes to zero.

In general, we can verify significantly more program properties using a
combination of runtime checks and static proof, than we can using static proof
alone. That may seem like quite an obvious statement, but the consequence is
that any particular property is, in general, not verified purely statically or
purely at runtime.

I am not opposed to being able to annotate an assertion to say that it should
be statically provable and that a runtime check should not be used. However,

- such annotations should be very lightweight and visually undistracting,
relative to the assertion itself;

- a programmer should not interpret such an annotation on a particular assertion
to mean that its static validity is not reliant on runtime checks elsewhere;

- if the class of assertions that are statically provable changes, then a
tool should be provided which can *automatically* add or remove these
annotations (with programmer approval when they are removed).

I'd like to make a couple more comments about when it is sufficient to detect
errors and when it is necessary to prevent them:

- If a language supports transactions, then this increases the proportion
of cases in which it is sufficient to detect errors in imperative code.
When state changes are encapsulated in a transaction, it is much easier
to recover if an error is detected, because invariants that were true of
objects used by the transaction when it started will be automatically
reestablished. (Purely functional code does not need this.)

- Almost all safety-critical systems have a recovery or safe shutdown
behaviour which should be triggered when an error is detected in the
rest of the program. The part of the program that implements this behaviour
definitely needs to be statically correct, but it is usually only a small
amount of code.

Safety-critical systems that must either prevent errors or continue
functioning in their presence (aircraft control systems, for example) are
in a separate category that demand *much* greater verification effort. Even
for these systems, though, it is still useful to detect errors in cases
where they cannot be prevented. When multiple independent implementations
of a subsystem are used to check each other, this error detection can be
used as an input to the decision of which implementation is failing and
which should take over.

--
David Hopwood <email***@***.com>

java-programmer >> What is a type error? Chris Smith wrote:
> Joachim Durchholz <email***@***.com> wrote:
>
>>OTOH, isn't that the grail that many people have been searching for:
>>programming by simply declaring the results that they want to see?
>
> Possibly.
>
>>No, FPLs are actually just that: compilable postconditions.
>
> This seems to me a bit misleading. Perhaps someone will explain why I
> should stop thinking this way; but currently I classify statements like
> this in the "well, sort of" slot of my mind. If functional programming
> were really just compilable postconditions, then functional programmers
> would be able to skip a good bit of stuff that they really can't. For
> example, time and space complexity of code is still entirely relevant
> for functional programming. I can't simply write:
>
> (define fib
> (lambda (x) (if (< x 2) 1 (+ (fib (- x 1)) (fib (- x 2))))))
>
> and expect the compiler to create an efficient algorithm for me.

This is true, but note that postconditions also need to be efficient
if we are going to execute them.

That is, the difference you've pointed out is not a difference between
executable postconditions and functional programs. Both the inefficient
functional definition of 'fib' and an efficient one are executable
postconditions. In order to prove that the efficient implementation is
as correct as the inefficient one, we need to prove that, treated as
postconditions, the former implies the latter.

(In this case a single deterministic result is required, so the former
will be equivalent to the latter.)

--
David Hopwood <email***@***.com>

java-programmer >> What is a type error? Joe Marshall wrote:
> Marshall wrote:
> >
> > Again, I disagree: it is posible to have mutability without
> > pointers/identity/objects.
>
> I think you are wrong, but before I make a complete ass out of myself,
> I have to ask what you mean by `mutability'. (And
> pointers/identity/objects, for that matter.)

Responding to requests for examples from Joachim, Joe, and Chris....

The very simple example is the one Darren New already mentioned.

Consider the following Java fragment:

void foo() {
int i = 0;
int j = 0;

// put any code here you want

j = 1;
i = 2;
// check value of j here. It is still 1, no matter what you filled in
above.
// The assignment to i cannot be made to affect the value of j.

}

Those two local primitive variables cannot be made to have the same
identity. But you can update them, so this is an example of mutability
without the possibility of identity.

Earlier I also mentioned SQL tables as an example, although SQL
supports *explicit* aliasing via views.

> Alan Bawden discusses the phenomenon of `state' in his Ph.D.
> dissertation "Implementing Distributed Systems Using Linear Naming".
> MIT AI Lab Technical Report AITR-1627. March 1993 He makes a
> persuasive argument that `state' is associated with cycles in naming.

I would like to read that, but my brain generally runs out of gas at
about 21
pages, so it's about an order of magnitude bigger than I can currently
handle. :-( As to "cycles in naming" that's certainly an issue. But it
it
a requirement for state? Back to Java locals, it seems to me they meet
the standard definition of state, despite the lack of cycles.

As to pointers/references, I earlier mentioned the existence of the
reference/dereference operations as being definitional. Note that
one can go to some lengths to obscure them, but they're still there.
For example, Java has the reference and dereference operators;
Java's "." operator is actually C's "->" operator.

I am not so bold/foolish as to attempt a defintion of "object" however.
:-)

Marshall

java-programmer >> What is a type error?
Marshall wrote:
>
> Consider the following Java fragment:
>
> void foo() {
> int i = 0;
> int j = 0;
>
> // put any code here you want
>
> j = 1;
> i = 2;
> // check value of j here. It is still 1, no matter what you filled in
> above.
> // The assignment to i cannot be made to affect the value of j.
>
> }

True, but you have hidden the pointers. Semantically, the identifiers
i and j refer not to integers but to locations that hold integers. The
assignment modifies the location.

> Those two local primitive variables cannot be made to have the same
> identity. But you can update them, so this is an example of mutability
> without the possibility of identity.

The identity is temporal: You use the same variable name at two
different times. Do you intend for the second `i' to mean the same
variable as the first `i'?

java-programmer >> What is a type error? Darren New <email***@***.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.
Some might call that a problem in and of itself, as it complicates the
formal model of the language and makes it difficult to predict what
result will be produced by normal order evaluation.

On the other hand, this thread seems to be using "identity" to mean
"identity with potential for aliasing", in which case it is vacuously
true that eliminating identity also prevents the problems that arise
from aliasing. It is true, and I agree on this with Marshall, that
eliminating the potential for aliasing solves a lot of problems with
checking invariants. 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. I'd like to see an example of code that would be harder to
write without mutation, but which can obey any restriction that's
sufficient to prevent aliasing.

> Why is it problematic that variables have identity and are mutable?
> Certainly I can later "find" whatever value I put into x.

I simply found the language confusing. I said it would be nonsensical
for a language to have mutation without identity.

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

java-programmer >> What is a type error? David Hopwood <email***@***.com> wrote:
> This is true, but note that postconditions also need to be efficient
> if we are going to execute them.

If checked by execution, yes. In which case, I am trying to get my head
around how it's any more true to say that functional languages are
compilable postconditions than to say the same of imperative languages.
In both cases, some statement is asserted through a description of a
means of computing it. There may be a distinction worth making here,
but I'm missing it so far.

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