# determine a type by universal property

4 messages
Open this post in threaded view
|

## determine a type by universal property

Open this post in threaded view
|

## Re: determine a type by universal property

 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 -- Joachim Breitner   [hidden email]   http://www.joachim-breitner.de/_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (849 bytes) Download Attachment