On 24-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> Fergus Henderson <[EMAIL PROTECTED]> writes:
> > What if the body of min2 were defined so that it returned
> > something different in the two cases? Your code has no proof that the
> > code for the two cases is equivalent. If it's not, then the behaviour
> > would depend on whether the compiler could deduce that a particular
> > argument had type Sorted or not. And that in turn could depend on the
> > amount of inlining etc. that the compiler does.
>
> I would assume that any language with this feature would have a
> precise specification of type inference sufficient to determine which
> of the two cases was used. Without such a specification, portable
> programming with dependent types is impossible; programs would compile
> under one "smart" compiler (which does more inference) and fail with a
> type error on another.
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.
--
Fergus Henderson <[EMAIL PROTECTED]> | "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh> | but source code lives forever"
PGP: finger [EMAIL PROTECTED] | -- leaked Microsoft memo.
