[Haskell] Announce: revamped free theorems generator

Janis Voigtländer jv at informatik.uni-bonn.de
Sun Jun 20 07:57:41 EDT 2010

Jean-Philippe Bernardy schrieb:
> On Sun, Jun 20, 2010 at 12:47 PM, Janis Voigtländer
> <jv at 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

Yes, kind of. I had this in mind when asking Andreas for a kind of
characterization akin to his "f :: a -> a can only be identity" example,
but for the type [a] -> [a]. The point being that one doesn't get a
finite enumeration of possible values, except in very few cases.

BTW, can one get a characterization from your results, establishing
*when* the class of possible (semantic) values of a type is finite?


Jun.-Prof. Dr. Janis Voigtländer
mailto:jv at iai.uni-bonn.de

More information about the Haskell mailing list