Finite maps (#279)

This commit introduces finite maps implemented as 2-3-trees, where the
balance invariant is enforced by types (using nested datatypes
approach). While this is not the best implementation in terms of
efficiency, its correctness is relatively easy to verify and maintain.
The implementation can be seen as a temporary solution, and as a
guideline for the interface of a better implementation that will be
provided in the future.

Author: ppolesiuk