maps and set

[jmchapman]

Add support for maps and sets

[HeinrichApfelmus]

I have some code that I can contribute:

https://github.com/HeinrichApfelmus/agda-notes/blob/1a6519bb3002aaad07d5eeac0380eacdb4777e63/lib/containers/agda/Haskell/Data/Set.agda

I figured that module names Haskell.Data.Map and Haskell.Data.Set are appropriate.

[HeinrichApfelmus]

I'm wondering how to deal with the Setoid question. 🤔

The issue is this:

Consider two x y : ℙ a that are equal x == y ≡ True. In general, it does not follow that x ≡ y. For example, if we were to provide an implementation in terms of binary search trees as part of agda2hs, then postulating x ≡ y would actually make the theory inconsistent because the trees can be distinguished internally.

Unfortunately, distinguishing x and y has ripple effects on structures built on top of Data.Set, e.g. the monoid Set.union will not be a lawful Monoid instance — because "lawful" is defined in terms of ≡ at the moment.

In general, it would be desirable to be able to substitute x for y in any context, which is equivalent to x ≡ y. In Haskell, this is "solved" through abstraction: All exported functions of Data.Set — except for a few debugging functions — preserve the equivalence relation, and we can pretend that x ≡ y as long as we only use functions from the public interface.

The alternative is Setoids — which implies that all "lawful" class instances will have to be redefined in terms of an equivalence relation, e.g. mempty <> x ≈ x instead of mempty <> x ≡ x.

[HeinrichApfelmus]

My postulate-based axiomatization of Data.Map is now public:

https://github.com/cardano-foundation/cardano-wallet-agda/blob/2293efc8138d473f2f7240e567ed362967b13b98/lib/customer-deposit-wallet-pure/agda/Haskell/Data/Map.agda

This is an axiomatization in the sense a finite map m is completely determined by:

• The extensional behavior of the lookup function.
• The fact that the lookup function is Just on only finitely many elements of its domain.

I'm not yet fully happy with it, though:

• Prefixing all properties with prop- is cumbersome. I think that a separate module Haskell.Law.Data.Map or Haskell.Data.Map.Law is more appropriate.

• On the setoid question, I now believe that the best way to proceed is to add an axiomatization of quotient types. Then, we have two types: Data.Map the implementation in terms of binary trees, and Data.Map the quotient type uniquely determined by lookup. (The fact about lookup probably makes this an instance of a definable quotient type, with the twist that extensional equality on A → Maybe B is also a quotient of sorts.)