[Haskell] Announce: revamped free theorems generator
Sebastian Fischer
sebf at informatik.uni-kiel.de
Tue Jun 22 06:27:03 EDT 2010
On Jun 20, 2010, at 12:47 PM, Janis Voigtländer wrote:
>> 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?
Now it seems you did it for me, thanks!
I am interested in a more general statement like
For every given type a and function f :: forall b . (a -> b) -> b
there exists an x :: a such that f = ($x) .
Jean-Philippe's remark
> Using the main result of our ESOP paper (Testing Polymorphic
> Properties),
> you can get there for a large class of input types.
suggests that this may not be true for certain types a .
I need to read his paper again for the proof idea. Maybe I'll find a
counter example then.
A variant of the above statement incorporating type classes is:
For every given type a and function
f :: forall b . Monoid b => ((a -> b) -> b)
one of the following cases holds:
there exists x such that f = \k -> k x
f = \_ -> mempty
there exists g and h such that f = \k -> g k `mappend` h k
I find these statements plausible and would be interested in counter
examples. If they are true, I'd feel that they may be easily shown by
type information only, that is via free theorems.
Sebastian
--
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)
More information about the Haskell
mailing list