map: x->y->[x]->[y]

I'd like to have ({x} is for a set of x)

map: x->y->{x}->{x}

defined elegantly without introducing {arbitrary-element|the-rest} and,
if possible, without resorting to monads.

Another idea would be to wrap the arbitrary linearization of a set in a
type that explicitly disallows any iteration primitives except for map
(map in the FP sense), and of course allows getting to the set back.
This would IMHO come close to what I'm after. I'm not an expert in
Haskell, is it possible?

But I guess we are back with a monad then, right?

rMap :: (x -> y) -> [x] -> [y]
rMap f = map f . reverse

You do have type correctness.  Now, would you like to call rMap a map?

RobertSzefler napisal(a):

It seems that the problem is indeed severe, quoting the above:

"It is striking that the categorical framework has been applied only
sporadically to data types that are not just given by free term
structures, such as abstract data types. Although the catamorphism
approach principally works also for sub-algebras that satisfy certain
laws, one cannot map into algebras with less structure [9, 10]. This
innocent looking restriction means a rather severe limitation of
expressiveness: for instance, such a simple task as counting the
elements of a set cannot be expressed by a catamorphism"

For example, a map over a binary tree:

# type 'a tree = Empty | Node of 'a tree * 'a * 'a tree;;
type 'a tree = Empty | Node of 'a tree * 'a * 'a tree

# let rec map f = function
      Empty -> Empty
    | Node(l, x, r) -> Node(map f l, f x, map f r);;
val map : ('a -> 'b) -> 'a tree -> 'b tree = <fun>

# map (fun x -> x+1) (Node(Node(Empty, 1, Empty),
                           2,
                           Node(Empty, 3, Empty)));;
- : int tree = Node (Node (Empty, 2, Empty),
                     3,
                     Node (Empty, 4, Empty))

  nil : set
  add : t * set -> set

There are no equations between the lists you build up using nil and
add, aside from reflexivity.  A finite set is also generated by these
two function symbols, but it satisfies the two additional equations

  forall x, y, rest. add x (add y rest) == (add y (add x rest))

and

  forall x, rest. add x (add x rest) == add x rest

The first equation says that changing the order of insertion doesn't
change the value, and the second says that adding the same element
multiple times won't change the value. (The second equation is why
sets require equality.)

Assuming that you have a function

  choose : set -> (t * set) option

which satisfies the equations

  choose nil == None

and

  forall x, rest. there exist x', rest'.
    (add x rest) == (add x' rest') and
    (x' not in rest') and
    choose (add x rest) == Some(x', rest')

then you can define a perfectly good map function in the obvious way:

  fun map f list =
    case choose list of
      None => nil
    | Some(x', rest') => add x' (map f rest')

Now, you can show the correctness of map with a simple inductive
argument based on the number of distinct elements of a finite
set. There are other ways of specifying sets algebraically, but this
works fine -- you can define map, union, and so on, and relatively
easily prove that they have the desired properties.

If I understand you correctly, the reason you're worried arises from
something like the following implementation:

  structure IntSet =
  struct
    type set = int list

    val nil = []

    val add (x, set) = x :: set

    fun choose [] = NONE
      | choose (x :: tail) = SOME(x, filter (fn x' => x <> x') tail)
  end

You are worried that if you have

val s = add(1, add(2, nil))
val r = add(2, add(1, nil))

then s and r represent the same set {1,2}, but that calls to s and
r can give different results:

  choose(s) evaluates to SOME(1, {2})

and

  choose(r) evaluates to SOME(2, {1})

This superficially looks like it breaks the equational reasoning
property. However, this isn't actually so, because of the way that we
specified choose:

  forall x, rest. there exist x', rest'.
    (add x rest) == (add x' rest') and
    (x' not in rest') and
    choose (add x rest) == Some(x', rest')

Here, we very carefully DON'T say that

  choose (add x rest) == Some(x, rest)

Instead, we use an existential quantifier to say that choose returns
some distinct element of the set, not necessarily the "most recently
inserted" one. Indeed, upon reflection it should be clear that because
of the property that the order of insertion doesn't matter, we /can't/
promise any such behavior.

 From what I gather, it all boils down to maps and (especially) folds
working over things in the Cpo category, ie, as Neelakantan Krishnaswami
pointed out, free algebras (is it?). What if we abandon that formalism
and try to work in a different setting, a'la Bird-Meertens, but
dismissing the notion of order in recursion? What would the underlying
category be then? (I'm just starting to learn this, sorry for my
ignorance) I guess the objects would still be sets (?) and arrows would
have to be chosen to reflect the lack of meaningful order... Is it the
case that for example the Third Manifesto can be formalized in such
generic terms?

Next we'd have a problem of recursively (or meta-recursively as a
recursion over a set isn't really a recursion) processing mixed
structure things, like lists of sets of lists. Here's where my mind
starts to crash and burn ;)

Does anyone know about any work in these directions?

Because "set of T" is not an initial algebra (or sufficiently close to
it for catamorphisms to make sense), you cannot treat it as if it is
one.

However, "set" or "finite set" is still a (covariant) _functor_, and I
would say that the action of a functor on a morphism (i.e., the
function you want to map over the structure) is the most natural and
general way do define what we mean when we say "map f over som data
structure": We view the data structure as a functor in some
appropriate way, and then lift f trough this functor.

Yes, almost nothing happens here, which suggests that "map" should in
general be tought of as a _primitive_, rather than something you
necessarily want to construct out of smaller bits.

The decomposition of the map operation as a catamorphism is nice and
interesting when it works, but it is not the end of the world when it
doesn't.

Perhaps you want to be able to treat sets as some sort of inductive
datatypes?  If that is the case, then you might want to take a look at
Martin Ervig's papers on FGL:

  http://web.engr.oregonstate.edu/~erwig/fgl/

IOW, I think that it would probably be possible to specify a "match"
operation on sets (and hopefully implement it reasonable efficiently)
that would allow you to treat sets inductively in a "functional style"
(map, fold, etc... would then fall out naturally).  The idea seems so
simple to me that I would not be surprised to hear about prior art.
(If you know of relevant papers, please post details.)

-- setFunctions.hs
-- author Gene A.
-- date last revised: 2005.12.19
-- version 0.1

-- ====================================

-- uniq
-- uniq filters out any non unique items from a list

uniq :: Eq a => [a] -> [a]
uniq []      = []
uniq (x:[])  = [x]
uniq (x:xs)  =  x : uniq (filter ((/=) x) xs)

-- ====================================

-- setFromList
-- converts a list that may have non unique members to a list with unique
members therefore
-- a set structured as a list, but a set never the less

setFromList :: Eq a => [a] -> [a]
setFromList a  = uniq a
-- ====================================

-- setmap
-- this function will take a set as a list and map a function over it and
return a
-- set structured as a list.... well actually it will do that but will
also take a list that is
-- not a set map the function over it and then by eliminating redundant
members turn it into a
-- yup ...umhum a set structured as a list..

setmap :: Eq b => (a -> b) -> [a] -> [b]
setmap f s = uniq $ map f s

-- ====================================

-- setFoldr
-- This function first ensures that a list is a set and then  applies the
-- (foldr f) to it giving it a correct result.

Loading package base-1.0 ... linking ... done.
Compiling Main             ( setFunctions.hs, interpreted )
Ok, modules loaded: Main.
*Main>
*Main>
*Main> :b Main
setFoldr :: Eq a => (a -> b -> b) -> b -> [a] -> b
setFromList :: Eq a => [a] -> [a]
setmap :: Eq b => (a -> b) -> [a] -> [b]
uniq :: Eq a => [a] -> [a]

*Main> setFromList "this is a test to see if it works on chars"
"this aeofwrknc"

*Main> setFromList $ words $ "this is a test to see if the function works
in a test setting on words"
["this","is","a","test","to","see","if","the","function","works","in","sett ing","on","words"]

*Main> setFromList $ words $ "black blue yellow blue black red crimson
yellow"
["black","blue","yellow","red","crimson"]

*Main> setFoldr (++) " " $ setFromList $ words $ "black blue yellow blue
black red crimson yellow"
"blackblueyellowredcrimson "

*Main> setmap (\x -> x + 3) [2,7,3,1,5]
[5,10,6,4,8]

*Main> setmap (\x -> x * 3) [2,7,3,1,5,2,5,3]
[6,21,9,3,15]

*Main> setmap (\x -> 0) [2,7,3,1,5]
[0]

*Main> setmap (\x -> 5) [2,7,3,1,5]
[5]

*Main> setmap (\(x,y)  -> ((x + 3),(y * 2))) [(2,4),(4,4),(3,1)]
[(5,8),(7,8),(6,2)]

*Main> setmap (\(x,y)  -> ((x + 3),(y * 2))) [(2,4),(4,4),(3,1),(4,4)]
[(5,8),(7,8),(6,2)]

*Main> setmap  (\(a,b,c) -> ((a ++ " programmer"),(b * 4),(c * 5)))
[("gene",10,5),("Robert",12,5)]
[("gene programmer",40,25),("Robert programmer",48,25)]