coq
Ltac2 library: list and array fold functions don't match OCaml
I just found that I well and thoroughly messed up the parameter order of the list and array fold functions back then. I took the OCaml headers as blue print but still somehow I managed to get this quite wrong:
OCaml: val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
Ltac: List.fold_left : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a
2nd and 3rd parameter of fold_left swapped
OCaml: val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
Ltac2: List.fold_right : ('b -> 'a -> 'a) -> 'a -> 'b list -> 'a
2nd and 3rd parameter of fold_left swapped (plus names of 'a and 'b)
Ocaml: val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
Ltac2: Array.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
OK
Ocaml: val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a
Ltac2: Array.fold_right : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
2nd and 3rd parameter of fold_right swapped plus parameters of f
@ppedrot @JasonGross @Janno : any idea how this can be fixed? I would suggest that I adjust it to OCaml (although I don't like it that the fold_right functions take the initial value as last argument - bad for partial applications) and do PRs for all projects in CI. Since we don't have deprecations warnings in Ltac2, I don't think it makes a lot of sense to do it in two steps.
I personally am entirely used to these arguments appearing in pretty much random orders and I have mostly given up trying to remember which language does it which way around. Others in my team have introduced foldr and foldl wrappers that homogenize the order of arguments across the two directions. I am starting to use the wrappers because even though I do still need to look up the order once it saves me from having to change the order when I switch from a left fold to right fold and vice versa.
I suspect people used to the OCaml way of things will want to keep the odd inconsistency between left and right folds. I myself would much rather have a completely uniform interface.
One reason for making it close to OCaml was the (yet to be proven) idea that this makes it easier to port tactics from Ltac2 to OCaml. Of course this involves much larger construction sites, but still it is quite annoying to fix such things in nested constructions of the algorithmic part of a tactic.
I am personally in favor of having the accumulator argument first, so that one can supply it by partial application.
Anyway, the Ltac2 list and array functions should have the same interface.
This is maybe slightly off-topic but the only converting between Ltac2 and OCaml I've done so far was to move performance-critical Ltac2 code to OCaml. My experience has been that the code needs to be rewritten entirely anyway. With a reasonable IDE (and these days even emacs + dune qualifies) the order of arguments in folds is so far down on the list of annoying problems when writing Coq plugins in OCaml that I would disregard it entirely as far as justifying the order of arguments in Ltac2 folds is concerned.
No, this is not off topic - this is exactly the question we are discussing here. I think this depends a bit on how the ratio between the algorithmic part and interfacing with the guts of Coq is and how well this is modularized. In my tactics I have large parts which work on reified data structures which are pure Ltac2/Ocaml (no constr or the like). I would guess in ltac2 the algorithmic part is 80% of the code size. From the 20% I can usually manage to leave a large part in Ltac2, but the rest indeed increases quite a bit.
But besides the OCaml compatibility - there is also the point that the list and array fold have different arguments for "f" which makes it difficult to make fold functions which go over mixed/nested list/array data structure.
Ltac2 is still called "experimental" in the doc which IMO means we are less strict with backwards compat.
Not sure if this matter:
Using ocaml argument order,
fold_left (&) acc [x1;...;xn] is acc & x1 & ... & xn (assuming the correct associativity for (&))
fold_right (&) [x1;...;xn] acc is x1 & ... & xn & acc (assuming the opposite associativity)
Ltac2 array fold_right (&) acc [x1;...;xn] is acc & xn & ... & x1 (with the fold_left associativity)
This came up in https://github.com/coq/coq/pull/18095 which adds List.fold_lefti with API matching OCaml (and therefore not matching Ltac2 List.fold_left)
I am still open to change it - I guess Ltac2 is not yet that widely used that the effort should still be feasible.
Please vote on this comment with thumbs up if you want the change (Ocaml compatible) or thumbs down if we should keep it as is (my messed up version).
