Data.Map, Data.IntMap documentation

[apfelmus]

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
>> _can_ know about insert 
>> (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

  Philip Wadler. A prettier printer.
  http://homepages.inf.ed.ac.uk/wadler/topics/
   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 
introduction to Haskell

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

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