On 20-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> [Lennart wrote:]
> > [Nick Kallen wrote:]
> > > To what
> > > extent will a program that type checks completely fail to follow its
> > > specification? Can someone give specific examples?
> >
> > It's trivial to construct examples. Take sorting
> > sort :: (l :: [a]) -> ComplicatedTypeToSpecifySorting l
> >
> > Well, here's an implementation:
> >
> > sort xs = sort xs
> >
> > It's type correct, but doesn't really do what you want.
>
> but if you say
>
> sort [] = []
> sort (x:xs) = sort elts_lt_x ++ [x] ++ sort elts_greq_x
> where
> elts_lt_x = [y | y <- xs, y < x]
> elts_greq_x = [y | y <- xs, y >= x]
>
> will the type checker say "yes," and can you believe it?
No, the type checker will say "no", because the
"ComplicatedTypeToSpecifySorting" must contain
a proof of correctness, and the value returned from
your sort function doesn't include the proof of correctness.
But if you do include a proof of correctness, then
it will typecheck.
> What if you do this:
>
> sort (x:xs) = sort elts_lt_x ++ sort elts_greq_x
> where
> elts_lt_x = [y | y <- xs, y < x]
> elts_greq_x = [y | y <- xs, y >= x]
>
> (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?
If you return the same proof of correctness that you used
for the earlier definition of sort, then no it won't type check.
But if you return a proof defined as e.g.
proof = proof
then if I understand things correctly it will type check.
--
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.
