Sebastian Fischer schrieb:
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) .
My gut feeling is that this statement indeed holds. To prove it, one
might have to use a generalization of the logical relations proof
technique from binary relations to n-ary relations, where n is the
number of inhabitants of your fixed type a.
For finite n, the mentioned generalization is unproblematic, so the
argument easily transfers from a=Bool to all finite a. For countable n,
I am not aware of the proper formal development, but again I think that
the statement holds. Whether to prove this via a generalization to
relations with countable arity, or whether via some encoding into list
types or so, I don't know...
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.
In personal communication, Jean-Philippe added that for your type "(Bool
-> a) -> a" the statement that any such function is either ($True) or
($False) does *not* follow from the results in that paper. So I gather
that you will find neither proof nor counterexample for the more general
statement in that paper either. (It's worth reading nevertheless!)
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
My take would be: for any a and f as you mention, there is a list l::[a]
such that
f k = foldr mappend mempty (map k l)
That would be under the precondition (only) that all Monoid instances
satisfy the monoid laws.
If we don't have this precondition, then instead of l::[a] I would
demand the existence of some binary (or empty) tree with leaf nodes of
type a, and in the definition of f above, I would replace the map and
foldr by the corresponding operations over such trees.
In both cases, your statement that f is either ($x) for some x::a or is
const mempty or can be "factored" into some g and h via mappend, is a
relatively direct consequence of my statement(s).
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.
I'm pretty confident that there are no counterexamples. A proof via
type-based reasoning would of course have to solve the problems I
mentioned above about countability of type a, and additionally involve a
free theorem involving type class Monoid (which the online generator can
derive, albeit for the case of binary relations/functions only, of course).
Ciao,
Janis.
--
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:[email protected]
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
