Second order function formalization

Question

I need to work on a optimizer for a language whose operator are second order functions.

They are the well known ones filter, map, reduce, fold, foreach etc. etc.

I need to formalize as much as possible the language. I mean I would like to have at the end a description such this:

"Filter is function from this domain to that codomain, it has this and that properties, under some condition also this property holds"

Can you suggest me some publication/book where this work has been (at least partially) done?

Answer 1

You may not be able to completely specify formally in a tractable way the semantics of your functions, depending on what they are. But doing some of the work, even incompletely may help you significantly with optimizing your programs, since it may be enough to establish whatever properties are needed for optimization.

The first thing you want to do is to type your functions. For this, you probably want some kind of polymorphic typing (see ML or CAML), using type variables, as some of the base types you operate on will be left open.

Most of these function take several arguments, and (following the discussion in comments with @Jake) you may want to consider what would be a convenient order, and more to the point, whether you want them curried (or currified) or not.

For example, if we note [a] the type for a list of elements of type a, then you can define the function map as:

• a function of two arguments, the first being a function from a to b, and the second a list in [a], and returning a list in [b], i.e.
  map: (a→b)×[a] →[b]

• a function of one argument which is a function from a to b, and returns a specialized mapping function that maps lists in [a] to lists in [b], as specified by the argument to map, i.e.
  map: (a→b) →([a]→[b])

The latter is a curried version of the former. They give you the same computing power, but the curried one may be more convenient for optimization (just my intuition) as it decomposes structures.

Then the kind of information that you may need may depend on the kind of optimizations you intend to implement. Many types of optimizations ("strength reduction" is a typical example) may require knowing algebraic properties of your functions. But that may also depend on the algebraic properties of the types or type constructors used, such as the existence of "identity element" with respect to some operations (such as the empty list). I doubt your specification/formalization problem can be restricted to just your second order functions.

Typically, a relation such as:

head (map (f,l))= f(head(l)) may be very useful for some optimizations.

or more trivially:

map(f,[]) = [] where [] denote the empty list.

I do not recall all the literature on these issues. But you may want to look at abstract data types, formal algebras, and the algebraic techniques used in optimization.

There are probably other properties, less algebraic, that you may be interested in defining and using.

An important aspect is also whether your function are purely functional, or whether they have side effects. A map function could possibly destroy the list given as argument, the result reusing the same memory locations.

Answer 2

You may want to have a look at the Coq proof assistant. Its type system allows to express types as in other functional languages (e.g. filter is a function from [A] to [A]) and much more. You can easily add arbitrary properties.

Here is the definition of filter, taken from the list module of the standard library:

Fixpoint filter (l:list A) : list A :=
  match l with
    | nil => nil
    | x :: l => if f x then x::(filter l) else filter l
  end.

Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true.

The first part is a usual definition of filter, but the last line expresses more interesting features about it.