Stream: Coq devs & plugin devs

Topic: fold_left on maps in CMap


view this post on Zulip Hugo Herbelin (Aug 23 2021 at 12:13):

I'm confused with the meaning to give to fold_left in cMap.mli. Its type is (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b while I would have expected, following the model of List.fold_left, that it is (key -> 'a -> 'b -> 'a) -> 'a -> 'b t -> 'a.

Two parameters are in play regarding fold on maps:

Then, shouldn't there be four variants? Or, if only the increasing/decreasing order is expected to matter, shouldn't it be called fold_up and fold_down instead, both following the List.fold_right pattern, that is (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b?


Last updated: Oct 21 2021 at 21:03 UTC