Second order function formalization

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?

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.

StackExchange Computer Science Q#33480, answer score: 2