[28101] in Perl-Users-Digest
Perl-Users Digest, Issue: 9465 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Thu Jul 13 18:10:13 2006
Date: Thu, 13 Jul 2006 15:10:05 -0700 (PDT)
From: Perl-Users Digest <Perl-Users-Request@ruby.OCE.ORST.EDU>
To: Perl-Users@ruby.OCE.ORST.EDU (Perl-Users Digest)
Perl-Users Digest Thu, 13 Jul 2006 Volume: 10 Number: 9465
Today's topics:
Re: What is a type error? <dnew@san.rr.com>
Re: What is a type error? <eval.apply@gmail.com>
Re: What is a type error? <david.nospam.hopwood@blueyonder.co.uk>
Re: What is a type error? <marshall.spight@gmail.com>
Re: What is a type error? <david.nospam.hopwood@blueyonder.co.uk>
Re: What is a type error? <marshall.spight@gmail.com>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Thu, 13 Jul 2006 18:08:00 GMT
From: Darren New <dnew@san.rr.com>
Subject: Re: What is a type error?
Message-Id: <4_vtg.14828$MF6.8524@tornado.socal.rr.com>
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.
------------------------------
Date: 13 Jul 2006 11:15:22 -0700
From: "Joe Marshall" <eval.apply@gmail.com>
Subject: Re: What is a type error?
Message-Id: <1152814522.080290.267010@m73g2000cwd.googlegroups.com>
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.
------------------------------
Date: Thu, 13 Jul 2006 19:31:08 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is a type error?
Message-Id: <0cxtg.61529$181.2346@fe3.news.blueyonder.co.uk>
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 <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: 13 Jul 2006 12:47:57 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is a type error?
Message-Id: <1152820077.044047.228350@p79g2000cwp.googlegroups.com>
Joachim Durchholz wrote:
> 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).
Agreed on all counts.
> 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.
Unless we have some specific mechanism to make two named variables
have the same identity, (distinct from having the same value), then
there
is no aliasing. Pointers or references is one such mechanism; lexical
closures over variables is another. (I don't know of any others.)
> > I agree that mutability
> > plus identity implies aliasing problems, however.
>
> Then we're agreeing about the most important point anyway.
Yes.
> >> 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?
See next post.
Marshall
------------------------------
Date: Thu, 13 Jul 2006 19:56:36 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is a type error?
Message-Id: <Uzxtg.93986$7Z6.48541@fe2.news.blueyonder.co.uk>
Chris Smith wrote:
> Joachim Durchholz <jo@durchholz.org> 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 <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: 13 Jul 2006 12:59:30 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is a type error?
Message-Id: <1152820770.519295.323890@i42g2000cwa.googlegroups.com>
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
------------------------------
Date: 6 Apr 2001 21:33:47 GMT (Last modified)
From: Perl-Users-Request@ruby.oce.orst.edu (Perl-Users-Digest Admin)
Subject: Digest Administrivia (Last modified: 6 Apr 01)
Message-Id: <null>
Administrivia:
#The Perl-Users Digest is a retransmission of the USENET newsgroup
#comp.lang.perl.misc. For subscription or unsubscription requests, send
#the single line:
#
# subscribe perl-users
#or:
# unsubscribe perl-users
#
#to almanac@ruby.oce.orst.edu.
NOTE: due to the current flood of worm email banging on ruby, the smtp
server on ruby has been shut off until further notice.
To submit articles to comp.lang.perl.announce, send your article to
clpa@perl.com.
#To request back copies (available for a week or so), send your request
#to almanac@ruby.oce.orst.edu with the command "send perl-users x.y",
#where x is the volume number and y is the issue number.
#For other requests pertaining to the digest, send mail to
#perl-users-request@ruby.oce.orst.edu. Do not waste your time or mine
#sending perl questions to the -request address, I don't have time to
#answer them even if I did know the answer.
------------------------------
End of Perl-Users Digest V10 Issue 9465
***************************************
