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

[John Clements <address@hidden>]

On Dec 15, 2003, at 2:40 PM, Jan-Willem Maessen wrote:

> John Clements <clements@brinckerhoff.org> writes:
>> Based on my conversation with Philippe Meunier, I'm going to refine my
>> argument:  My claim is that you can't write down a deterministic
>> operational semantics for Haskell that doesn't involve the result of
>> the type proof.
>
> Correct.
>
>> My further claim is that for other languages, you can.
>
> You'll need to immediately rule out languages like Fortran, Pascal,
> Modula-2, Java, and so forth which permit "+" to mean both "integer
> add" and "floating point add".

No, wait a minute. I'm not excluding semantics that use type 
information, just those that use the result of the type proof.  That 
is, I'm perfectly "happy" with languages that dispatch on the types of 
their arguments, just not those that use the "future" information 
provided by the type proof.

Let's see if I can be clearer.  Suppose I have a Haskell-like language 
where the type-checker is oracular; that is, I supply a program, and 
the type-checker simply says "yes" or "no".  Now, can we write down a 
deterministic operational semantics for the user's program?   I claim 
that you're going to run into trouble disambiguating the various calls 
to 'read.'

Are there other programming languages that have this property?



... Now, it may well be that you think this is not a serious problem, 
and that it will be very rare for the type-checker to successfully 
construct a proof which gives a term a type 'A' when the programmer 
intended type 'B'.  I feel that this may be a problem, though legions 
of Haskell programmers are (even now!) proving me wrong. ...

john