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.)
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
