[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: -- booleans, just like in Haskell: data Bool : Set where True : Bool False : Bool _||_ : Bool -> Bool -> Bool False || False = False _ || _ = True _&&_ : Bool -> Bool -> Bool True && True = True _ && _ = False not : Bool -> Bool not True = False not False = True -- Now our first use of dependency: we need to turn a boolean value -- into the proposition that it's true. We do this with a type -- Check b where only Check True is inhabited; Check False is not data Check : Bool -> Set where OK : Check True -- a function f is satisfiable if there is some input on which it returns true data Sat {A : Set} : (A -> Bool) -> Set where Witness : {f : A -> Bool} -> (a : A) -> Check (f a) -> Sat f -- here's an easy one: example : Sat (\x -> x || not x) example = Witness True OK -- there's no way to prove this one, as each case you'd need -- a term of type Check False in the empty context example2 : Sat (\x -> x && not x) example2 = Witness True {! need a term of type Check False !} example2 = Witness False {! need a term of type Check False !} -- Now you can use Sat f as a precondition to filter: data List (A : Set) : Set where [] : List A _::_ : A -> List A -> List A filter : {A : Set} (f : A -> Bool) -> Sat f -> List A -> List A filter f sat [] = [] filter f sat (x :: xs) with f x ... | True = x :: (filter f sat xs) ... | False = filter f sat xs -- Note that the code doesn't use sat at all, so we might as well have -- written: stdfilter : {A : Set} -> (A -> Bool) -> List A -> List A stdfilter f [] = [] stdfilter f (x :: xs) with f x ... | True = x :: (stdfilter f xs) ... | False = stdfilter f xs fancyfilter : {A : Set} (f : A -> Bool) -> Sat f -> List A -> List A fancyfilter f _ l = stdfilter f l That is, the Sat f argument is used only to impose the precondition that you wanted, and it has no bearing on how filter actually computes. Of course, the trade-off here is that to call filter you have to cough up an argument on which the function is satisfiable. I don't know a way to get the compiler to construct this proof for you, but maybe someone who has done more dependent programming that I have knows a trick. You may be able to mimic this using GADTs, but it likely won't be as direct, because the 'Check (f a)' argument to Sat talks about the very code that you're passing to filter. -Dan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe