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.