Re: the forward method [dynamic vs. static typing]

[John Clements <address@hidden>]

On Dec 15, 2003, at 3:27 PM, Neelakantan Krishnaswami wrote:

> Joe Marshall writes:
>> John Clements <clements@brinckerhoff.org> writes:
>>
>>> Typically, type systems help you to construct a proof that certain
>>> errors cannot arise during evaluation.  When parts of that proof are
>>> used to alter the evaluation itself, you suddenly have a class of
>>> _runtime_ errors (or rather, "mis-behaviors") that can only be
>>> understood by examining the type proof.
>>
>> I think that John has identified what it is that made me
>> uncomfortable with this style.  I generally think of the type system
>> as meta information.  Intertwining the control flow with the meta
>> information about the value flow not only makes it hard for humans
>> to reason about the program, it makes it hard for programs to reason
>> about it as well.
>
> But OO languages already permit this sort of computation! If
> you CPS-converted Ken's example, then all of the cases in which
> the behavior depended on the return type would turn into cases of
> argument type dispatch. Am I misunderstanding your point somehow?

No, I don't believe this is an accurate characterization of the problem.

Objection 1:

Do such languages permit higher-order dispatch?  That is:

if (method-accepts-double(kont.invoke)) then
{
      kont.invoke(read-a-double());
} else {
     kont.invoke(read-a-string());
}

Objection 2:

Are these languages where  the type of kont.invoke may be inferred, 
rather than explicitly specified?

Objection 3:

Even in the presence of a language that satisfies objection 1 and 2, 
you're still arguing that it's just as easy to mentally CPS-convert and 
reason about the resulting program as it is to reason about the 
original.  Bleargh!

At least, that's  what I'm seeing.


john