Re: Modelling Disjoint Subtypes

From: Marshall <marshall.spight_at_gmail.com>
Date: 26 Mar 2007 15:44:06 -0700
Message-ID: <1174949046.562547.211020_at_y80g2000hsf.googlegroups.com>


On Mar 26, 12:30 pm, "David Cressey" <cresse..._at_verizon.net> wrote:
> "Marshall" <marshall.spi..._at_gmail.com> wrote in message
> > On Mar 26, 7:18 am, Bob Badour <bbad..._at_pei.sympatico.ca> wrote:
>
> > > But even if the type checking were deferred until runtime in the
> > > conditional test, the type of x and y is statically known in the block
> > > under consideration.
>
> > THAT was the point I was trying to make.
>
> > Regardless of how we got there, inside the block, the compiler
> > knows statically that the x and y values are integers, even
> > though their declared type in the code is rational. There can
> > exist implementations of rationals such that when the rationals
> > are integers, the generated code for a multiply is identical to
> > the generated code for multiplying integers. So within the
> > context of that block, looking at the generated code, you
> > would not be able to distinguish those two cases. The
> > types have been erased.
>
> OK, now you've lost me. Why is it necessary to distinguish between the case
> where x and y are integers, and the case where x and y are rationals that
> are constrained to take on only integer values?

Hmmm. There are some subtle issues with the way you've stated it above. This may seem like nitpicking, but I have to fix that before I can respond.

First, x and y are rationals exclusively. x and y are declared as rationals; that is their static type. This is set in stone before the program has ever run.

Second, the word "constrained" isn't apropos. The "if" statement in my earlier code doesn't constrain anything; rather it forks into one of two cases. Which case gets chosen for a particular invocation of the "if" statement will not be determined until runtime. However, the if statement has two branches, and within either branch, we know *statically* which one was chosen, because we are in that branch.

So:
1) x and y are rationals.
2) inside the previously specified block, we know that x and y   are integers.
3) the code generator does the optimization of generating

   code for an integer operation.

Therefore, if we are inspecting the code in that block, we will conclude something about the type of x and y, and that something that we will conclude will be incorrect.

This is possible because types don't exist at runtime. (In static languages.)

In another post I showed some C code and a case against that C code; the issue is clearer in that example, I think.

Marshall Received on Tue Mar 27 2007 - 00:44:06 CEST

Original text of this message