Chris Uppal <[EMAIL PROTECTED]> wrote:
> 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.
Yes, I definitely agree.
My point was that if you leave BOTH the "something" and the response to
verification failure undefined, then your definition of a dynamic type
system is a generalization of the definition of a conditional
expression. That is (using Java),
if (x != 0) y = 1 / x;
else y = 999999999;
is not all that much different from (now restricting to Java):
try { y = 1 / x; }
catch (ArithmeticException e) { y = 999999999; }
So is one of them a use of a dynamic type system, where the other is
not?
> Incidentally, using that idea, we get a fairly close analogy to the difference
> between strong and weak static type systems.
I think, actually, that the analogy of the strong/weak distinction
merely has to do with how much verification is done. But then, I
dislike discussion of strong/weak type systems in the first place. It
doesn't make any sense to me to say that we verify something and then
don't do anything if the verification fails. In those cases, I'd just
say that verification doesn't really exist or is incorrectly
implemented. Of course, this would make the type system weaker.
> 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.
Perhaps. I'm thinking some things over before I respond to Anton. I'll
do that first, and some of my thoughts there may end up being relevant
to this question.
> 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.
In the pragmatic sense of this desire, I'd suggest that a way to
characterize this is that your type system is a set of changes to the
language semantics. By applying them to a language L, you obtain a
different language L' which you can then use. If your type system has
any impact on the set of programs accepted by the language (static
types) or on any observable behavior which they exhibit (dynamic types),
then I can't see a justification for claiming that the result is the
same language; and if it does not, then the whole exercise is silly.
> 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.
Indeed, that is orthogonal to the discussion from the perspective of
static types. If you are proposing that it is also orthogonal with
respect to dynamic types, that will be a welcome step toward our goal of
a grand unified type theory, I suppose. I have heard from others in
this thread that they don't believe so. I am also interested in your
response to the specific example involving an if statement at the
beginning of this reply.
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
--
http://mail.python.org/mailman/listinfo/python-list
