Library proposal: add a Location interface for element-wise operations on Data.Map (#4887)

Ross Paterson ross at soi.city.ac.uk
Sat Jan 8 01:41:20 CET 2011


On Fri, Jan 07, 2011 at 10:10:51PM +0100, Henning Thielemann wrote:
> Location is really a hole, where a certain element is already removed?

Either a value has been removed, or a key not present has been added,
but yes, it's a hole.

> Then I find Location as name a bit misleading. I assumed, that a
> location also lets me peek the particular element. If the meaning
> remains, how about the name Hole?

It's certainly mnemonic.



More information about the Libraries mailing list