A while back I announced a library and tools for generating free theorems from Haskell types: http://www.haskell.org/pipermail/haskell/2006-August/018426.html There is now an improved version with new features. To try it out online, visit: http://linux.tcs.inf.tu-dresden.de/~voigt/ft Highlights are: - support for type classes (e.g., enter "elem" and note the generated respects-restrictions) - three different language subsets to choose from, including one that takes selective strictness into account and thus gives theorems that are valid even in the presence of seq and friends (e.g., enter "filter" and compare the outputs for the three language subsets) - equational as well as inequational free theorems, the latter often coming with less restrictive preconditions, and thus being applicable where equational free theorems are not (e.g., enter "head" and compare the outputs in equational vs. inequational style for the second or third language subset) The source code of the library is available from: http://wwwtcs.inf.tu-dresden.de/~voigt/dist.tar.gz This package additionally contains a shell-like interface to the library, giving more control than the web interface. In particular, using it one can declare one's own algebraic data types, type synonyms, type renamings and type classes, and then generate free theorems for types involving those. Credits for the implementation are due to Sascha Boehme! Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de