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?
If not, then the semantics could be nondeterministic,
in general, so you've broken referential transparency.
If so, what's the difference between that and this?
min3 :: [a] -> a
min3 (l:ls) | sorted (l:ls) = l
min3 l = min l
Here I'm just using an ordinary guard,
and `sorted' is just an ordinary function.
> Heh. I'm not seriously advocating adding my magic operator to the language,
> but I am pointing out that explicitly passing around proofs is a pain in the
> ass. This is good evidence that Fergus is right when he says: "As a
> programmer, I want the two to be clearly separated." However, his clear
> separation would not allow min2, would it?
It would allow min3, above. I'm not sure what min2 buys you over min3.
If the `Sorted' type is defined in terms of `sorted', then a compiler
ought to be able to optimize min3 just as well as min2, I think.
--
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.
