[Haskell-cafe] Re: Best idiom for avoiding Defaulting warnings with
ghc -Wall -Werror ??
apfelmus at quantentunnel.de
Sun Jun 24 07:36:38 EDT 2007
Neil Mitchell wrote:
>> 1) The programmer has to detail in some form the proof that his program
>> terminates. Arguably, he ought to do so anyway but he doesn't need to
>> write his proof in a way that can be checked by a dumb computer. Take
>> for example
>> minimum = head . sort
> minimum [1..] gives _|_ non-termination
> miniumum [1,_|_,3] gives _|_ while head [1,_|_,3] doesn't.
> Termination is all a bit more complex once you get to laziness.
Oops, the example was not meant for termination but for the invariants.
I wanted to say that the code of minimum is likely to be shorter than a
computer-checkable proof that shows that its result is indeed the
smallest element from the list.
More information about the Haskell-Cafe