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 holdsCan you suggest me some publication/book where this work has been (at least partially) done?
Second order function formalization
programming languages;functional programming;formal methods;program optimization;abstract data types
You may not be able to completely specify formally in a tractable waythe semantics of your functions, depending on what they are. But doingsome of the work, even incompletely may help you significantly withoptimizing your programs, since it may be enough to establish whateverproperties 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 beleft open.Most of these function take several arguments, and (following thediscussion in comments with @Jake) you may want to consider what wouldbe a convenient order, and more to the point, whether you want themcurried (or currified) or not.For example, if we note [a] the type for a list of elements of typea, then you can define the function map as:a function of two arguments, the first being a function from a tob, and the second a list in [a], and returning a list in [b], i.e.map: (ab)[a] [b]a function of one argument which is a function from a tob, 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: (ab) ([a][b])The latter is a curried version of the former. They give you thesame computing power, but the curried one may be more convenient foroptimization (just my intuition) as it decomposes structures.Then the kind of information that you may need may depend on the kindof optimizations you intend to implement. Many types of optimizations(strength reduction is a typical example) may require knowingalgebraic properties of your functions. But that may also depend onthe algebraic properties of the types or type constructors used, suchas the existence of identity element with respect to someoperations (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 wantto look at abstract data types, formal algebras, and the algebraictechniques used in optimization.There are probably other properties, less algebraic, that you may beinterested in defining and using. An important aspect is also whether your function are purelyfunctional, or whether they have side effects. A map function couldpossibly destroy the list given as argument, the result reusing thesame memory locations.