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

["Kevin S. Millikin" <address@hidden>]

> That is, when the meaning of a function call depends not just on
> its inputs but also on how its output is used, it could be very hard 
to
> reason about a program.

Yes, it sometimes can.  You are seeing the interaction of type 
inference and overloading (overloading that is based on return type as 
well as argument type, unlike some other languages).

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

Of course.  Typeclasses in Haskell implement overloading, or ad hoc 
polymorphism (dispatch to separate implementations based on type).  Why 
would you expect to be able to give a semantics for dispatch on type 
that doesn't involve types?

By the way, Ken's example might suggest that the choice of read 
function is resolved statically, but that's not (always) the case 
(though Ken knows this of course, that's why he talks about an 
inifinite family of types).  Also, programs using typeclasses can be 
translated into programs that do not and that can be assigned a type by 
H-M.  The implementation of typeclasses is actually really slick, 
something that even a DTer should appreciate.

-- Kevin