On Tue, 5 Feb 2008, Dan Licata wrote:
[CC'ed to the agda mailing list as well]
On Feb05, Henning Thielemann 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)) 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
You can definitely do this with dependent types. Here's a way to do it in Agda 2:
Thanks for your detailed answer! I don't fully understand the Agda code, but I record that there is another system which allows such kind of types. Now, 'filter' was a particular example where the type constraint can be reformulated as constraint on the element test 'f'. However there might be a composed function like stupidFilter = filter odd . map (2*) I assume that Agda lets me forbid such functions by properly designed types, too.