On Feb06, Henning Thielemann wrote:
On Tue, 5 Feb 2008, Dan Licata wrote:
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.
I think what you want to say now is not just (filter f l) is type correct when there is some argument on which f returns true but (filter f l) is type correct when there is some *element of l* on which f returns true Here is one way to say this with dependent types: data SatBy {A : Set} : (A -> Bool) -> List A -> Set where Here : {f : A -> Bool} {x : A} {xs : List A} -> Check (f x) -> SatBy f (x :: xs) There : {f : A -> Bool} {x : A} {xs : List A} -> SatBy f xs -> SatBy f (x :: xs) fancyfilter2 : {A : Set} (f : A -> Bool) (l : List A) -> SatBy f l -> List A fancyfilter2 f l _ = stdfilter f l The idea is that SatBy f l proves that there is some element of l on which (f x) is true. 'Here' says that this is true if (f x) is true on the head of the list; 'There' says that this is true of (x :: xs) if it's true of xs. Of course, now to call fancyfilter2, you need to prove this property of your f and your l. You won't be able to do this for 'odd' and 'map (2*) x', but you would be able to do this for, e.g., 'even' and 'map (2*) xs where xs is non-nil'. -Dan