[Haskell-cafe] is proof by testing possible?

Ketil Malde ketil at malde.org
Mon Oct 12 15:26:43 EDT 2009

Neil Brown <nccb2 at kent.ac.uk> writes:

>> swap :: (a,b) -> (b,a)

>> We don't need to test it at all, it can only do one thing, swap its
>> arguments. (Assuming it terminates.)

> swap = undefined

> Terminates and does not swap its arguments :-)

I think this counts as non-termination, and that for semantic purposes,
any bottom value -- infinite loops, exceptions, undefined -- is treated

If I haven't seen further, it is by standing in the footprints of giants

More information about the Haskell-Cafe mailing list