John Clements claims (I think correctly) that "you can't write down a
deterministic operational semantics for Haskell that doesn't involve
the result of the type proof". He also says that "for other languages,
you can", excluding C because it is nondeterminism. In fact, even a
deterministic C++ doesn't have a deterministic operational semantics
that doesn't involve the result of the type proof, because -- although
C++ doesn't resolve overloading by return type -- you can use output
reference arguments to rewrite your C++ code to always return void.
Indeed, I can write
int x;
cin >> x;
return x/2;
as well as
bool x;
cin >> x;
return !x;
to take advantage of overloading on operator>>. In C++, such use of
overloading does not make my program more concise, because I need to
write down the type of x explicitly. A more trivial example of how
types affect behavior in C++ is
struct A { A() { cout << "Constructing A" << endl; }
struct B { B() { cout << "Constructing B" << endl; }
int main() { A x; }
Here the type of x affects which constructor gets called. Of course,
you could regard the type declaration for x to be part of the program
proper rather than an annotation, but then again, one could regard type
annotations in Haskell to be part of the program proper rather than an
annotation, and devise an operational semantics whose very first stage
performs type-checking and type-class overloading resolution.
People including John Clements are concerns that the Haskell type
checker may "successfully construct a proof which gives a term a type
'A' when the programmer intended type 'B'". The existence of principle
types, and the type checker's guarantee to produce it, rules out such a
concern.
A related concern is Joe Marshall's worry that programs can be more
fragile, for example when dvi2ps is changed to produce PDF as well. But
the soundness of the type system prevenst new-and-improved dvi2ps from
possessing the type "dvi -> ps", so the problem is discovered and fixed
before eve TeX is run. This is a classical example of how static typing
can catch at least some problems early.
In the end, I don't think any amount of CPS-conversion will make
dispatching on the (return) type of functions seem any less weird (or,
for that matter, more weird) to people. For example, Joe Marshall
comments that "it seems weird to dispatch on the type of CONT when
ultimately we are interested not in CONT but in FOO. Changes to FOO
must take into account all the continuations that may be supplied to
FOO." Reverting to direct style, that is just saying that it seems
weird to dispatch on the return type of a function when ultimately
we are interested not in the return but in the function. Changes to
the function must take into account all the ways in which it may (be
asked to) return. Haskell type classes make an open-world assumption
that, like generic functions or virtual methods or many other things,
allow what some people might prefer to think of as a single function
with internal dispatch to be extended incrementally while maintaining
separate compilation.
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Remember 9/11 * "It's untidy. And freedom's untidy. And free people are free
to make mistakes and commit crimes and do bad things." -- Donald Rumsfeld
China has listed the organization behind http://www.uygur.org/ as terrorist.
(http://www.mps.gov.cn/webpage/showNews.asp?id=1118&biaoshi=bitGreatNews)
Attachment:
signature.asc
Description: Digital signature