[Haskell-cafe] Signature for non-empty filter
Henning Thielemann
lemming at henning-thielemann.de
Tue Feb 5 10:01:27 EST 2008
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))
will always compute an empty list. Using an appropriate signature for
the function it shall be rejected at compile time, because it is probably
a mistake - probably (filter (\x -> x==1 || x==2) xs) was meant. I assume
that the type must contain somehow an example input for which the function
value is non-trivial. If Haskell's type system is not strong enough, what
about dependently typed languages like Cayenne or Epigram? (I know,
theorem provers have no problem with such types.)
More information about the Haskell-Cafe
mailing list