Haskell generics. Constructing Rep

Question

I got stuck on this tutorial https://ocharles.org.uk/blog/posts/2014-04-26-constructing-generically.html when trying verify the type of mk for l :*: r when l = K1 _ a, fl = ((->) a) and r = K1 _ b, fr = ((->) b)

class Functor f => Mk rep f | rep -> f where
  mk :: f (rep a)

instance Mk (K1 i c) ((->) c) where
  mk = \x -> K1 x

instance (Mk l fl, Mk r fr) => Mk (l :*: r) (Compose fl fr) where
  mk = Compose (fmap (\l -> fmap (\r -> l :*: r) mk) mk)

Now by the type class definition mk :: f (rep _) and we have f = Compose ((->) a) ((->) b) = * -> a -> b -> * and rep _ = l:*:r and so mk :: a -> b -> l:*:r. This is what I expected.

However, I think (fmap (\l -> fmap (\r -> l :*: r) mk) mk) :: a -> b -> l:*:r and I cant see how using this as a first argument to Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> * will ever give back the expected signature of mk??

Also, I found this answer https://stackoverflow.com/a/35424427/11998382 helpful but I got lost at

f :: Compose ((->) a) ((->) b) (f r)
g :: Compose ((->) c) ((->) d) (g r)
mk f g :: Compose (Compose ((->) a) ((->) b)) (Compose ((->) c) ((->) d)) ((:*:) f g r)

Did they mean fl :: Compose ((->) a) ((->) b) (f r) or mk f :: Compose ((->) a) ((->) b) (f r)?

Daniel Wagner · Accepted Answer · 2021-07-18T15:57:48.047

we have f = Compose ((->) a) ((->) b) = * -> a -> b -> * and rep _ = l:*:r and so mk :: a -> b -> l:*:r

You've got the spirit, but there's a few details I want to quibble on here.

First: Compose ((->) a) ((->) b) is not equal to anything interesting except itself. However, it is isomorphic to some other interesting types. For example, Compose ((->) a) ((->) b) c is isomorphic (but not equal!) to a -> b -> c. (I'm not sure what the *'s are in your equality or where they came from, though.)

Second: in this instance, rep (not rep _) is being replaced by l :*: r. Consequently, where you replaced rep a by l :*: r, you should actually be replacing rep a by (l :*: r) a (or, up to alpha renaming, rep c by (l :*: r) c). Like we did with Compose, we could observe an isomorphism here, namely that (l :*: r) c is isomorphic to (l c, r c).

Putting these together, we have

f (rep a)
= { alpha renaming: a is not bound (but f and rep are) }
f (rep c)
= { definition of f and rep }
Compose ((->) a) ((->) b) ((l :*: r) c)
~= { the two isomorphisms described above }
a -> b -> (l c, r c)

However, I think (fmap (\l -> fmap (\r -> l :*: r) mk) mk) :: a -> b -> l:*:r and I cant see how using this as a first argument to Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> * will ever give back the expected signature of mk

Beware! There are two entities named Compose. One is at the type level, and has the kind you gave:

Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> *

But there is another at the computation level, with a very different-looking type:

Compose :: f (g a) -> Compose f g a

In this type, the first Compose is the computation-level Compose, and the second Compose in is the type-level Compose.

It is the term-level Compose that is being used in the definition of mk, not the type-level one as you seem to be assuming. (In this part, you've also not been careful about the distinction between l :*: r and (l :*: r) c, as in the last bit.) So the correct version of the quoted statement is: (fmap (\l -> fmap (\r -> l :*: r) mk) mk) :: a -> b -> (l:*:r) c, so using this as the first argument to Compose :: f (g a) -> Compose f g a means that Compose (fmap ... mk) :: Compose ((->) a) ((->) b) ((l:*:r) c).

Thanks! this has been valuable. I probably meant `Compose ((->) a) ((->) b) :: * -> a -> b -> *` rather than equals — Tom Huntington, Jul 20 '21 at 22:01
@TomHuntington Okay. Well, if that's what you meant, it's still not quite right: `Compose ((->) a) ((->) b) :: * -> *`. — Daniel Wagner, Jul 21 '21 at 02:08

Tom Huntington · Answer 2 · 2021-07-20T23:23:32.107

So Compose is defined

newtype Compose f g a = Compose {getCompose :: f (g a)}

The return type of getCompose

Prelude Data.Functor.Compose> :t getCompose

getCompose :: Compose f g a -> f (g a)

is of kind * and so determines the kind of Compose

Prelude Data.Functor.Compose> :k Compose

Compose :: (k -> *) -> (k1 -> k) -> k1 -> *

And the data constructor has type

Prelude Data.Functor.Compose> :t Compose

Compose :: f (g a) -> Compose f g a

So the purpose of Compose is just to encode types, it doesn't do anything with the term it stores.

I need to stop getting confused between type and data constructors, in Haskell you cant only tell the difference by the context.

Haskell generics. Constructing Rep

2 Answers2