[Haskell-cafe] determine a type by universal property

[Olaf Klinke]

Dear cafe,

We know how to derive free theorems from a type [1]. But there exist also
examples where the existence of a certain function determines the type. I suppose this is a special case of a free theorem? For example, every functor that is right adjoint to another functor in Hask is
representable in the sense of [2], that is, isomorphic to (r->) for some type r. [see * below]

I have two type signatures where I conjecture the only functors satisfying these
are the Identity functor and functors of the form (,)s. Can anyone give hints as
how to tackle a proof?

Signature 1: What functors t admit a function
forall f. Functor f => t (f a) -> f (t a)

Signature 2: What functors t admit a function
t (t a -> b) -> a -> b

Signature 1 is like Data.Traversable.sequence, only the Applicative constraint is
weakened to Functor. It is somewhat dual to Distributive [3]. Signature 2 can,
with some currying, for t = (,)s be transformed into Data.Function.flip. 

I am unable to comprehend the free theorem for signature 2. For signature 1, the Rank-2 type seems to cause trouble with free-theorems? 

Thanks,
Olaf

[1] https://hackage.haskell.org/package/free-theorems
[2] https://hackage.haskell.org/package/adjunctions
[3] https://hackage.haskell.org/package/distributive
[*] The argument goes like this:
(1)  bottoms aside, every type x is isomorphic to () -> x.
(2) f and g are adjoint if and only if (f a -> b) is isomorphic to (a -> g b).
(3) g b is isomorphic to () -> g b by (1) with x = g b
(4) () -> g b is isomorphic to f () -> b by (2) with a = ().
(5) By (3) and (4), g b is isomorphic to f () -> b. We have found g = (r->) with r = f ().