determine a type by universal property

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

determine a type by universal property

Olaf Klinke
Dear cafe,

We know how to derive free theorems from a type [1]. But there exist also
examples where the existence of a certain function determines the type. I suppose this is a special case of a free theorem? For example, every functor that is right adjoint to another functor in Hask is
representable in the sense of [2], that is, isomorphic to (r->) for some type r. [see * below]

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)

Signature 2: What functors t admit a function
t (t a -> b) -> a -> b

Signature 1 is like Data.Traversable.sequence, only the Applicative constraint is
weakened to Functor. It is somewhat dual to Distributive [3]. Signature 2 can,
with some currying, for t = (,)s be transformed into Data.Function.flip.

I am unable to comprehend the free theorem for signature 2. For signature 1, the Rank-2 type seems to cause trouble with free-theorems?

Thanks,
Olaf

[1] https://hackage.haskell.org/package/free-theorems
[2] https://hackage.haskell.org/package/adjunctions
[3] https://hackage.haskell.org/package/distributive
[*] The argument goes like this:
(1)  bottoms aside, every type x is isomorphic to () -> x.
(2) f and g are adjoint if and only if (f a -> b) is isomorphic to (a -> g b).
(3) g b is isomorphic to () -> g b by (1) with x = g b
(4) () -> g b is isomorphic to f () -> b by (2) with a = ().
(5) By (3) and (4), g b is isomorphic to f () -> b. We have found g = (r->) with r = f ().
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: determine a type by universal property

Joachim Breitner-2
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-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: 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.

_______________________________________________
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.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: determine a type by universal property

Olaf Klinke
In reply to this post by Olaf Klinke
Am 18.01.2019 um 13:00 schrieb [hidden email]:

>
> 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 <[hidden email]>:
>
> 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
_______________________________________________
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.