5 Feb
2008
5 Feb
'08
11:01 p.m.
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.)