Re: More on dispatching by function return type

[John Clements <address@hidden>]

On Dec 16, 2003, at 5:05 PM, Ken Shan wrote:

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

This is exactly the distinction I'm getting at.  An operational 
semantics whose domain is "programs the programmer writes down" is 
going to get to see the types written down by the programmer, and _not_ 
those inferred by the type system. So the C++ situation is different 
from the Haskell situation.  A "very first stage" which performs 
type-checking is explicitly fenced out by the oracular type-checker I 
tried to describe before.

At the end of the day, this is an argument about a sociological 
problem: how confused can the programmer get?  My point is that I can 
draw a fairly well-defined "line in the sand" between languages which 
"have an operational semantics" and those which don't.  The problem 
here is one of locality: how far away in the program do I have to look 
in order to understand what's happening in my little corner of it?  In 
languages like ML, Scheme, etc. etc. etc., I can figure out what a 
function call will do, knowing only the inputs and the code of the call 
itself (plus all that icky mutable state).  In the scenario you've 
described, Haskell appears to make that impossible.

Let me take a step back, as well, and point out that the _whole_point_ 
of purely functional programming is to enable componential reasoning 
about program fragments; it's curious that Haskell, of all languages, 
would break this.

Keep in mind that I have no problem at all with inference as a part of 
type-checking; ML falls into the "has an operational semantics" 
category, as far as I can tell.  It's just that the result of 
type-checking is simply a "yea" or "nay" on whether the program is 
well-typed.


*******

Here's the other side of the coin, as I see it: Macros.  Macros (e.g. 
in Scheme) _also_ have the "bad" property that unless I know what 
macros are present, I cannot hope to understand what a piece of code 
does.  My take on this (not an original thought, of course) is that the 
macros are part of the language, and not part of the program, so the 
operational semantics for a program written in Scheme must already take 
into account the macros that are present.

So how does this apply to Haskell?  It would appear that Haskell's type 
classes are a different form of program abstraction, and therefore that 
just as a Scheme program expands away the macros to reveal the "core" 
program, a Haskell program is elaborated through type class resolution 
and type checking into the "core" program.  The difference I'm 
suggesting is that in the Scheme case, I can push these expansion rules 
into the language's semantics, because they're not whole-program 
transformations.  In Haskell, on the other hand, type-class resolution 
and type-checking certainly appear (pardon my ignorance) to be global 
transformations.

john