Skip to content

BatSeq: Fix specification of `filter` #545

Open
wants to merge 1 commit into from

3 participants

@nbraud
nbraud commented Mar 6, 2014

The previous specification for filter (and other functions) was nonsensical as it considered elements of a sequence that “occur” after an infinite number of other elements.

For instance, it could have lead one to understand that filter (fun x -> x == 0) should terminate on the sequence 1 1 1 1 ....

@nbraud nbraud BatSeq: Fix specification of `filter`
The previous specification for `filter` (and other functions) was nonsensical as it considered elements of a sequence that “occur” after an infinite number of other elements.

For instance, it could have lead one to understand that `filter (fun x -> x == 0)` should terminate on the sequence `1 1 1 1 ...`.
53682ba
@gasche
ocaml-batteries-team member
gasche commented Mar 6, 2014

I don't think your change is correct. Consdier:

let rec cycle a = fun () -> Cons (a, cycle a)
let _ = filter ((=) 0) (append (cycle 1) (cycle 0))
@c-cube c-cube commented on the diff Mar 6, 2014
src/batSeq.mli
@@ -218,12 +218,11 @@ val filter : ('a -> bool) -> 'a t -> 'a t
{b Note} filter is lazy in that it returns a lazy sequence, but
each element in the result is eagerly searched in the input
- sequence. Therefore, the access to a given element in the result
- will diverge if it is preceded, in the input sequence, by
- infinitely many false elements (elements on which the predicate
- [p] returns [false]).
+ sequence. Therefore, this will diverge on an infinite sequence
+ containing finitely many true elements (elements on which the predicate
@c-cube
ocaml-batteries-team member
c-cube added a note Mar 6, 2014

I think, to be more precise, that it should state that the function diverges at the first infinite subsequence without true element it met. For instance, on append (singleton 0) (cycle 1) (cycle 2) (singleton 0) (say), filter (= 0) diverges only after it returns the first element.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
@nbraud
nbraud commented Mar 6, 2014

Indeed, the new formulation isn't quite right either (though I meant what @c-cube said), but I wanted to avoid formulations like “the first infinite subsequence without true element”.

Part of the problem might be the specification of append/concat/flatten, which have the same problem (i.e. do not make explicit what the behavior is when dealing with infinite operands).

PS: find/find_map are also concerned.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.