[Haskell-cafe] Re: Best idiom for avoiding Defaulting warnings with ghc -Wall -Werror ??

[apfelmus]

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.

Regards,
apfelmus