Fergus Henderson <[EMAIL PROTECTED]> writes:

> Certainly a language with dependent types should define exactly what
> types the type checker will infer.  But when generating code, the
> compiler ought to be able to make use of more accurate type information,
> if it has that information available, wouldn't you agree?
> I think it would be most unfortunate if simply adding more accurate type
> information could change a program's behaviour.

I'm not sure if that last sentence refers to 1) the compiler inferring
more accurate type information or 2) the user adding a more accurate
type declaration.

1) There's a word for "optimizers" that change the meaning of a
program (in ways not allowed by the language spec); that word is
"buggy".

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.

Carl Witty
[EMAIL PROTECTED]


Reply via email to