[Haskell-cafe] determine a type by universal property

[Oleg Grenrus]

I'd say that

    forall f. t (f a) -> f (t a)

with f = Identity

    should be identity.

And there's probably some composition/associativity law, about t (f (g
a)) -> f (g (t a))

---

I also sent direct answer, which would benefit from this additional laws
too:
Lensy/Traveral business this is.

I immediately see

    forall f a b. Functor f => (a -> f b) -> t a -> f (t b)

which is Lens' (t a) a, which is an iso

   exists e. (t a) ~ (e, a)

Maybe that helps to find some pointers.

You can remove Functor f using yoneda lemma, so you get Rank1Type

    forall a b. t a -> (a, b -> t b)

For which you can apply free theorem's machinery?

- Oleg

On 17.1.2019 16.46, Joachim Breitner wrote:
> Hi,
>
> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190117/e0b31b1f/attachment.sig>