# [Haskell-cafe] determine a type by universal property

Thu Jan 17 13:33:14 UTC 2019

```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