[Haskell] Announce: generating free theorems, online and offline

[Janis Voigtlaender]

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 at tcs.inf.tu-dresden.de