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

[John Clements <address@hidden>]

On Dec 17, 2003, at 3:08 PM, Kevin S. Millikin wrote:

> On Wednesday, December 17, 2003 12:51 PM, John Clements
> [SMTP:clements@brinckerhoff.org] wrote:
>>
>> Cribbing again from my response to Ken, I think the core of the
> debate
>> has to do with typeclasses as a program abstraction mechanism that is
>> inherently non-local.
>
> Invoking a first class function is "inherently non-local".

Let me advance/retreat (depending on your point of view) to what I 
believe is a restatement of my prior claim.

Informally: Let's say I'm trying to reason about a piece of code.  
Let's say that code is

if (f(x)) then g() else h();

Let's further assume that I know what the value of x is, and what the 
values of f and g are.  The hope is that I can then know what the 
language will evaluate f(x) to, and therefore figure out whether g or h 
will be called.  I think everyone agrees that we want this.

The question, then is what it means to "know the value" of f and g.  In 
Scheme, ML, Java, & most other languages you can think of, you can 
easily identify the parts of the program that are part of the value of 
f and g.  In particular, only parts of the program that have been 
evaluated will affect the values of f and g.[*]

In Haskell, as I understand it, there are a certain number of cases in 
which these parts of the program will _not_ be sufficient to determine 
what's going to happen next.  In particular, I have to examine the type 
proof of the program--the whole program--to see how things were 
resolved in order to figure out what's going to happen next.

Put more concisely, you can't write down an operational semantics that 
doesn't involve computing the result of the type proof.

john

[*] plus some static set of type declarations.