[Haskell-cafe] Signature for non-empty filter

[Henning Thielemann]

On Wed, 6 Feb 2008, 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

If the type checker does not terminate because the checked function does
not terminate on the example input, then the function does not pass the
type check and as a compromise this would be ok.