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
>> _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
More information about the Libraries
mailing list