Re: Haskell 2 -- Dependent types?

[Fergus Henderson]

On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
> 
> > (i.e., you leave out the pivot [x])
> > 
> > Obviously the result of sort will no longer be a permutation of its
> > argument. Will this then not type check?
>
> No, the proof (whereever it is) would no longer type check.

As I understand it, this is not necessarily true:
if the proof contains loops, it might type check,
even though it is not really a valid proof.

So even though the sort function itself doesn't loop,
if its proof of correctness has loops, then the
sort function might return the wrong answer.

Do I understand this correctly?

-- 
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.