[Haskell-cafe] Signature for non-empty filter

[Dan Licata]

Let's be careful here: decidability is only relevant if you want to
*automatically* prove calls to filter correct.  It is certainly possible
to give a type system/specification logic for reasoning about all
functions written in a Turing-complete language (e.g., all Haskell
functions).  In such a type system/logic, you will be able to prove that
particular functions have particular results (e.g., "that function f
over there maps 4 to true").  If you give filter the type/specification
that Henning wants, you may not be able to get a computer to
automatically validate all "correct" calls to filter, where "correct"
means that I can prove, in the specification logic, that the predicate
is satisfiable.  However, you can get a computer to validate some calls
to filter, and a human may be able to validate others by hand.

I.e., it's not necessary to restrict the class of functions you consider
if you're willing to give up on full automation.  So I disagree with the
"only if" below.  

-Dan

On Feb06, Bulat Ziganshin wrote:
> Hello Henning,
> 
> Wednesday, February 6, 2008, 6:09:28 PM, you wrote:
> 
> >> it's another question: you can describe trivial values using type
> >> system, but can't prohibit them using it - it's impossible because you
> >> can't check for arbitrary algorithm whether it will be finally stopped
> 
> > I could consider the function buggy, if it does not terminate on the given
> > example.
> 
> it's impossible to check for *arbitrary* function call whether it will be
> terminated. seems that you don't have formal CS education? :)
> 
> so one can develop set of functions that are guaranteed to be
> terminated or guaranteed to be non-trivial. but it's impossible to
> check for arbitrary function whether it's trivial and even whether it
> will terminate for particular data
> 
> this means that answer to original question - one can ensure that
> argument for filter is non-terminating function only if these
> functions are written using some special notation which doesn't allow
> to write arbitrary turing-complete algorithms
>