Re: [Haskell-cafe] determine a type by universal property

Am 18.01.2019 um 13:00 schrieb haskell-cafe-request@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)

What about the functor

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 :

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 MonadFoo m => MonadFoo (BarT m) e.g. MonadExcept m => MonadExcept (StateT s m) One can factor StateT s into two adjoint functors, G = (s->) and F = (,)s. For defining the instance above generically it was necessary for the functor F to aadmit functions with the signatures in my original post. Then I conjectured that I actually had not generalized anything if the signatures forced my F to be of the form (,)s. Olaf