# Data.Map, Data.IntMap documentation

apfelmus apfelmus at quantentunnel.de
Sat Aug 18 08:22:54 EDT 2007

```Andriy Palamarchuk wrote:
> apfelmus wrote:
>
>> I prefer to know the laws that hold. In
>> other words, I want an infinite amount of examples
>> at once.  For instance, the laws
>>
>> lookup k' (insert k x m) = Just x    if  k ==> k'
>> lookup k' (insert k x m) = lookup k' m   if  k /=>
> k'
>> uniquely define insert, they are everything you
>> (from the denotational point of view). And they are
>> even shorter than
>> concrete examples (= their special cases).
> ....
>
> Such formulas can definitely be part of the
> description.
> I'm relatively new to Haskell. While I trust that the
> way you described it are accurate, it takes much more
> effort to understand it (especially the parts with
> "homomorphisms", "mplus", etc) than to understand what
> function does. This is probably not because these
> topics are complex, but because I don't know
> terminology, not yet fluent with the concepts.
> Concrete examples are more useful for a person with
> "practical programming" background learning Haskell
> libraries, who just wants to start using them.
> [...]

> I want to collect feedback on your suggestion. Do you
> guys prefer this format:
>
>  let m = fromList [(5,'a'), (3,'b')]
>  insert 5 'x' m == fromList [(5,'x'), (3,'b')]
>  insert 10 'x' m == fromList [(5,'a'), (3,'b'),
> (10,'x')]
>  insert 5 'x' empty == fromList [(5,'x')]
>
> over this:
>
>  let m = fromList [(5,'a'), (3,'b')]
>  insert 5 'x' m
>    {3:='b',5:='x'}
>  insert 10 'x' m
>    {3:='b',5:='a',10:='x'}
>  insert 5 'x' empty
>    {5:='x'}
>
> apfelmus, the first form is what you want?

Yes. Perhaps aligning the equality signs. And there's the question
whether to use == or = to express equality. Strictly speaking, the
latter would be wrong since the binary tree may be balanced differently
(which bite us in functions like  showTree ) but the former is not
capable of expressing properties like

fromList [(undefined, 'a')] = undefined

that convey information about strictness. Personally, I think I'd use =
since it feels "more equal" :)

The ultra-correct way would be to only use  toAscList  to observe
equality, i.e. to state

toAscList (insert 5 'x' m) = [(3,'b'), (5,'x')]

but not

insert 5 'x' m = fromList [(3,'b'), (5,'x')]

since we are not guaranteed that the latter trees on each side of the
equation are balanced the same way. This is related to the question

"now, but what _is_ a finite map from keys to values?"

that I tried to hint at in my previous post. Your examples are based -
whether intentionally or not - on the answer

"such a map _is_ a list of (key,value) pairs."

In other words, to explain what an operation like  insert  does with
Map k a  , you explain it in terms of the two functions  fromList  and
toAscList. Here's a reformulation of your example:

toAscList (insert 5 'x' (fromList [(3,'b'), (5,'a')]))
= [(3,'b'), (5,'x')]

We can go further and say that this is

= insertList 5 'x' [(3,'b'), (5,'a')]

where

insertList k x []          = [(k,x)]
insertList k x ((k',y):ms) =
if k == k' then (k,x):ms else (k',y):insertList k x ms

In other words, the description of  insert  is based on knowing how to
insert a key-value pair into a list of key-value pairs. Removing the
concrete example list, we get

toAscList . insert 5 'x' . fromList = insertList 5 'x'

or

toAscList . insert k x = insertList k x . toAscList

for all keys k and values x.

> (especially the parts with "homomorphisms", "mplus", etc)

(Due to the equation above, mathematicians would call  toAscList  a
"homomorphism", but you can safely ignore that word. In the last post, I
tried to show that  lookup  can take the role of  toAscList  , so that a
finite map may also seen as being a function  k -> Maybe a  instead of
being a list  [(k,a)] . The  mplus  would be an equivalent of  unionList
with a strange name.)

>> I prefer to know the laws that hold.
> Such formulas can definitely be part of the description.

The discussion with  lists of key-value pairs  and  insert  may seem
like nitpicking since to insert a key-value pair into a list, we humans
can "look at it" and "just do it". Of course, we can only do so with a
concrete examples. So, your examples are indeed best to show how the
function "just does it".

With examples only, we can't "do it in general" though. "Doing it in
general" also means to be able to formally _prove_ that a program you
write is correct. Only equational laws like

toAscList . insert k x = insertList k x . toAscList

or

lookup k' (insert k x m) = Just x       if  k == k'
lookup k' (insert k x m) = lookup k' m  if  k /= k'

allow you to do that. With some training and an intuition about what the
functions are supposed to do, succinctly formulated laws like that are
almost easier to read than examples.

In fact, it's a good idea to think up specifying laws before starting to
code since in purely functional languages, you can systematically obtain
and implementation from the laws. The classic paper on deriving
implementations from their specification is

Paul Hudak. The Design of a Pretty-printing Library.
http://citeseer.ist.psu.edu/hughes95design.html

with a follow-up

language-design.html#prettier

The man who derives all his programs from specification is Richard
Bird. You may want to have a look at his recent sudoku solver

Richard Bird. A program to solve Sudoku
Slides: http://icfp06.cs.uchicago.edu/bird-talk.pdf

where he starts with an apparently correct but hopelessly slow
specification and transforms it into a blazingly fast one. His

Richard Bird.
Introduction to Functional Programming using Haskel (2nd edition).
http://www.amazon.com/

emphasizes this style, too.

> Can you suggest any other improvements?

Maybe some examples are a bit arbitrary, for instance for the  ..WithKey
functions. I mean functionality like

\k a -> Just ((show k) ++ ":" ++ a)

probably won't show up in a real program. I wonder whether there are
examples that are useful on their own.

Regards,
apfelmus

```