[Haskell-cafe] determine a type by universal property
Joachim Breitner
mail at joachim-breitner.de
Thu Jan 17 14:46:01 UTC 2019
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
mail at joachim-breitner.de
http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190117/0c842bfd/attachment.sig>
More information about the Haskell-Cafe
mailing list