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