[27990] in Perl-Users-Digest
Perl-Users Digest, Issue: 9354 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Fri Jun 23 09:10:18 2006
Date: Fri, 23 Jun 2006 06:10:08 -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 Fri, 23 Jun 2006 Volume: 10 Number: 9354
Today's topics:
Re: What is a type error? <pc@p-cos.net>
Re: What is a type error? <pc@p-cos.net>
Re: What is a type error? <chris.uppal@metagnostic.REMOVE-THIS.org>
Re: What is a type error? <chris.uppal@metagnostic.REMOVE-THIS.org>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: Fri, 23 Jun 2006 13:32:22 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is a type error?
Message-Id: <4g21q7F1lf5lsU1@individual.net>
Matthias Blume wrote:
> Pascal Costanza <pc@p-cos.net> writes:
>
>> Chris Smith wrote:
>>
>>> While this effort to salvage the term "type error" in dynamic
>>> languages is interesting, I fear it will fail. Either we'll all
>>> have to admit that "type" in the dynamic sense is a psychological
>>> concept with no precise technical definition (as was at least hinted
>>> by Anton's post earlier, whether intentionally or not) or someone is
>>> going to have to propose a technical meaning that makes sense,
>>> independently of what is meant by "type" in a static system.
>> What about this: You get a type error when the program attempts to
>> invoke an operation on values that are not appropriate for this
>> operation.
>>
>> Examples: adding numbers to strings; determining the string-length of
>> a number; applying a function on the wrong number of parameters;
>> applying a non-function; accessing an array with out-of-bound indexes;
>> etc.
>
> Yes, the phrase "runtime type error" is actually a misnomer. What one
> usually means by that is a situation where the operational semantics
> is "stuck", i.e., where the program, while not yet arrived at what's
> considered a "result", cannot make any progress because the current
> configuration does not match any of the rules of the dynamic
> semantics.
>
> The reason why we call this a "type error" is that such situations are
> precisely the ones we want to statically rule out using sound static
> type systems. So it is a "type error" in the sense that the static
> semantics was not strong enough to rule it out.
>
>> Sending a message to an object that does not understand that message
>> is a type error. The "message not understood" machinery can be seen
>> either as a way to escape from this type error in case it occurs and
>> allow the program to still do something useful, or to actually remove
>> (some) potential type errors.
>
> I disagree with this. If the program keeps running in a defined way,
> then it is not what I would call a type error. It definitely is not
> an error in the sense I described above.
If your view of a running program is that it is a "closed" system, then
you're right. However, maybe there are several layers involved, so what
appears to be a well-defined behavior from the outside may still be
regarded as a type error internally.
A very obvious example of this is when you run a program in a debugger.
There are two levels involved here: the program signals a type error,
but that doesn't mean that the system as a whole is stuck. Instead, the
debugger takes over and offers ways to deal with the type error. The
very same program run without debugging support would indeed simply be
stuck in the same situation.
So to rephrase: It depends on whether you use the "message not
understood" machinery as a way to provide well-defined behavior for the
base level, or rather as a means to deal with an otherwise unanticipated
situation. In the former case it extends the language to remove certain
type errors, in the latter case it provides a kind of debugging facility
(and it indeed may be a good idea to deploy programs with debugging
facilities, and not only use debugging tools at development time).
This is actually related to the notion of reflection, as coined by Brian
C. Smith. In a reflective architecture, you distinguish between various
interpreters, each of which interprets the program at the next level. A
debugger is a program that runs at a different level than a base program
that it debugs. However, the reflective system as a whole is "just" a
single program seen from the outside (with one interpreter that runs the
whole reflective tower). This distinction between the internal and the
external view of a reflective system was already made by Brian Smith.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Fri, 23 Jun 2006 13:39:53 +0200
From: Pascal Costanza <pc@p-cos.net>
Subject: Re: What is a type error?
Message-Id: <4g2289F1kv8htU1@individual.net>
Chris Smith wrote:
> Pascal Costanza <pc@p-cos.net> wrote:
>> What about this: You get a type error when the program attempts to
>> invoke an operation on values that are not appropriate for this operation.
>>
>> Examples: adding numbers to strings; determining the string-length of a
>> number; applying a function on the wrong number of parameters; applying
>> a non-function; accessing an array with out-of-bound indexes; etc.
>
> Hmm. I'm afraid I'm going to be picky here. I think you need to
> clarify what is meant by "appropriate".
No, I cannot be a lot clearer here. What operations are appropriate for
what values largely depends on the intentions of a programmer. Adding a
number to a string is inappropriate, no matter how a program behaves
when this actually occurs (whether it continues to execute the operation
blindly, throws a continuable exception, or just gets stuck).
> If you mean "the operation will
> not complete successfully" as I suspect you do, then we're closer...
No, we're not. You're giving a purely technical definition here, that
may or may not relate to the programmer's (or "designer's")
understanding of the domain.
Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
------------------------------
Date: Fri, 23 Jun 2006 13:03:13 +0100
From: "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org>
Subject: Re: What is a type error?
Message-Id: <449bde5f$0$663$bed64819@news.gradwell.net>
Eliot Miranda wrote:
[me:]
> > Taking Smalltalk /specifically/, there is a definite sense in which it
> > is typeless -- or trivially typed -- in that in that language there are
> > no[*] operations which are forbidden[**],
>
> Come one Chris U. One has to distinguish an attempt to invoke an
> operation with it being carried out. There is nothing in Smalltalk to
> stop one attempting to invoke any "operation" on any object. But one
> can only actually carry-out operations on objects that implement them.
> So, apart from the argument about inadvertent operation name overloading
> (which is important, but avoidable), Smalltalk is in fact
> strongly-typed, but not statically strongly-typed.
What are you doing /here/, Eliot, this is Javaland ? Smalltalk is thatta
way ->
;-)
But this discussion has been all about /whether/ it is ok to apply the notion
of (strong) typing to what runtime-checked languages do. We all agree that
the checks happen, but the question is whether it is
reasonable/helpful/legitimate to extend the language of static checking to the
dynamic case. (I'm on the side which says yes, but good points have been made
against it).
The paragraph you quoted doesn't represent most of what I have been saying --
it was just a side-note looking at one small aspect of the issue from a
different angle.
-- chris
------------------------------
Date: Fri, 23 Jun 2006 13:32:31 +0100
From: "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org>
Subject: Re: What is a type error?
Message-Id: <449bde60$0$663$bed64819@news.gradwell.net>
Chris Smith wrote:
[me:]
> > I think we're agreed (you and I anyway, if not everyone in this thread)
> > that we don't want to talk of "the" type system for a given language.
> > We want to allow a variety of verification logics. So a static type
> > system is a logic which can be implemented based purely on the program
> > text without making assumptions about runtime events (or making
> > maximally pessimistic assumptions -- which comes to the same thing
> > really). I suggest that a "dynamic type system" is a verification
> > logic which (in principle) has available as input not only the program
> > text, but also the entire history of the program execution up to the
> > moment when the to-be-checked operation is invoked.
>
> I am trying to understand how the above statement about dynamic types
> actually says anything at all. So a dynamic type system is a system of
> logic by which, given a program and a path of program execution up to
> this point, verifies something. We still haven't defined "something",
> though.
That was the point of my first sentence (quoted above). I take it, and I
assumed that you shared my view, that there is no single "the" type system --
that /a/ type system will yield judgements on matters which it has been
designed to judge. So unless we either nominate a specific type system or
choose what judgements we want to make (today) any discussion of types is
necessarily parameterised on the class(es) of <Judgements>. So, I don't --
can't -- say /which/ judgements my "dynamic type systems" will make. They may
be about nullablity, they may be about traditional "type", they may be about
mutability...
When we look at a specific language (and its implementation), then we can
induce the logic(s) that whatever dynamic checks it applies define.
Alternatively we can consider other "dynamic type systems" which we would like
to formalise and mechanise, but which are not built into our language of
choice.
> We also haven't defined what happens if that verification
> fails.
True, and a good point. But note that it only applies to systems which are
actually implemented in code (or which are intended to be so).
As a first thought, I suggest that a "dynamic type system" should specify a
replacement action (which includes, but is not limited to, terminating
execution). That action is taken /instead/ of the rejected one. E.g. we don't
actually read off the end of the array, but instead a signal is raised. (An
implementation might, in some cases, find it easier to implement the checks by
allowing the operation to fail, and then backtracking to "pretend" that it had
never happened, but that's irrelevant here). The replacement action must -- of
course -- be valid according to the rules of the type system.
Incidentally, using that idea, we get a fairly close analogy to the difference
between strong and weak static type systems. If the "dynamic type system"
doesn't specify a valid replacement action, or if that action is not guaranteed
to be taken, then it seems that the type system or the language implementation
is "weak" in very much the same sort of way as -- say -- the 'C' type system is
weak and/or weakly enforced.
I wonder whether that way of looking at it -- the "error" never happens since
it is replaced by a valid operation -- puts what I want to call dynamic type
systems onto a closer footing with static type systems. Neither allows the
error to occur.
(Of course, /I/ -- the programmer -- have made a type error, but that's
different thing.)
> In other words, I think that everything so far is essentially just
> defining a dynamic type system as equivalent to a formal semantics for a
> programming language, in different words that connote some bias toward
> certain ways of looking at possibilities that are likely to lead to
> incorrect program behavior. I doubt that will be an attractive
> definition to very many people.
My only objections to this are:
a) I /want/ to use the word "type" to describe the kind of reasoning I do (and
some of the mistakes I make)
b) I want to separate the systems of reasoning (whether formal or informal,
static or dynamic, implemented or merely conceptual, and /whatever/ we call 'em
;-) from the language semantics. I have no objection to <some type system>
being used as part of a language specification, but I don't want to restrict
types to that.
> > Note that not all errors that I would want to call type errors are
> > necessarily caught by the runtime -- it might go happily ahead never
> > realising that it had just allowed one of the constraints of one of the
> > logics I use to reason about the program. What's known as an
> > undetected bug -- but just because the runtime doesn't see it, doesn't
> > mean that I wouldn't say I'd made a type error. (The same applies to
> > any specific static type system too, of course.)
>
> In static type system terminology, this quite emphatically does NOT
> apply. There may, of course, be undetected bugs, but they are not type
> errors. If they were type errors, then they would have been detected,
> unless the compiler is broken.
Sorry, I wasn't clear. I was thinking here of my internal analysis (which I
want to call a type system too). Most of what I was trying to say is that I
don't expect a "dynamic type system" to be complete, any more than a static
one. I also wanted to emphasise that I am happy to talk about type systems
(dynamic or not) which have not been implemented as code (so they yield
judgements, and provide a framework for understanding the program, but nothing
in the computer actually checks them for me).
> If you are trying to identify a set of dynamic type errors, in a way
> that also applies to statically typed languages, then I will read on.
Have I answered that now ? /Given/ a set of operations which I want to forbid,
I would like to say that a "dynamic type system" which prevents them executing
is doing very much the same job as a static type system which stops the code
compiling.
Of course, we can talk about what kinds of operations we want to forbid, but
that seems (to me) to be orthogonal to this discussion. Indeed, the question
of dynamic/static is largely irrelevant to a discussion of what operations we
want to police, except insofar as certain checks might require information
which isn't available to a (feasible) static theorem prover.
-- chris
------------------------------
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 9354
***************************************
