[m-dev.] Automatic generation of map, foldr, foldl

[Peter Schachte]

On Tue, Sep 22, 1998 at 01:48:39PM +0200, Lee Naish wrote:

> I was just saying that no set of HO predicates will be enough, thats why we
> want to allow programmers to write their own predicates.

I'm really curious:  what do you mean by "write their own predicates?"
This, it seems to me, is the key.

> Re iterators:
> This reminds me of Richard O'Keefe's work on sequences.

Do you have a reference for this?

> I think its a mistake to convert data types to instances of iterators then
> use a general predicate on iterators such as member.  It assumes that the
> compiler can do a good job of deforestation.

Using map assumes higher order code is efficient (call/N are still a
bit slow in Mercury, IMHO), or that the compiler specializes HO calls
(does the Mercury compiler do this yet?).

Anyway, it would be possible to implement iterators using specialized
language constructs that guarantee deforestation.  At this point I'm
just proposing an overall approach, not a specific implementation.

This is how I look at it:  map abstracts all predicates that relate
corresponding elements of two lists in some way; fold[lr] abstracts
predicates that traverse a list collecting something.  What you are
proposing to do is to extend these abstractions to aggregate data
structures other than lists.  The problem with this is that there is
no canonical set of such abstractions.  I'd like to go further,
abstracting as many of these sorts of predicates as possible in a
single quantification construct.

In logic, we can write (slipping into \LaTeX-ish syntax):

	\forall x \in l : p(x)

to specify that p(x) holds for all x in the list l.  suppose we define

	x_1 \in l_1 \as ... \as x_n \in l_n

to mean that x_1,...,x_n are corresponding elements of l1,...,l_n.
Then map is just

	\forall x \in l \as y \in m : p(x,y)

That's not so exciting, but we don't have to limit ourselves to only
lists.  We could use the same syntax for mapping over other data
structures.

The interesting bit, though, comes when we iterate over different
types of data structures at the same time.  For example, we could
define

	x \in \inorder(tree)

to mean that x is in tree and that the tree is to be traversed
inorder.  Then

	\forall x \in \inorder(tree) as y \in l : x = y

(where l is of type list) specifies that l is a flattened version of
tree.  If we let

	x \in 1..n

mean that x is between 1 and n inclusive, iterated in that order, then

	\forall x \in l \as i \in 1..n : x = i

means that l is a list of the first n integers, and
	
	\forall x \in l \as i \in 1..n : true

means that the length of l is n (defining the base cases suitably).

This overall scheme handles quite a variety of different sorts of
higher-order constructions in, IMHO, a fairly natural declarative
framework.  What it doesn't handle is accumulation.  I don't (yet)
have a way to incorporate this, but I'll think of something.

> Its better to generalise
> member to data types in a similar way to how map, foldl and foldr can be
> generalised.

I think it's better to generalize member to existential
quantification:

	\exists x \in l : ...


> Of course the functional people have not generalised member because they
> don't have nondeterminism.

I don't think we should assume that the functional people will hit on
the right sorts of HO abstractions for logic programming.  For
example, a functional programmer would insist on thinking of mapping
as applying a function to each element of a data structure and
collecting the result, while a logic programmer would want to think of
it as expressing a relationship between corresponding elements of two
data structures.  When generalized to more than two data structures,
this is a considerably more general view.


> They have not even discussed converting and
> data structure into a list (which is rather like an iterator, especially
> with lazy evaluation), though this can be done quite easily with foldr, nil
> and append.

This approach won't work, because you can't (easily) convert the
resulting list into a data structure of the correct shape.  You can
get away with a lot on lists that you can't on non-flat data
structures.

> One advantages of HO
> programming is deforestation can be done by transforming the HO code.  This
> requires that the compiler knows the right "laws", eg (map f).(map g) =
> map (f.g).

I think

	(\forall x \in l \as y \in m : g(x, y)) \wedge
	(\forall x \in m \as y \in n : f(x, y))

is quite easily combined into

	(\forall x \in l \as y \in m \as z \in n: g(x, y), f(y, z)

(though it's clearly nowhere near as concise!)

> With hand coded iterators its going to be harder for the
> compiler to know what laws can be applied

With hand coded iterators it's mostly a matter of (a) exploding a
single compound data structure passed as an argument in a specialized
recursive predicate into several separate arguments, and sometimes (b)
recognizing that one of these (compound term) arguments should be
allocated on the call stack rather than the heap because it will not
survive the call.

> whereas if the compiler
> automatically generates certain predicates from the type definitions it
> should also be able to determine what laws apply.

The same argument applies to compiler-generated iterators.

-- 
Peter Schachte                | I love deadlines. I like the whooshing sound
mailto:pets at cs.mu.OZ.AU       | they make as they fly by.
http://www.cs.mu.oz.au/~pets/ |     -- Douglas Adams 
PGP: finger pets at 128.250.37.3 |