Chris Okasaki wrote:

> Unfortunately, it's not quite that easy.  For a library with several
> implementations
> of, say, sets, you want the various implementations to support the same
> fold function.  In other words, in a library with abstract data types, you
> want
> the folds to be over the abstract data type, not over their concrete
> representations.
> Of course, the fold over the abstract data type will often be implemented in
> terms of the fold over the concrete representation, but rarely will it be
> the same function.
> 
> For example, if you have an implementation of ordered sets represented as
> unbalanced binary search trees, then the abstract fold probably has a type
> something like
> 
>   abs_fold :: (a -> b -> b) -> b -> Set a -> b 
>
> whereas the concrete fold (which is the one that would be generated by your
> system)
> has a type something like
>
>  conc_fold :: (b -> a -> b -> b) -> b -> Set a  -> b
>
> One simple but inefficient implementation of abs_fold might be
>
>   abs_fold f c s = List.foldr f c (flatten s)
>     where flatten = conc_fold (\ xs a ys -> xs ++ a:ys) []


While the types you give for abs_fold and conc_fold are perfectly
sensible, the thing I am missing from the types is the fact that they
are related. I think the types should reflect that abs_fold is
'implemented_by' conc_fold and conc_fold 'implements' abs_fold.


How about generalising the type of abs_fold a bit?

  abs_fold :: (X a -> Set a) -> b -> (a -> b -> b) -> X a -> b

(X is existentially(?) quantified)

(*)  abs_fold abstr empty add set
       = case (abstr set) of
           Empty      -> empty
           Add x set' -> add x (abs_fold abstr empty add set')


instantiating X with Tree
(unbalanced trees: Tree a = Leaf | Branch a (Tree a) (Tree a))

  abstr = foldrTree Empty (\a l r -> Add a (join l r))
          where
            join :: Set a -> Set a -> Set a
            and implements union on sets in terms of Tree primitives


Then you can write your functions in terms of the abstract type

  sum_Set  = abs_fold abstr 0 (+)
  size_Set = abs_fold abstr 0 (\_ xs -> 1+xs)

I cannot see any problems with generating folds like (*). Or am I
missing something?

Laszlo

PS. I have been trying to generalise folds to be able to cope with
mutually recursive data types (this is easy) and simultaneous
induction over more than one type (I know Fegaras' work, but I want
one fold). Any thoughts on this would be welcome.


Reply via email to