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.)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe