On 22-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> > > min2 :: [a] -> a
> > > min2 ((l:ls) :: [a] <= Sorted) = l
> > > min2 l = min l
> >
> > What's the semantics of that supposed to be?
> > If the list is not known to be definitely sorted,
> > will it check sortedness at runtime?
>
> No.
>
> > If not, then the semantics could be nondeterministic,
> > in general, so you've broken referential transparency.
>
> If this is true, then what I'm doing is horrible. But I don't see how this
> leads to nondeterminism or broken referential transparency. min2 returns the
> same value for the same list, but it's simply more efficient if we happen to
> know some more information about the list.
In this particular case that happens to be so. But it's not true in
general. 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.
You could of course simply say that it's the programmer's
responsibility to ensure that the two cases have equivalent semantics,
and if they're not, then the behaviour is undefined.
And indeed, for this sort of feature, that may well be the only
reasonable approach. But in that case I think there should be some
highly visible marker, e.g. something containing the word "unsafe"
or "unchecked" somewhere in the code, to flag it as a dangerous construct.
--
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.
