SIGNATURE BagFold[data, <]

-- folding of bags

-- Parameter
SORT data
FUN < : data ** data -> bool
        -- total strict-order; in 
        --   ~(x < y) AND ~(y < x) => x = y
        -- should = represent semantic equality

IMPORT  Bag[data, <] ONLY bag

FUN / : (data ** data -> data) ** bag -> data
--    + / b
    -- fold bag by +
    -- function f should be left-commutative:  x o (y o z) = y o (x o z)
    -- since reduction order is implementation dependent and should 
    -- not be relevant!
    -- informally
    -- + / {{a,a,b,...,y,z}} == a o (a o (b o (...(y o z)...)))
    -- undefined for empty bags