On Sun, Jun 20, 2010 at 12:47 PM, Janis Voigtländer <jv@informatik.uni-bonn.de> wrote:
Sebastian Fischer schrieb:
Hello,
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`.
Did you manage to do this now?
Driven by Andreas' comment about what he considers "free theorems", statements like the above about an exhaustive enumeration of possible values of a given type, like
- ($True) and ($False) for type (Bool -> a) -> a - id for type a -> a
In any case, for additional possibilities like "exhaustive value enumeration (where possible at all)", I don't yet have a generic strategy.
Using the main result of our ESOP paper (Testing Polymorphic Properties), you can get there for a large class of input types. http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=99387 Cheers, JP.