[isabelle] map, difference, image, etc.


I recently improved my life quite a lot by assigning an infix operator symbol to the ‘map’ function. Expressions like “map (f x) (g y)” could become expressions like “f x ``` g y” -- much more readable without all those parentheses. As you can see, I chose (```) as my infix operator. 

But it got me thinking: why can’t I just use (`) instead? That is, the same symbol as is used for the image of a set. “Map” and “image” are pretty similar functions, after all:

map : (‘a => ‘b) => ‘a list => ‘b list
image: (‘a => ‘b) => ‘a set => ‘b set

There’s no problem with (+) being polymorphic over any sort of number, so why can’t (`) be polymorphic over any sort of “collection”? And while we’re at it, we could make the set-minus operator (-) polymorphic too, so that when X and Y are of type “list”, then “X-Y” is the list obtained by removing from X all elements in Y.

Would that work?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.