Re: Typing and semantics [dynamic vs. static typing]

[John Clements <address@hidden>]

On Dec 17, 2003, at 5:33 PM, Ken Shan wrote:

> On 2003-12-17T17:05:29-0500, John Clements wrote:
>>> Yes in general, but (1) is also spread all over the whole program, 
>>> and
>>> that's the case in ML as well, as I tried to explain above.
>
>> Okay, good, so I'm not crazy.
>>
>> Yes, unification is whole-program for ML, BUT the results of the type
>> proof are not needed to evaluate the program, as they are in Haskell.
>>
>> No one seems to be refuting the point that a difference between ML and
>> Haskell is the inability to formulate a reduction semantics that
>> ignores the type proof.
>
> Right.  C++ is similar to Haskell in this regard.

I'm sorry, I don't see that.  Can you give me that example again?  In 
fact, I don't see how this can arise without type inference.

> You seem to be (also) talking about a different inability: the 
> inability
> to formulate a reduction semantics that works on one part of a program
> at a time, in other words the inability to know how an expression will
> evaluate without looking at the rest of the program.  To the extent 
> that
> this inability holds, it holds of both Haskell and ML.  For example,
> you need to know the value of f in order to know how an expression
> containing f evaluates, and the value of f could come from anywhere in
> the program.

Forgive me; that's not what I meant at all, and I'm sorry if I gave you 
that impression.  Values flow from one part of the program to another 
in every operational semantics I'm familiar with.  The step that 
confuses me is where (in Haskell) I have to make a control-flow 
decision based on type information associated with code that hasn't yet 
been executed.



As an aside; my basic point, as someone who has not done a lot of 
Haskell coding, is that Haskell seems to have this funny feature that 
would appear (to me) to make it difficult to reason about programs.  
That's all, and I'm certainly willing to let this drop. Modulo 
everyone's closing statement, of course...

john