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

[John Clements <address@hidden>]

On Dec 17, 2003, at 4:50 PM, Ken Shan wrote:

>
> On 2003-12-17T16:25:11-0500, John Clements wrote:
>>> (1) the typing environment, just like in ML, and (2) the type 
>>> assigned
>>> to the expression you are interested in.  Item (2) is just as local
>>> as (1).
>>
>> Determining (2) can only be done by unification over the whole 
>> program,
>> no?
>
> 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.


john