[Haskell] Announce: FreeTheorems library and tools

[Janis Voigtlaender]

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