Announce: generating free theorems, online and offline
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
[Ccing to haskell-cafe; please direct any replies there instead of haskell] G'day all. First of all, once again well done to Sascha on a great tool. Just a few comments. Quoting Janis Voigtlaender <voigt@tcs.inf.tu-dresden.de>:
- support for type classes (e.g., enter "elem" and note the generated respects-restrictions)
This is a great feature, and it'll be even better when constructor classes are done. Some of these respects-restrictions arent as useful as they might be, because they don't take into account easily-predictable invariants. For example, the type: (Eq a) => [a] -> [a] generates the following restriction: g respects Eq if forall x :: t1. forall y :: t1. (==) x y = (==) (g x) (g y) forall x :: t1. forall y :: t1. (/=) x y = (/=) (g x) (g y) Thats correct, but redundant, because (x == y) = (g x == g y) if and only if (x /= y) = (g x /= g y). Crucially, you can work this out from the definition of Eq, because (/=) has a default implementation defined in terms of (==) alone. The type (Monoid a) => [a] -> a gives: forall t1,t2 in TYPES(Monoid), g :: t1 -> t2, g respects Monoid. forall x :: [t1]. g (f x) = f (map g x) The class restriction occurring therein is defined as follows: g respects Monoid if g mempty = mempty forall x :: t1. forall y :: t1. g (mappend x y) = mappend (g x) (g y) forall (x, y) in lift{[]}(g). g (mconcat x) = mconcat y Again, mconcat is redundant. Even more curiously, though, map appears in the theorem, but lift{[]} appears in the class restriction. Cheers, Andrew Bromage
participants (2)
-
ajb＠spamcop.net -
Janis Voigtlaender