[Resend - mlist trouble; apologies if you've already
 received it.  -moderator]

Lennart Augustsson <[EMAIL PROTECTED]> writes:

> > 2) Yes, I agree that the possibility that user-supplied type
> > declarations can change the meaning of the program is a strike against
> > the idea.
> I don't find that so strange.  If there are no principal types
> (which we can't hope for), then user added signatures can
> have the effect of changing the meaning of a program.

I've lost track of what we're talking about here.  In what system can
we not hope for principal types?  (I believe that there are type
theories with dependent types, such as the one in Thompson's _Type
Theory and Functional Programming_, where each term has at most one
type; so it can't just be dependent types that disallow principal
types.)

> BTW, Haskell already has this property.  There are programs that
> yield different results depending on if you have a type signature
> or not (and it's not because of the numeric defaulting).

Could you give an example?  I can't think how to construct a 
Haskell 98 program with this property (unless you count "compiling"
and "failing to compile" as different results).

Carl Witty
[EMAIL PROTECTED]


Reply via email to