> 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.
See my email where I derive a type for apply. Note how by using different
types, you can change the range of apply to:
a,
or
F a * -- i.e., a, a->a, a->a->a, ...
By restricting the range. So different types does equal different behavior.
