Deforestation / "transducers" for values and lists

[countvajhula]

Design Parameters

In general for compiler optimizations, we can assume that flows are free of side-effects(!). For cases where there are side effects, it will probably make sense to introduce a new do form which will not do any optimizations. E.g. (do (~> some side effecting functions)).

Goals

Conjecture: Any sequential composition of functions (i.e. via ~>) operating on either:

• a certain number of input values, or
• input values contained in a list

... can be expressed in such a way that computing the result involves at most one pass over the input values.

I'm using the word "conjecture" here not to imply that this is an unknown theoretical result to be established but, rather, to represent my ignorance as to whether this result is true or not 😆

Some rough justification for the likelihood of the above is the "universality of fold" with respect to with map- and filter-like operations. So the problem seems to reduce (so to speak) to, "is any composition of functions that fold over the input list expressible as a single function that folds over the list?"

Map, Filter and Fold on Lists

It may be that we should narrow the scope of the optimization specifically to map, filter, and fold operations, rather than any functions composed via ~>. Towards this end, it may be useful to first determine the pairwise composition:

(~> (fold f init-a) (fold g init-b)) → (fold h init-c)

... where we'd need to define h in terms of f and g and init-c in terms of init-a and init-b (where f, g and h are the binary functions used in folding, and init-a, init-b and init-c are the seed values used).

Since we already have ways to transform map to fold and also filter to fold in general (by virtue of "universality"), that should mean that we can transform any sequence of map, filter, and fold operations into a sequence of fold operations alone, and then with the above pairwise composition available, we would be able to express that as a single fold operation by iterating the pairwise composition (folding over the folds!).

Extending to Pure Values

Presumably, it will be easier to focus on lists at first to understand the general approach while using a standard data structure. Then, the approach could be easily(?) extended to work with pure values not contained in any collection (i.e. pipelines like (~> (>< f) (pass g))).

Implementation

Iterating the Pairwise Fold Composition

Assuming we can define the pairwise composition of folds mentioned above, then iterating this (by folding) on the input syntax could be one way to achieve deforestation.

As a State Machine

The docs for Rebellion re: "transducers" describe how they can be thought of as a state machine (an intuitive way to look at it!). This could be another implementation strategy.

Resources

Is there anything in academic literature or in other programming languages that could be applicable here? Here are some resources that may be relevant:

Positive Supercompilation for a Higher-Order Call-By-Value Language (from @soegaard) Clojure's Transducers Common Lisp's Series

[benknoble]

"is any composition of functions that fold over the input list expressible as a single function that folds over the list?" (~> (fold f init-a) (fold g init-b)) → (fold h init-c)

I conjecture that this is possible iff (fold f init-a) applied to a list produces a list. Otherwise the application of (fold g init-b) will go wrong.

Given that (~> (fold f init-a) (fold g init-b)) would be (roughly¹) in the original source, perhaps it is acceptable to assume that (fold f init-a) produces a list.

I should have some spare time today to work up a short Coq proof or two of some parts of your post; in particular, I think I can prove the special cases

• (~>> (F f) (F g)) = (F (flow (~> f g)) _) where F is map or filter
• (~>> (F f) (G g)) = (H (J f g)) where (F,G) ∈ {filter,map}2 | F =/= G, H is a folding operation, and J computes some combination of f and g for the fold (variables because I don't yet know the exact form).

I'll try to work on the double-fold case above, but no promises :)

---

1. Roughly because either fold-based expression might originally have been a filter or map.

[benknoble]

Note that if an assumption is made about (fold f init-a) resulting in a list, the error message given at run-time when it does not may be phrased in terms of (fold h init-c) and thus be quite confusing.

[benknoble]

I'll post the proofs here; I'm working on the double-fold case some, too, but am doing some related readings and haven't quite gotten in to the weeds of that case yet.

I did prove all the cases I said I would, though with slight tweaks for the first map and filter cases, and with the addition of several other (known) properties. Most of this is not, I think, new; it is useful for me to write and have machine-checked proofs, though.

Critical proofs (in the single-in-single-out case):

• (~>> (map f) (map g)) = (map (~> f g) _)
• (~>> (filter p) (filter q)) = (filter (conjoin p q) _) (see conjoin in the proof below, which I think corresponds to (lambda (p q) (flow (and p q))) or to Racket's conjoin)
• (~>> (map f) (filter pi)) = (foldr (MF f pi) null _) where (MF f pi) = (~> f (make_fold_pred pi)), (make_fold_pred pi) = (flow (if (~> 1> pi) cons 2>))
• (~>> (filter psi) (map g)) = (foldr (FM psi g) null _) where (FM psi g) = (flow (if (~> 1 psi) (~> (== g _) cons) 2>))

I used the notation f;g for (compose1 g f), also given as g ∘ f. The semicolon notation is standard for math and (here) is analogous to (flow (~> f g))

Require Import Utf8.
Require Import Program.
Require Import List.

(* fold_right : ∀ [A B : Type], (B → A → A) → A → list B → A *)
(* fold_left : ∀ [A B : Type], (A → B → A) → list B → A → A *)
(* map : ∀ [A B : Type], (A → B) → list A → list B *)
(* filter : ∀ [A : Type], (A → bool) → list A → list A *)

Lemma fold_universal {α β} (g: list α → β) (v: β) (f: α → β → β):
  g nil = v ∧ (∀ x xs, g (x::xs) = f x (g xs))
  ↔
  g = fold_right f v.
Proof.
  split.
  - intros [Gnil Gcons].
    apply functional_extensionality; intros xs.
    induction xs as [| x xs IHxs]; auto.
    now rewrite Gcons, IHxs.
  - now intro Gfold; subst.
Qed.

(* fold_universal : *)
(* ∀ {α β : Type} (G : list α → β) (v : β) (F : α → β → β), *)
(*   G nil = v ∧ (∀ (x : α) (xs : list α), G (x :: xs) = F x (G xs)) *)
(*   ↔ G = fold_right F v *)

Section map_filter_fold.
  Context {A B: Type}.
  Notation "f ; g"  := (compose g f) (at level 70).

  Definition make_fold_map (f: A → B) := f; cons.

  Lemma map_is_fold (f: A → B):
    map f = fold_right (make_fold_map f) nil.
  Proof.
    unfold make_fold_map.
    now apply fold_universal.
  Qed.

  Definition make_fold_pred (p: A → bool) :=
    (λ x acc, if p x then x::acc else acc).

  Lemma filter_is_fold (p: A → bool):
    filter p = fold_right (make_fold_pred p) nil.
  Proof.
    unfold make_fold_pred.
    now apply fold_universal.
  Qed.
End map_filter_fold.

(* map_is_fold : *)
(* ∀ {A B : Type} (f : A → B), map f = fold_right (make_fold_map f) nil *)
(* filter_is_fold : *)
(* ∀ {A : Type} (p : A → bool), filter p = fold_right (make_fold_pred p) nil *)

Section deforestation_map_filter.
  (* Caveat: the following proofs are all for functions of a single input and
   * output. Generalizing them over arities remains an exercise; clearly
   * when input and output arities align, one can curry or uncurry functions as
   * needed to fit these theorems (simply subsitute the tuple type (X x Y x Z …)
   * for types A, B, C, etc.). When arities do not align, we must decide a
   * behavior. My preference is to error, so that we can ignore those cases
   * entirely. *)

  Notation "f ; g"  := (compose g f) (at level 70).
  Context {A B C: Type}.
  Implicit Type f: A → B.
  Implicit Type g: B → C.
  Implicit Types p q: A → bool.
  Implicit Types π ψ: B → bool.

  Lemma compose_map_map_is_map f g:
     map f; map g = map (f; g).
  Proof.
    transitivity (fold_right (make_fold_map (f;g)) nil).
    - now apply fold_universal.
    - apply map_is_fold.
  Qed.

  Definition conjoin (p q: A → bool): A → bool :=
    λ x, andb (p x) (q x).

  Lemma compose_filter_filter_is_filter p q:
    filter p; filter q = filter (conjoin p q).
  Proof.
    transitivity (fold_right (make_fold_pred (conjoin p q)) nil).
    - apply fold_universal. split; try easy.
      unfold conjoin, make_fold_pred; cbn.
      intro x.
      now destruct (p x); cbn; destruct (q x).
    - apply filter_is_fold.
  Qed.

  (* the "J" operator in my GitHub comment for the map;filter case *)
  Definition make_fold_map_pred f π :=
    f; make_fold_pred π.

  Lemma compose_filter_map_is_fold f π:
    map f; filter π = fold_right (make_fold_map_pred f π) nil.
  Proof.
    now apply fold_universal.
  Qed.

  (* "J" operator for filter;map *)
  Definition make_fold_pred_map ψ g :=
    λ x acc, if ψ x then g x::acc else acc.

  Lemma compose_map_filter_is_fold ψ g:
    (filter ψ); (map g) = fold_right (make_fold_pred_map ψ g) nil.
  Proof.
    apply fold_universal; split; try easy.
    unfold conjoin, make_fold_pred_map; cbn.
    intro x.
    now destruct (ψ x).
  Qed.

End deforestation_map_filter.

(* compose_map_map_is_map : *)
(* ∀ {A B C : Type} (f : A → B) (g : B → C), map g ∘ map f = map (g ∘ f) *)

(* compose_filter_filter_is_filter : *)
(* ∀ {A : Type} (p q : A → bool), filter q ∘ filter p = filter (conjoin p q) *)

(* compose_filter_map_is_fold : *)
(* ∀ {A B : Type} (f : A → B) (π : B → bool), *)
(*   filter π ∘ map f = fold_right (make_fold_map_pred f π) nil *)

(* compose_map_filter_is_fold : *)
(* ∀ {B C : Type} (ψ : B → bool) (g : B → C), *)
(*   map g ∘ filter ψ = fold_right (make_fold_pred_map ψ g) nil *)

[countvajhula]

Given that (~> (fold f init-a) (fold g init-b)) would be (roughly1) in the original source, perhaps it is acceptable to assume that (fold f init-a) produces a list.

That's a good point, and agreed.

I should have some spare time today to work up a short Coq proof or two of some parts of your post in particular, I think I can prove the special cases (~>> (F f) (F g)) = (F (flow (~> f g)) _) where F is map or filter

Built-in map must preserve the size of the list, so I'm assuming the F on the RHS is something like filter-map?

(~>> (F f) (G g)) = (H (J f g)) where (F,G) ∈ {filter,map}2 | F =/= G, H is a folding operation, and J computes some combination of f and g for the fold (variables because I don't yet know the exact form). I'll try to work on the double-fold case above, but no promises :)

That would be amazing! My feeling is that it would be simpler to attempt a proof of the double-fold case than the {filter,map}² case since the latter has more combinations to consider, but I've never used Coq so I don't really know what's possible / practical.

[countvajhula]

Note that if an assumption is made about (fold f init-a) resulting in a list, the error message given at run-time when it does not may be phrased in terms of (fold h init-c) and thus be quite confusing.

As deforestation is a standard technique, I wonder if there are ways that people have already figured out to provide useful error messages. We might be able to attach syntax properties containing the original source expressions and then write the expansions in such a way that they check for list? at appropriate times and blame the right source expression. But that'd probably be easier to figure out down the line when we know exactly how the expansions work.

[countvajhula]

Ah whoops looks like our messages crossed. Having proofs is indeed valuable, thanks for furnishing them!

[benknoble]

That would be amazing! My feeling is that it would be simpler to attempt a proof of the double-fold case than the {filter,map}² case since the latter has more combinations to consider, but I've never used Coq so I don't really know what's possible / practical.

You're correct that the cross-product case is implied by the double-fold case once you show that map and filter are both folds (easy), but I haven't proved the double-fold case yet and knew I could do the cross-product cases :)

As deforestation is a standard technique, I wonder if there are ways that people have already figured out to provide useful error messages. We might be able to attach syntax properties containing the original source expressions and then write the expansions in such a way that they check for list? at appropriate times and blame the right source expression. But that'd probably be easier to figure out down the line when we know exactly how the expansions work.

Good thought! I hope the error messages don't end up being too opaque; it's one thing that concerns me about massive rewriting under the hood :)

Ah whoops looks like our messages crossed. Having proofs is indeed valuable, thanks for furnishing them!

Looks like I didn't refresh before posting.

I'm going to continue my reading but working the proofs today is out (cycling injury). "Next time on …", as they say.

[countvajhula]

@michaelballantyne pointed out today that while maps and filters operate on individual elements, folds are able to reason about the structure of the list as a whole. So if one fold were to reverse the order of elements (e.g. (foldl cons null (list 1 2 3)), then it may not be possible for the next fold to account for that. He would guess that this kind of fold composition is not possible in the general case.

It'd be nice to have a proof one way or the other, of course (and I'm now wondering whether playing with the composition order in the binary functions used in folding could address the order issue, i.e. a -> b -> b vs b -> a -> b... probably not?), but until such a time, he suggested treating map and filter as primitives as far as this kind of composition is concerned, for which we could apply the identities that you proved above. This would mean that we can compose any contiguous sequence of Fs where F ∈ {map,filter}, while leaving (a priori) folds alone.

Michael also mentioned "supercompilation" as another approach to consider (which happens to be the subject of one of the resources linked above).

Cycling injury, ouch, sorry to hear that! Take it easy and get well soon! 🤕 🛏️ ➡️ 🏃

[benknoble]

I'm still investigating the "composing folds" idea, but I need to dig into some papers linked from A tutorial on the universality and expressiveness of fold, particularly on deforestation.

I aim to prove that such a composition is either always possible (constructively, so that the composition is shown, if possible) or it is not always possible by giving a concrete counter-example (clearly with map and filter it is possible, therefore it is sometimes possible).

Unfortunately, I cannot see a quick way to derive a contradiction assuming the composition is possible, so I may need to rely on a proof that the composed fold is somehow "inexpressible"? I'm running out of ideas, hence my desire to dig into the papers.

In the meantime, proceeding with map + filter is a good idea. One interesting difficulty is that Racket's map and folds are variable arity; filter is not. Both map and folds require lists of the same length, at least.