[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: Typing and semantics [dynamic vs. static typing]
> 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
> 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.