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

Sat Jan 19 22:37:53 UTC 2019

```Am 18.01.2019 um 13:00 schrieb haskell-cafe-request at haskell.org:
>
> Am Donnerstag, den 17.01.2019, 14:33 +0100 schrieb Olaf Klinke:
>> 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)
>
>
>   data Void1 a
>
> It seems I can write
>
>   g :: forall f. Functor f => t (f a) -> f (t a)
>   g x = case x of {}
>
> but Void1 is not the identity. (I guess it is `(,) Void`, if you want…)
>
> So if you allow the latter, let’s try a proof. Assume we have t, and
>
>   g :: forall f. Functor f => t (f a) -> f (t a)
>
> We want to prove that there is an isomorphism from t to ((,) s) for
> some type s. Define
>
>   s = t ()
>
> (because what else could it be.) Now we need functions
>
>   f1 :: forall a. t a -> (t (), a)
>   f2 :: forall a. (t (), a) -> t a
>
> that are isomorphisms. Here is one implementation:
>
>   f1 :: forall a. t a -> (t (), a)
>   f1 = swap  . g . fmap (λx → (x,()))
>
>   {- note:
>     x1 :: t a
>     x2 :: t ((,) a ())
>     x2 = fmap (λx → (x,())) x1
>     x3 :: (,) a (t ())
>     x3 = g x2
>     x4 :: (t (), a)
>     x4 = swap x3
>   -}
>
>   f2 :: forall a. (t (), a) -> t a
>   f2 (s, x) = x <\$ s
>
> Now, are these isomorphisms? At this point I am not sure how to
> proceed… probably invoking the free theorem of g? But even that will
> not work nicely. Consider
>
>   type T = (,) Integer
>   g :: forall f. Functor => T (f a) -> f (T a)
>   g (c, fx) = (,) (c + 1) <\$> fx
>
> here we count the number of invocations of g. Surely with this g,
> f2 . f1 cannot be the identity.
>
>
> Cheers,
> Joachim

Hi Joachim,

thanks a lot for the clue. I had not thought about the function \x -> (x,()).
Your last example of g shows that if a g exists, it is not necessarily unique. Possibly I am missing a law for the function g that entails uniqueness. The identity law in Data.Traversable comes to mind and would rule out your last example.

> Am 17.01.2019 um 15:42 schrieb Oleg Grenrus <oleg.grenrus at iki.fi>:
>
> I immediately see
>
>     forall f a b. Functor f => (a -> f b) -> t a -> f (t b)
indeed my type
forall a f. Functor f => t (f a) -> f (t a)
is interdefinable with your type above.
>
> which is Lens' (t a) a,
agreed.

> which is an iso
>
>    exists e. (t a) ~ (e, a)
I fail to follow this step. How does the Lens above imply this isomorphism? Is this a lens-specific thing or were you thinking along the same lines as Joachim?

Let me give a bit of context. I was looking at generic functions that give rise to monad transformer instances of the form