How do I implement this transformation using generics?

Learn
1

Let’s say I have a data type for integer lists. There are two Conses: one that takes a normal List, and one that takes a DeeperList, which just embeds a List.

data DeeperList = DeeperList List
data List = Nil
            | Cons1 Int List
            | Cons2 Int DeeperList

I’d like to write a function incr:

incr :: Int -> List -> List

such that incr k l increments each integer in l by k plus the number of DeeperLists that embeds that integer. For example:

incr 3 $ Cons1 2 $ Cons2 4 $ DeeperList $ Cons2 0 $ DeeperList $ Cons1 5 Nil
         -------------------------------------------------------------------
         --  represented more compactly as [ 2, 4, D[ 0, D[ 5 ]]]

should be:

Cons1 5 $ Cons2 7 $ DeeperList $ Cons2 4 $ DeeperList $ Cons1 10 Nil
-------------------------------------------------------------------
--  [ 5, 7, D[ 4, D[ 10 ]]]

I’d like to implement incr with generics, specifically with something like gfoldl, gmapT, etc., stuff from Data.Data. How do I do that?

2

It’s not often someone asks about generics and means Data.Data!

Here’s one way to do it, setting the c type of gfoldl to (->) Int. fld is the function that handles one field of a constructor. Within fld, the k j d calls mean: continue with the rest of the fields (to the left) of this constructor, using j as increment value and d as the replacement value for the current field. So in the case of an Int field, we use d + j as replacement, in the case of DeeperList, we recurse (using go) with j + 1 as increment. Otherwise (here only in the case of List) recurse with the current increment value.

Pattern matching on Refl tells the compiler that the two arguments to eqT are equal, which we need in the Int case, otherwise d + j wouldn’t type-check.

incr :: Int -> List -> List
incr = go
  where
    go :: Data d => Int -> d -> d
    go i l = gfoldl fld const l i
    fld :: forall d b. Data d => (Int -> d -> b) -> d -> Int -> b
    fld k d j = case eqT @d @Int of
      Just Refl -> k j (d + j)
      Nothing -> case eqT @d @DeeperList of
        Just Refl -> k j (go (j + 1) d)
        Nothing -> k j (go j d)