Re: Static typechecking in OO [was Re: Strong Types ?]

> >> So in such a language one could write:
>
> >> for(polimorphic_container<my_base_class>::iterator i =
> >> my_container.begin();
> >> i != my_container.end();
> >> ++i)
> >> {
> >> do_special_thing(*i);
>
> >> }
>
>
> > In case I misunderstood, and the virtual modifier in the parameter
> > list for do_special_thing is telling the compiler to use a more
> > specific type, the compiler will have to do some form of type check at
> > runtime for the branching.
>
> virtual tells compiler to dispatch on actual (runtime) type.


In which case it is no longer statically verifiable, as the compiler
has to do run time dispatch and can not verify at compile time whether
it should be calling the overload for my_derived_1 or my_derived_2,
which are safe, or for my_derived_3 which would be unsafe. The only
way it would be safe is if the subtypes were limited to only those you
defined -- it would be much easier to make the function be a virtual
function on the type, and do dynamic look up -- although the moment
you do that you're removing your downcast.


>
> > Essentially the copmiler would be emitting
> > code like that you have below, all you would have added is syntactic
> > sugar.
>
> Type checking is not a syntactic sugar.
Agreed. The syntax for dispatch *is*. You syntax is sugar for a
switch on type, that allows for (by definition) a finite set of
subclasses that must be known at compile time. The syntax for other
statically checked language hides a function pointer lookup that
allows for an unlimited number of subclasses.


> Whether underlying code uses dynamic
> or static dispatch is a technical detail. What is important is a static
> guarantee that there is no situation where proper dispatch could not be
> performed/.


Exactly, and that's what your example doesn't allow, your language
requires the call site to choose from a static set of functions,
thereby meaning either you have a restricted set of subtypes -- to
allow the static check to cover all possibilities -- or it will hit a
runtime error when it encounters an unsupported type.


> >> Notice, that compiler can statically check at every call site if there is
> >> no such my_base_class subclass for which there is not any matching
> >> do_special_thing() variant.
>
> > The problem is, your generic_list<my_base_class> can contain any of
> > the subtypes, and the compiler can't determine at compile time what
> > code to emit.
>
> Of course it can. Runtime type dispatch is a thing known for decades.


You've missed the point -- there can be any number of subclasses of
my_base_class and it is still entirely statically verifiable, whereas
your approach will place a restriction on the number of classes that
it is type safe over.


>
>
>
> >> switch class(obj)
> >> {
> >> case my_derived_1:
> >> obj.foo();
> >> break;
>
> >> case my_derived_2:
> >> obj.bar();
> >> break;
>
> >> }
>
> >> Again, a compiler could (statically) check if above switch covers all the
> >> possible variants.
>
> > The underlying problem with this is the same as above, the type check
> > is still at runtime.
>
> Type security check is done at compile time and that's what's important.


Sorry, that was a bad example on my part. What i was (probably)
trying to say (and as i have said before) is that your implementation
requires that there be a limited set of subtypes, that are known by
the compiler, at compile time.


>
> > The reality is that the type system provided by most mainstream
> > languages, say C++, Java, the CLR, Obj-C cannot be entirely statically
> > typed due to the ability to downcast. A downcast is intrinsically a
> > runtime operation.
>
> But static type checking is about guaranteeing that no type errors would
> occur at runtime. it's not about banishment of runtime mechanisms.
static type checking is about the banishment of runtime type errors,
which while not precluding runtime dispatch, and that means that there
cannot be downcasting.


Simple example:
class A;
class B : A; (or class B extends A, etc)


void foo(A myA) {
      ...
      B myB = (B)myA; // Cannot be statically verified
      ...
}


This isn't strictly true -- if you have access to all the code that
can possibly call this function, static analysis will get you there.
The problem is that in many cases (especially as a library) you can't
make that guarantee, and in many others the analysis is intractable --
i can't remember whether worst case is np-complete or the halting
problem...


> > However there's no actual requirement for an OO type system to provide
> > support for downcasting. There are people who believe that
> > downcasting is a sign of bad design even -- and by downcasting they
> > include any kind of switch on type semantic (though i can't find any
> > of the "casting considered harmful" pages at the moment).
>
> But such checked downcasting does not break static type safety so it
Checked downcast? you mean a cast that can fail? that would be a
*type error*, and it would not occur until runtime, your language
could force you to handle that case, in your earlier example
void do_special_thing(..);


you would be required to write an implementation for the base class
which would be used as the default fall back, but at this point it's
looking more and more like a convoluted approach to abstract methods
in ordinary OO languages.


> > There are plenty of ways to not use a cast to accomplish something.


> And that's what my example accomplishes -- there is complete static type
> safety. There is no way to compile code which then could not dispatch in
> runtime. There are executions paths depending on type, but all possible
> types are covered.


Yes, but it achieves it's complete static type safety, if, and only
if, there is a finite set of subtypes, all of which must be known at
compile time.


> Ad mine is that limited (checked) downcasts do not break static type safety
> either.
You need to define what a checked down cast is -- it has no meaning
currently, from my earlier example:
    ...
    B myB = (B)myA;
    ...


What happens when the cast fails? you say it's checked, but i cannot
see a way for the check to occur at compile time, therefore it mmust
occur at runtime, this doesn't mean that it isn't type safe, it just
means it is not statically verifiable.


Cheers,
    Oliver

Return to the comp.compilers page.
Search the comp.compilers archives again.