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

Reply via email to