Hello all, Sascha Boehme, a student of mine, has done a project to implement the Reynolds/Wadler algorithm generating theorems from polymorphic types, plus simplifications and postprocessings for such free theorems. The result can be found at: http://haskell.as9x.info To play with the tool online, follow the link http://haskell.as9x.info/ft.html input some valid Haskell type (there are some restrictions, for example no type classes; see the description), and enjoy the result. The types of many standard Haskell functions are predefined, for example you can also simply enter "filter" to generate the respective free theorem. (For a more complicated example, with still quite readable output, try "zip".) Free theorems can be generated in two "models". The "basic model" is the one from the original papers, ignoring the presence of _|_ and fixpoint recursion in Haskell, thus delivering simpler theorems that are only "morally correct" (a slight abuse of this term from the recent POPL paper). The "fix model" takes _|_ and fixpoint recursion into account, delivering more complicated theorems (mainly by including strictness preconditions). The proper treatment of seq being present in Haskell is not yet implemented. Finally, there is also a Shellac-based interpreter-like tool available for download, with slightly more powerful postprocessing facilities. If you have comments, questions, suggestions, please answer on the list or write directly to Sascha (see CC above) or myself. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de