Typing and semantics [dynamic vs. static typing]

[Jan-Willem Maessen <address@hidden>]

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".

In a dynamically typed language, you don't naturally disentangle the
type semantics and the value semantics at all.  Why should it be so
disturbing that program semantics depend on types even in a
strongly-typed language?

-Jan-Willem Maessen
jmaessen@alum.mit.edu