Skip to content

Draft: Add law `map_fold_foldr` to `FinMap` interface.

Robbert Krebbers requested to merge robbert/map_fold_foldr into master

See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do

This rule expresses a form of "parametricity": it says that regardless of A, B, f, and b, the function map_fold f b m will always traverse the map m in the same order. Namely the order of converting the map into a list.

This law holds for all instances of FinMap we currently have, and I think without weird non-constructive axioms (that allow one to define non-parametric functions) it is impossible to define a FinMap instance that does not satisfy this law.

/cc @johannes @ivanbakel

Merge request reports