[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Typing and semantics [dynamic vs. static typing]
On Dec 15, 2003, at 2:40 PM, Jan-Willem Maessen wrote:
> John Clements <email@example.com> 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.
>> 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
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. ...