[Haskell-cafe] Signature for non-empty filter

[Henning Thielemann]

On Wed, 6 Feb 2008, Bulat Ziganshin wrote:

> Hello Henning,
>
> Wednesday, February 6, 2008, 5:09:56 PM, you wrote:
>
> >> > Is Haskell's type system including extensions strong enough for describing
> >> > a function, that does not always return a trivial value? E.g.
> >> >    (filter (\x -> x==1 && x==2))
> >>
> >> such things may be detected by (too) smart compiler, but in general
> >> it's undecidable: filter (if LifeHasMeaning then const True else odd) ;)
>
> > As I said, if the programmer could specify an input on the type level for
> > which the output is non-trivial, then this would solve the problem.
>
> 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.