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:[EMAIL PROTECTED]

_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to