Haskell syb Data.Generics not working as expected-CodePudding

On a ghci prompt everywhere (mkT (\x -> 2 * x)) (8.7, 21, "word") evaluates to (8.7, 42, "word").

I expected the 8.7 to be doubled as well. Why am I wrong?

CodePudding user response：

Here is a simplification of your case that doesn't use any Data stuff.

module MyModule where

dbl x = 2 * x
myId :: (a->a) -> a -> a
myId f = f
myDbl = myId dbl

Don't type this to the ghci prompt, rather, create a .hs file and load it.

Now check what type myDbl has.

Prelude > :l MyModule
[1 of 1] Compiling MyModule         ( MyModule.hs, interpreted )
Ok, one module loaded.
*MyModule > :t MyModule.myDbl
MyModule.myDbl :: Integer -> Integer

Surprise! Why is it compiling at all? And why the weird types?

Because of the defaulting rules. (Basically, "if you don't know what to do with Num a, just use Integer"). Since myId cannot deal with dbl :: Num a => a -> a, Haskell allows it to take the Integer version.

Disable defaulting by adding default () at the top, and this module no longer compiles.

mkT is no different from myId in this respect.

CodePudding user response：

This is the result of mkT monomorphizing its argument in this particular case, but it turns out there's no broader way to address the issue. mkT isn't doing anything wrong.

It's worth looking first at why everywhere (* 2) doesn't type-check.

ghci> :t everywhere
everywhere
  :: (forall a. Data a => a -> a) -> forall a. Data a => a -> a
ghci> :t (* 2)
(* 2) :: Num a => a -> a
ghci> :t everywhere (* 2)

<interactive>:1:13: error:
    • Could not deduce (Num a) arising from a use of ‘*’
      from the context: Data a
        bound by a type expected by the context:
                   forall a. Data a => a -> a
        at <interactive>:1:12-16
      Possible fix:
        add (Num a) to the context of
          a type expected by the context:
            forall a. Data a => a -> a
    • In the expression: (*)
      In the first argument of ‘everywhere’, namely ‘(* 2)’
      In the expression: everywhere (* 2)

everywhere has a higher-rank type - the first forall a. is inside the parentheses. I kind of dislike documenting the type that way - it uses a as a type variable in two completely separate ways. But there are two different scopes, and that matters. What it's saying is that any function passed to it must be polymorphic over all instances of Data.

But the type of (* 2) doesn't match up there. It won't work with any instance of Data. It requires more - it requires that it be provided an instance of Num. So the error message dutifully reports that it can't deduce (Num a) from the context Data a. So this isn't going to work. The pieces don't fit together.

This is where mkT comes into play:

ghci> :t mkT
mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a

Its type is a bit funny. It looks almost like it does nothing at all, but Typeable is a funny class. mkT actually compares a and b for type equality, using those Typeable constraints. If they're the same, it applies the function you provided. Otherwise, it just acts as the identity function.

What it does when it's applied to a function is where things are going wrong for you:

ghci> :t mkT (* 2)
mkT (* 2) :: Typeable a => a -> a

It's still polymorphic in a, but the b it used to have has vanished. It had to pick a specific type b to work against, and it did that by defaulting to Integer. (See ghc's extended defaulting rules for details on how that works in ghci.) So...

ghci> mkT (* 2) 3.5
3.5
ghci> mkT (* 2) 7
14
ghci> mkT (* 2) (7 :: Int)
7

At the type level, mkT has to monomorphize its argument. That's the only way it can make use of the Typeable constraint when used in a context where a relevant variable no longer appears in its type.

(To tie the loop back to everywhere, the reason mkT (* 2) works as an argument to everywhere is because Data is a subclass of Typeable. The Data constraint implies that the Typeable requirement will be satisfied.)

So what can you do about this? Well, it's impossible to write it truly generically because of Haskell's open world assumption. Anywhere in the program, any type might be declared an instance of Num with arbitrary implementations of (*) and fromInteger. In order to work with everywhere, there would need to be some mechanism to go from knowing something is an instance of Data to looking up its Num instance. This just isn't possible at run time. Types have been erased. There may be some residues like Typeable dictionaries being carried around, but they don't provide any means to look up other instance dictionaries. And while you might be able to envision a language where that sort of lookup is possible, it actually would be very harmful to allow it in Haskell. It would invalidate the ability to reason about types parametrically, which would be a giant loss.

The best you can do is write transformation functions that work on multiple types:

ghci> let f = mkT (* (2 :: Int)) . mkT (* (2 :: Double)) . mkT (* (2 :: Integer))
ghci> f 5
10
ghci> f 2.7
5.4
ghci> f (9 :: Int)
18
ghci> f "hello"
"hello"

It's verbose and you can probably write something better by hand if you so desire. But it at least works, at least to some extent. And it doesn't require breaking foundational assumptions in the language design, which is always a bonus.