[28085] in Perl-Users-Digest
Perl-Users Digest, Issue: 9449 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Tue Jul 11 14:10:13 2006
Date: Tue, 11 Jul 2006 11:10:07 -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 Tue, 11 Jul 2006 Volume: 10 Number: 9449
Today's topics:
Re: What is a type error? <david.nospam.hopwood@blueyonder.co.uk>
Re: What is a type error? <cdsmith@twu.net>
Re: What is a type error? <cdsmith@twu.net>
Re: What is a type error? <dnew@san.rr.com>
Re: What is a type error? <dnew@san.rr.com>
Re: What is a type error? <dnew@san.rr.com>
Re: What is a type error? <marshall.spight@gmail.com>
Re: What is a type error? <gneuner2/@comcast.net>
Re: What is a type error? <cdsmith@twu.net>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Tue, 11 Jul 2006 14:59:46 GMT
From: David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
Subject: Re: What is a type error?
Message-Id: <C1Psg.56632$181.30396@fe3.news.blueyonder.co.uk>
Chris Smith wrote:
> David Hopwood <david.nospam.hopwood@blueyonder.co.uk> wrote:
>
>>Maybe I'm not understanding what you mean by "complete". Of course any
>>type system of this expressive power will be incomplete (whether or not
>>it can express conditions 3 to 5), in the sense that it cannot prove all
>>true assertions about the types of expressions.
>
> Ah. I meant complete enough to accomplish the goal in this subthread,
> which was to ensure that the compiler knows when a particular int
> variable is guaranteed to be greater than 18, and when it is not.
I don't think that placing too much emphasis on any individual example is
the right way of thinking about this. What matters is that, over the range
of typical programs written in the language, the value of the increased
confidence in program correctness outweighs the effort involved in both
adding annotations, and understanding whether any remaining run-time checks
are guaranteed to succeed.
Look at it this way: suppose that I *need* to verify that a program has
no range errors. Doing that entirely manually would be extremely tedious.
If the compiler can do, say, 90% of the work, and point out the places that
need to be verified manually, then that would be both less tedious, and
less error-prone.
--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>
------------------------------
Date: Tue, 11 Jul 2006 09:43:48 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is a type error?
Message-Id: <MPG.1f1d751dd472b86d989783@news.altopia.net>
David Hopwood <david.nospam.hopwood@blueyonder.co.uk> wrote:
> I don't think that placing too much emphasis on any individual example is
> the right way of thinking about this. What matters is that, over the range
> of typical programs written in the language, the value of the increased
> confidence in program correctness outweighs the effort involved in both
> adding annotations, and understanding whether any remaining run-time checks
> are guaranteed to succeed.
Are you really that short on people to disagree with?
In this particular branch of this thread, we were discussing George's
objection that it would be ridiculous for a type system to check that a
variable should be greater than 18. There is no such thing as placing
too much emphasis on what we were actually discussing. If you want to
discuss something else, feel free to post about it. Why does it bother
you that I'm considering George's point?
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: Tue, 11 Jul 2006 09:53:39 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is a type error?
Message-Id: <MPG.1f1d777230d4eb9b989784@news.altopia.net>
Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> wrote:
> Chris Smith <cdsmith@twu.net> writes:
> >> No what happens if right here you code
> >> b := 16;
> >>
> >> Does that again change the type of "b"? Or is that an illegal
> >> instruction, because "b" has the "local type" of (18..22)?
> >
> > It arranges that the expression "b" after that line (barring further
> > changes) has type int{16..16}, which would make the later call to
> > signContract illegal.
>
> The assignment might be performed in a function called there, so it's
> not visible locally.
Indeed, I pointed that out a few messages ago. That doesn't mean it's
impossible, but it does mean that it's more difficult. Eventually, the
compiler will have to stop checking something, somewhere. It certainly
doesn't, though, have to stop at the first functional abstraction it
comes to. The ways that a function modifies the global application
state certainly ought to be considered part of the visible API of that
function, and if we could reasonably express that in a type system, then
that's great! Granted, designing such a type system for an arbitrary
imperative language seems a little scary.
> Propagating constraints from conditionals is not applicable to mutable
> variables, at least not easily.
Certainly it worked in the code from my original response to George.
Regardless of whether it might not work in more complex scenarios (and I
think it could, though it would be more challenging), it still doesn't
seem reasonable to assert that the technique is not applicable. If the
type system fails, then it fails conservatively as always, and some
programmer annotation and runtime check is needed to enforce the
condition.
> I think that constant bounds are not very useful at all. Most ranges
> are not known statically, e.g. a variable can span the size of an
> array.
I think you are overestimating the difficulties here. Specialized
language already exist that reliably (as in, all the time) move array
bounds checking to compile time; that means that there exist at least
some languages that have already solved this problem. Going back to my
handy copy of Pierce's book again, he claims that range checking is a
solved problem in theory, and the only remaining work is in how to
integrate it into a program without prohibitive amounts of type
annotation.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
Date: Tue, 11 Jul 2006 16:15:05 GMT
From: Darren New <dnew@san.rr.com>
Subject: Re: What is a type error?
Message-Id: <d8Qsg.14127$MF6.7513@tornado.socal.rr.com>
Marshall wrote:
> Now, I'm not fully up to speed on DBC. The contract specifications,
> these are specified statically, but checked dynamically, is that
> right?
Yes, but there's a bunch more to it than that. The handling of
exceptions, an in particular exceptions caused by failed pre/post
conditions, is an integral part of the process.
Plus, of course, pre/post condition checking is turned off while
checking pre/post conditions. This does make sense if you think about it
long enough, but it took me several months before I realized why it's
necessary theoretically rather than just practically.
> Wouldn't it be possible to do them at compile time?
For some particularly simple ones, yes. For others, like "the chess
pieces are in a position it is legal to get to from a standard opening
set-up", it would be difficult. Anything to do with I/O is going to be
almost impossible to write a checkable postcondition for, even at
runtime. "After this call, the reader at the other end of the socket
will receive the bytes in argument 2 without change."
As far as I understand it, Eiffel compilers don't even make use of
postconditions to optimize code or eliminate run-time checks (like null
pointer testing).
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
------------------------------
Date: Tue, 11 Jul 2006 16:20:16 GMT
From: Darren New <dnew@san.rr.com>
Subject: Re: What is a type error?
Message-Id: <4dQsg.23042$Z67.18834@tornado.socal.rr.com>
Marcin 'Qrczak' Kowalczyk wrote:
> The assignment might be performed in a function called there, so it's
> not visible locally.
In Hermes, which actually does this sort of constraint propagation, you
don't have the ability[1] to munge some other routine's[2] local
variables, so that becomes a non-issue. You wind up with some strange
constructs, tho, like an assignment statement that copies and a
different assignment statement that puts the rvalue into the variable on
the left while simultaneously destroying whatever variable held the rvalue.
[1] You do. Just not in a way visible to the programmer. The compiler
manages to optimize out most places that different names consistantly
refer to the same value.
[2] There aren't subroutines. Just processes, with their own address
space, to which you send and receive messages.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
------------------------------
Date: Tue, 11 Jul 2006 16:30:39 GMT
From: Darren New <dnew@san.rr.com>
Subject: Re: What is a type error?
Message-Id: <PmQsg.23044$Z67.11504@tornado.socal.rr.com>
Chris Smith wrote:
> Specialized
> language already exist that reliably (as in, all the time) move array
> bounds checking to compile time;
It sounds like this means the programmer has to code up what it means to
index off an array, yes? Otherwise, I can't imagine how it would work.
x := read_integer_from_stdin();
write_to_stdout(myarray[x]);
What does the programmer have to do to implement this semantic in the
sort of language you're talking about? Surely something somewhere along
the line has to "fail" (for some meaning of failure) at run-time, yes?
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
------------------------------
Date: 11 Jul 2006 09:31:30 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is a type error?
Message-Id: <1152635490.527372.51150@h48g2000cwc.googlegroups.com>
Chris Smith wrote:
>
> Going back to my
> handy copy of Pierce's book again, he claims that range checking is a
> solved problem in theory, and the only remaining work is in how to
> integrate it into a program without prohibitive amounts of type
> annotation.
This is in TAPL? Or ATTPL? Can you cite it a bit more specifically?
I want to reread that.
Marshall
------------------------------
Date: Tue, 11 Jul 2006 13:26:43 -0400
From: George Neuner <gneuner2/@comcast.net>
Subject: Re: What is a type error?
Message-Id: <tog7b2te7ck12cv35l4b3dm2visfrtevgp@4ax.com>
On Tue, 11 Jul 2006 14:59:46 GMT, David Hopwood
<david.nospam.hopwood@blueyonder.co.uk> wrote:
>What matters is that, over the range
>of typical programs written in the language, the value of the increased
>confidence in program correctness outweighs the effort involved in both
>adding annotations, and understanding whether any remaining run-time checks
>are guaranteed to succeed.
Agreed, but ...
>Look at it this way: suppose that I *need* to verify that a program has
>no range errors. Doing that entirely manually would be extremely tedious.
>If the compiler can do, say, 90% of the work, and point out the places that
>need to be verified manually, then that would be both less tedious, and
>less error-prone.
All of this presupposes that you have a high level of confidence in
the compiler. I've been in software development for going in 20 years
now and worked 10 years on high performance, high availability
systems. In all that time I have yet to meet a compiler ... or
significant program of any kind ... that is without bugs, noticeable
or not.
I'm a fan of static typing but the major problem I have with complex
inferencing (in general) is the black box aspect of it. That is, when
the compiler rejects my code, is it really because a) I was stupid, b)
the types are too complex, or c) the compiler itself has a bug. It's
certainly true that the vast majority of my problems are because I'm
stupid, but I've run into actual compiler bugs far too often for my
liking (high performance coding has a tendency to uncover them).
I think I understand how to implement HM inferencing ... I haven't
actually done it yet, but I've studied it and I'm working on a toy
language that will eventually use it. But HM itself is a toy compared
to an inferencing system that could realistically handle some of the
problems that were discussed in this and Xah's "expressiveness" thread
(my own beef is with *static* checking of range narrowing assignments
which I still don't believe can be done regardless of Chris Smith's
assertions to the contrary).
It seems to me that the code complexity of such a super-duper
inferencing system would make its bug free implementation quite
difficult and I personally would be less inclined to trust a compiler
that used it than one having a less capable (but easier to implement)
system.
George
--
for email reply remove "/" from address
------------------------------
Date: Tue, 11 Jul 2006 11:35:32 -0600
From: Chris Smith <cdsmith@twu.net>
Subject: Re: What is a type error?
Message-Id: <MPG.1f1d8f46483dc014989786@news.altopia.net>
Marshall <marshall.spight@gmail.com> wrote:
> Chris Smith wrote:
> > Going back to my
> > handy copy of Pierce's book again, he claims that range checking is a
> > solved problem in theory, and the only remaining work is in how to
> > integrate it into a program without prohibitive amounts of type
> > annotation.
>
> This is in TAPL? Or ATTPL? Can you cite it a bit more specifically?
> I want to reread that.
It's TAPL. On further review, I may have done more interpretation than
I remembered. In particular, the discussion is limited to array bounds
checking, though I don't see a fundamental reason why it wouldn't extend
to other kinds of range checking against constant ranges as we've been
discussing here.
Relevant sections are:
Page 7 footnote: Mentions other challenges such as tractability that
seem more fundamental, but those are treated as trading off against
complexity of annotations; in other words, if we didn't require so many
annotations, then it might become computationally intractable. The next
reference better regarding tractability.
Section 30.5, pp. 460 - 465: Gives a specific example of a language
(theoretical) developed to use limited dependent types to eliminate
array bounds checking. There's a specific mention there that it can be
made tractable because the specific case of dependent types needed for
bounds checking happens to have efficient algorithms, although dependent
types are intractable in the general case.
I'm afraid that's all I've got. I also have come across a real-life
(though not general purpose) languages that does bounds checking
elimination via these techniques... but I can't find them now for the
life of me. I'll post if I remember what it is, soon.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
------------------------------
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 9449
***************************************
