Higher-Order List Functions

Here is a useful higher-order function, taking a list of Xs and a predicate on X (a function from X to bool) and "filtering" the list, returning a new list containing just those elements for which the predicate returns true.

For example, if we apply filter to the predicate evenb and a list of numbers l, it returns a list containing just the even members of l.

We can use filter to give a concise version of the countoddmembers function from the Lists chapter.

Higher-order Functions and Anonymous Functions: Together Forever

It is arguably a little sad, in the example just above, to be forced to define the function length_is_1 and give it a name just to be able to pass it as an argument to filter, since we will probably never use it again. Moreover, this is not an isolated example: when using higher-order functions, we often want to pass as arguments "one-off" functions that we will never use again; having to give each of these functions a name would be tedious. Fortunately, we've already seen a better way. We can construct a function "on the fly" without declaring it at the top level or giving it a name.

Exercise: 2 stars, standard (filter_even_gt₇)

Use filter (instead of Fixpoint) to write a Coq function filter_even_gt₇ that takes a list of natural numbers as input and returns a list of just those that are even and greater than 7.

Exercise: 3 stars, standard (partition)

Use filter to write a Coq function partition:
      partition : ∀ X : Type,
                  (X → bool) → list X → list X × list X Given a set X, a predicate of type X → bool and a list X, partition should return a pair of lists. The first member of the pair is the sublist of the original list containing the elements that satisfy the test, and the second is the sublist containing those that fail the test. The order of elements in the two sublists should be the same as their order in the original list. Your definition should not be recursive: just use filter!

enumerate is a handy function for processing a list of items and which item each one is. Here we'll define it using zero_to_n!

Map

Another handy higher-order function is called map. Perhaps you've heard of systems like MapReduce or Hadoop---they're massive, distributed systems that implement efficient computations on huge datasets using what are common higher-order functions like map and reduce (similar to fold, which we'll introduce later).

It takes a function f and a list l = [n₁, n₂, n₃, ...] and returns the list [f n₁, f n₂, f n₃,...] , where f has been applied to each element of l in turn. For example:

The element types of the input and output lists need not be the same, since map takes two type arguments, X and Y; it can thus be applied to a list of numbers and a function from numbers to booleans to yield a list of booleans:

It can even be applied to a list of numbers and a function from numbers to lists of booleans to yield a list of lists of booleans:

Exercise: 2 stars, standard (complementary')

Define a different version of complementary that doesn't use recursion; you may of course call a recursive function. (Hint: try using map!)

Exercise: 2 stars, standard (map_option)

We can also use lists and options together. Define a function map_option that takes a function f : X → option Y and a list of Xs and returns a list of those Ys for which f didn't return None. Take X and Y as implicit arguments.

EX₂ (min_by) Remember argmin? What if we wanted it to work for an arbitrary number of objects? We have list_min from last time, but that only works on lists of nats. Can we come up with min_by which takes a cost function and a list and gives the least element from the list according to that function? It will look very similar to list_min!

Exercise: 2 stars, standard (flat_map)

The function map maps a list X to a list Y using a function of type X → Y. We can define a similar function, flat_map, which maps a list X to a list Y using a function f of type X → list Y. Your definition should work by 'flattening' the results of f, like so:
        flat_map (fun n ⇒ [n;n+1;n+2]) [1;5;10]
      = [1; 2; 3; 5; 6; 7; 10; 11; 12].

Exercise: 2 stars, standard, optional (map_option')

The flat_map function defined above is a little bit more general than map_option. Define a function map_option' that has map_option's type, but uses flat_map to do the work. You'll need to somehow take f : X → option Y and produce some other function of type X → list Y.

One very general higher-order list function is fold_right. Fold takes three arguments: a function f : X → Y → Y, an initial value of type Y, and a list X. It outputs a Y. Fold will call f with each element of the list in turn (starting from the back and going to the front) along with the result of the previous call to f (or, for the first element of the list, the initial value). It can be used in a variety of fun ways:

fold_left is like fold_right but applies the function starting from the seed and first element:

What's the first day I like?

What's the last day I like?

Can we do it with a friendly combinator?

We can go combinator-crazy:

Ahh, so concise!

We can pack it into a handy helper:

And now we're done with this weekday picking example, we've reached the apotheosis of day selection. Fold is extremely generic, and many of our list functions can be built on top of it. map via fold_right:

length:

How is it so general? Well, look at its definition---fold_right and fold_left are pretty much just our list fixpoint template! Take map as an example, and compare it with fold_right (renaming f in fold_right to g for clarity):
  match l with
  | [] ⇒ []
  | h :: t ⇒ cons (f h) (map f t)
  end

  match l with
  | [] ⇒ seed
  | a :: l' ⇒ g a (fold_right g seed l')
  end. We can rearrange the terms of map like so:
  let g := (fun a rest ⇒ cons (f a) rest) in
  match l with
  | [] ⇒ []
  | h :: t ⇒ g h (map f t)
  end fold_right just makes g and the base case output into parameters!
  match l with
  | [] ⇒ acc (* for map, this is  --- the base case *)
  | a::l' ⇒ g a (fold_right g seed l') (* if g does cons (f a) rest then this is just map'! *)
  end

Exercise: 2 stars, standard (fold_practice)

Can you implement filter, flat_map, and min_by using folds? No fixpoints allowed! Hints: For filter', look at map'! For flat_map', also look at map' but think about how you'll be adding elements onto the list.

This one is tricky. Check out the weekday example earlier. unwrap_or may be convenient!