On 2003-12-17T17:05:29-0500, John Clements wrote:
> >Yes in general, but (1) is also spread all over the whole program, and
> >that's the case in ML as well, as I tried to explain above.
> Okay, good, so I'm not crazy.
>
> Yes, unification is whole-program for ML, BUT the results of the type
> proof are not needed to evaluate the program, as they are in Haskell.
>
> No one seems to be refuting the point that a difference between ML and
> Haskell is the inability to formulate a reduction semantics that
> ignores the type proof.
Right. C++ is similar to Haskell in this regard.
You seem to be (also) talking about a different inability: the inability
to formulate a reduction semantics that works on one part of a program
at a time, in other words the inability to know how an expression will
evaluate without looking at the rest of the program. To the extent that
this inability holds, it holds of both Haskell and ML. For example,
you need to know the value of f in order to know how an expression
containing f evaluates, and the value of f could come from anywhere in
the program.
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
SigChangeCGI.hs:42:Program error: {head []}
Attachment:
signature.asc
Description: Digital signature