Signature for non-empty filter
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.)
Hello Henning, Tuesday, February 5, 2008, 6:01:27 PM, you 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))
such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;) -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Tue, 5 Feb 2008, Bulat Ziganshin wrote:
Hello Henning,
Tuesday, February 5, 2008, 6:01:27 PM, you 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))
such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;)
As I said, if the programmer could specify an input on the type level for which the output is non-trivial, then this would solve the problem.
Hello Henning, Wednesday, February 6, 2008, 5:09:56 PM, you 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))
such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;)
As I said, if the programmer could specify an input on the type level for which the output is non-trivial, then this would solve the problem.
it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Wed, 6 Feb 2008, Bulat Ziganshin wrote:
Hello Henning,
Wednesday, February 6, 2008, 5:09:56 PM, you 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))
such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;)
As I said, if the programmer could specify an input on the type level for which the output is non-trivial, then this would solve the problem.
it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped
I could consider the function buggy, if it does not terminate on the given example.
Hello Henning, Wednesday, February 6, 2008, 6:09:28 PM, you wrote:
it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped
I could consider the function buggy, if it does not terminate on the given example.
it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :) so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Wed, 6 Feb 2008, Bulat Ziganshin wrote:
Hello Henning,
Wednesday, February 6, 2008, 6:09:28 PM, you wrote:
it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped
I could consider the function buggy, if it does not terminate on the given example.
it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :)
so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.
Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination. Matthew
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote:
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.
Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination.
I would second this --- letting the compiler go only to discover that it's been running for the last 3 hours because it's diverging seems like a wasted 3 hours. jcc
On Wed, 6 Feb 2008, Jonathan Cast wrote:
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote:
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.
Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination.
I would second this --- letting the compiler go only to discover that it's been running for the last 3 hours because it's diverging seems like a wasted 3 hours.
There is the same problem with unit testing: Tests that eat too much time have to be rewritten. Same here: If the automatic proof takes too long - choose a simpler example input (if possible). But Dan's point definitely applies here - there is no need to automatically prove every instance, if there is a possibility to do a proof manually.
On 7 Feb 2008, at 12:07 AM, Henning Thielemann wrote:
On Wed, 6 Feb 2008, Jonathan Cast wrote:
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote:
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.
Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination.
I would second this --- letting the compiler go only to discover that it's been running for the last 3 hours because it's diverging seems like a wasted 3 hours.
There is the same problem with unit testing: Tests that eat too much time have to be rewritten.
Tell that to my co-workers...
Same here: If the automatic proof takes too long - choose a simpler example input (if possible).
3 hours wasn't chosen arbitrarily --- I've had suites of unit tests take that long, and that's realistically about when I'd check for divergence. And in a large program I'd hate to recompile only to discover that it's taking so long because *I* introduced an infinite loop into the compiler.
But Dan's point definitely applies here - there is no need to automatically prove every instance, if there is a possibility to do a proof manually.
jcc
Hello Henning, Thursday, February 7, 2008, 12:29:02 AM, you wrote:
it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :)
so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.
how you can check that some code doesn't terminate? ;) it may be just a bit too slow. we again return to my original point - we can check for *some* representations of trivial functions values, but we can't *ensure* that some computation is non-trivial -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Am Mittwoch, 6. Februar 2008 18:39 schrieb Bulat Ziganshin:
[…]
this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms
And this is exactly what Agda, Epigram, Coq, etc. do. Note however that those systems are not very restrictive. It’s possible, for example, to define Ackermann’s function in Agda:
module Ackermann where
data Nat : Set where
O : Nat
↑_ : Nat -> Nat
ackermann : Nat -> Nat -> Nat ackermann O m = ↑ m ackermann (↑ n) O = ackermann n (↑ O) ackermann (↑ n) (↑ m) = ackermann n (ackermann (↑ n) m)
Best wishes, Wolfgang
Let's be careful here: decidability is only relevant if you want to *automatically* prove calls to filter correct. It is certainly possible to give a type system/specification logic for reasoning about all functions written in a Turing-complete language (e.g., all Haskell functions). In such a type system/logic, you will be able to prove that particular functions have particular results (e.g., "that function f over there maps 4 to true"). If you give filter the type/specification that Henning wants, you may not be able to get a computer to automatically validate all "correct" calls to filter, where "correct" means that I can prove, in the specification logic, that the predicate is satisfiable. However, you can get a computer to validate some calls to filter, and a human may be able to validate others by hand. I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the "only if" below. -Dan On Feb06, Bulat Ziganshin wrote:
Hello Henning,
Wednesday, February 6, 2008, 6:09:28 PM, you wrote:
it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped
I could consider the function buggy, if it does not terminate on the given example.
it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :)
so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data
this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms
Hello Dan, Thursday, February 7, 2008, 4:04:03 AM, you wrote:
I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the "only if" below.
ok, read this as "computer can ensure...", because it was exactly the original question - "can computer check that any given function in turing-complete language is non-trivial?"
this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms
-- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Thu, 7 Feb 2008, Bulat Ziganshin wrote:
Thursday, February 7, 2008, 4:04:03 AM, you wrote:
I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the "only if" below.
ok, read this as "computer can ensure...", because it was exactly the original question - "can computer check that any given function in turing-complete language is non-trivial?"
My original question according to http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html was "Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value?"
Hello Henning, Thursday, February 7, 2008, 4:27:30 PM, you wrote:
ok, read this as "computer can ensure...", because it was exactly the original question - "can computer check that any given function in turing-complete language is non-trivial?"
My original question according to
http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html was "Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value?"
where Haskell is *turing-complete* *computer* language this allows to answer to your question that you need to use special, non-turing language if you want to check arbitrary functions for non-trivialness. one example of such language: data Func = ConstTrue | ConstFalse and dependent-typed languages provides you (afaiu) much richer facilities to describe functions for which you still may prove something useful so, if you term "function" includes the Func type, the answer is "yes", but if you mean usual haskell functions, the answer is no -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Hi Bulat, Once again, let's be careful about what "check arbitrary functions for termination/non-trivialness" means. If you mean, "decide via an algorithm whether a function is terminating on all inputs", then yes, you need to restrict the class of functions. If you mean "prove in some logic that a function is terminating on all inputs", then there is no reason to restrict the class of functions. (Think of it this way: the truth of propositions in that logic may not be decidable, so the existence of a proof of termination in that logic does not imply an algorithm for deciding termination.) ACL2 and Twelf are practical systems built around this second kind of reasoning. In these systems, you write down partial functions (in a functional notation in ACL2, in a logic programming notation in Twelf) and then prove that they are terminating, and therefore total. Both systems permit the definition of all computable functions on the natural numbers (worst comes to worst, you can write an interpreter for the untyped lambda-calculus). So in neither system is it *decidable* whether a function is terminating. However, both provide helpful tools for proving that individual functions are terminating, and in both systems you can help these tools along yourself when the automated reasoning doesn't do the job. Many dependently typed programming languages have this flavor, in that you can prove propositions that are not decidable. Propositions are represented by types, and proofs by programs, so the truth of a proposition comes down to the existence of a term of a particular type. There is no reason that type inhabitation (and therefore all propositions) needs to be decidable. So it is perfeclty possible to have a dependent type system where you give filter the type "for all satisfiable f" where f ranges over all computable functions of the appropriate type, even though this proposition is not decidable. -Dan On Feb07, Bulat Ziganshin wrote:
Hello Henning,
Thursday, February 7, 2008, 4:27:30 PM, you wrote:
ok, read this as "computer can ensure...", because it was exactly the original question - "can computer check that any given function in turing-complete language is non-trivial?"
My original question according to
http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html was "Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value?"
where Haskell is *turing-complete* *computer* language
this allows to answer to your question that you need to use special, non-turing language if you want to check arbitrary functions for non-trivialness. one example of such language:
data Func = ConstTrue | ConstFalse
and dependent-typed languages provides you (afaiu) much richer facilities to describe functions for which you still may prove something useful
so, if you term "function" includes the Func type, the answer is "yes", but if you mean usual haskell functions, the answer is no
[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
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.
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
Hi
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
or in Haskell: filterNonEmpty f x = assert (not $ null res) res where res = filter f x If you give that definition to the Catch tool (http://www-users.cs.york.ac.uk/~ndm/catch/) it will try and prove each call is safe. For certain examples, Catch will do the job very well - for example if your filter is something structural like isJust or null. Thanks Neil
On Thu, 7 Feb 2008, Neil Mitchell wrote:
Hi
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
or in Haskell:
filterNonEmpty f x = assert (not $ null res) res where res = filter f x
If you give that definition to the Catch tool (http://www-users.cs.york.ac.uk/~ndm/catch/) it will try and prove each call is safe. For certain examples, Catch will do the job very well - for example if your filter is something structural like isJust or null.
Indeed, if Catch or ESC or similar tools can handle such specifications it would be great. However I suspect that the translation you gave is different from what I wanted. I consider a function buggy, if it implements 'const' considerably more complicated than just saying 'const'. :-) That is, I only want to reject a function if it _always_ returns the empty list. Your 'filterNonEmpty' is rejected whenever _some_ arguments yield the empty list.
Hi
Indeed, if Catch or ESC or similar tools can handle such specifications it would be great. However I suspect that the translation you gave is different from what I wanted. I consider a function buggy, if it implements 'const' considerably more complicated than just saying 'const'. :-) That is, I only want to reject a function if it _always_ returns the empty list. Your 'filterNonEmpty' is rejected whenever _some_ arguments yield the empty list.
Yes, but someone redefined your problem as the above one, which I can solve :-) For your original problem, Catch is entirely unsuitable. ESC/Haskell would be my preferred method of solving this within Haskell, but I'm not sure if it has existentials or not. I could imagine writing something like: filter :: {f: exists x. f x == True} -> {True} -> {True} filter :: (a -> Bool) -> [a] -> [a] Thanks Neil
participants (7)
-
Bulat Ziganshin -
Dan Licata -
Henning Thielemann -
Jonathan Cast -
Matthew Pocock -
Neil Mitchell -
Wolfgang Jeltsch