Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Traversable instance for general type composition

I am completely stuck on this is an exercise from the excellent Haskell Programming book.

Given the following newtype for type composition and instances of Functor and Applicative, write an instance of Traversable (Compose f g).

newtype Compose f g a =
  Compose { getCompose :: f (g a) }
  deriving (Eq, Show)

instance (Functor f, Functor g) => Functor (Compose f g) where
  fmap f (Compose fga) = Compose $ (fmap . fmap) f fga

instance (Applicative f, Applicative g) => Applicative (Compose f g) where
  pure = Compose <$> pure . pure
  Compose f <*> Compose x =
    Compose $ ((<*>) <$> f) <*> x

My proposed solution looks like it should work, based on the type of traverse.traverse but ghci complains. I have a vague feeling it is something to do with re-wrapping in the Compose constructor:

instance (Traversable f, Traversable g) => Traversable (Compose f g) where
  traverse f1 (Compose fga) = (traverse.traverse) f1 fga

gives the type error:

composing_types.hs:69:31:
    Couldn't match type ‘b’ with ‘g b’
      ‘b’ is a rigid type variable bound by
          the type signature for
            traverse :: Applicative f1 =>
                        (a -> f1 b) -> Compose f g a -> f1 (Compose f g b)
          at composing_types.hs:69:3
    Expected type: f1 (Compose f g b)
      Actual type: f1 (Compose f g (g b))
    Relevant bindings include
      fga :: f (g a) (bound at composing_types.hs:69:24)
      f1 :: a -> f1 b (bound at composing_types.hs:69:12)
      traverse :: (a -> f1 b) -> Compose f g a -> f1 (Compose f g b)
        (bound at composing_types.hs:69:3)
    In the expression: (traverse . traverse) f1 fga
    In an equation for ‘traverse’:
        traverse f1 (Compose fga) = (traverse . traverse) f1 fga

composing_types.hs:69:54:
    Couldn't match type ‘f’ with ‘Compose f g’
      ‘f’ is a rigid type variable bound by
          the instance declaration at composing_types.hs:68:10
    Expected type: Compose f g (g a)
      Actual type: f (g a)
    Relevant bindings include
      fga :: f (g a) (bound at composing_types.hs:69:24)
      traverse :: (a -> f1 b) -> Compose f g a -> f1 (Compose f g b)
        (bound at composing_types.hs:69:3)
    In the second argument of ‘traverse . traverse’, namely ‘fga’
    In the expression: (traverse . traverse) f1 fga
like image 341
Stephen Pascoe Avatar asked May 02 '16 16:05

Stephen Pascoe


1 Answers

H O L E S

This is another great question that can be solved with holey expressions.

First, let's assume we have Foldable instances all defined already.

λ> instance (Foldable f, Foldable g) => Foldable (Compose f g) where
     foldr = undefined

Next, instance Traversable. Pattern match on the Compose argument because you know you will have to, but otherwise leave everything in a hole.

λ> instance (Traversable t, Traversable u) => Traversable (Compose t u) where
     traverse a2fb (Compose tua) = _ tua

GHC will helpfully spit out an error–

<interactive>:...:...
  Found hole ‘_’ with type: f (Compose t u b)

–in addition to the types of all variables in scope.

Relevant bindings include
  tua :: t (u a) (bound at ...)
  a2fb :: a -> f b (bound at ...)
  traverse :: (a -> f b) -> Compose t u a -> f (Compose t u b)
    (bound at ...)

(I have chosen the type and value names so that everything lines up neat. Pay no attention to the man behind the curtain.) Now then the question of the hour: how to conjure a value of f (Compose t u b) given everything else. We know

  • The only way to construct Compose t u b is by creating a value t (u b).

  • There is no way to produce a value of f anything except by (1) pure and (2) fmap, and intuitively we know we cannot use pure because we are trying to collect the 'side effects' of a2fb :: a -> f b here.

This leads us to our next stab at the solution.

λ> instance (Traversable t, Traversable u) => Traversable (Compose t u) where
     traverse a2fb (Compose tua) =
       fmap Compose (_ tua)

<interactive>:...
  Found hole ‘_’ with type: t (u a) -> f (t (u b))

At last we have a t. We know t is Traversable so let's try traversing it.

λ> instance (Traversable t, Traversable u) => Traversable (Compose t u) where
     traverse a2fb (Compose tua) =
       fmap Compose ((\tua -> traverse _ tua) tua)

<interactive>:56:138:
  Found hole ‘_’ with type: u a -> f (u b)

Same deal. We know u is Traversable so let's try traversing it.

λ> instance (Traversable t, Traversable u) => Traversable (Compose t u) where
     traverse a2fb (Compose tua) =
       fmap Compose ((\tua -> traverse (\ua -> traverse _ ua) tua) tua)

<interactive>:57:155:
  Found hole ‘_’ with type: a -> f b

A goldilocks hole for our a2fb.

λ> instance (Traversable t, Traversable u) => Traversable (Compose t u) where
     traverse a2fb (Compose tua) =
       fmap Compose ((\tua -> traverse (\ua -> traverse a2fb ua) tua) tua)

Eta-reduce to excise the lambdas, and you end up with the solution.

λ> instance (Traversable t, Traversable u) => Traversable (Compose t u) where
     traverse a2fb (Compose tua) =
       fmap Compose (traverse (traverse a2fb) tua)
like image 183
hao Avatar answered Sep 28 '22 05:09

hao