On 2003-12-17T13:31:48-0800, Christopher Dutchyn wrote:
> > Perhaps it is relevant for me to point out that you don't have to
> > examine the type proof for the -whole- program to know the operational
> > behavior of the expression you are interested in. You only need to know
> > (1) the typing environment, just like in ML, and (2) the type assigned
> > to the expression you are interested in. Item (2) is just as local
> > as (1).
>
> But, where does (1) come from? The whole program. I can use a typeclass
> constraint to "forward-reference" an implementation of a procedure that
> may appear anywhere in the program. The type-environment ends up
> containing the proven types of the entire program. Admittedly, that's not
> the entire proof, but pretty close.
An operational semantics for ML necessarily
- either requires as input values for every free variable in the term
being evaluated (this is the "explicit substitutions" way);
- or can only evaluate closed terms (this is the "implicit
substitutions" way).
In this regard, Haskell is no different from ML. If what you mean by
"use a typeclass constraint to 'forward-reference' an implementation of
a procedure that may appear anywhere in the program" is what I think you
mean, then recursive let does that in ML. If not, could you please give
a concrete example of what you mean?
> Haskell lacks a decent module system, and so offer decent type and
> implementation hiding capabilities. I asked Tim Sheard about this, and
> he pointed out that to have an ML-like module system would require rank-n
> types. Rank-2 is already hard. CaML gives recursive modules, requiring
> module fixpoints over rank-infinity types. Ouch, my head hurts.
Actually (going off to a tangent), it's not so hard to get the hang of
using rank-n types in GHC as your module system... I don't know about
recursive modules though.
On 2003-12-17T16:25:11-0500, John Clements wrote:
> >(1) the typing environment, just like in ML, and (2) the type assigned
> >to the expression you are interested in. Item (2) is just as local
> >as (1).
>
> Determining (2) can only be done by unification over the whole program,
> no?
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.
--
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