[Haskell] Announce: revamped free theorems generator
jv at informatik.uni-bonn.de
Tue Jun 22 07:32:38 EDT 2010
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]
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).
Jun.-Prof. Dr. Janis Voigtländer
mailto:jv at iai.uni-bonn.de
More information about the Haskell