Haskell: trying to understand the type of fmap (+) (1)

Question

i am trying to understand why there is no type error for fmap (+) (1)

I do understand the following sequence:

Prelude> :t  fmap 
fmap :: Functor f => (a -> b) -> f a -> f b
Prelude> :t  (+)  
(+) :: Num a => a -> a -> a                          # like a-> b with b = a -> a
Prelude> :t  fmap (+)
fmap (+) :: (Functor f, Num a) => f a -> f (a -> a)
Prelude> :t  fmap (+) (Just 1)                       
fmap (+) (Just 1) :: Num a => Maybe (a -> a)         # f=Maybe is implied by the Just constructor
Prelude>

I expected a type error for fmap (+) (1) since there is no functor implied for (1), instead i get:

Prelude> :t (1)
(1) :: Num p => p
Prelude> :t  (+)  
(+) :: Num a => a -> a -> a                          
Prelude> :t  fmap (+)
fmap (+) :: (Functor f, Num a) => f a -> f (a -> a)
Prelude> :t  fmap (+) (1)
fmap (+) (1) :: (Functor f, Num a, Num (f a)) => f (a -> a)  ## why ??
Prelude>

why is this ?

Similarly, i don't understand the type of fmap (+) id:

Prelude> :t  fmap (+)   
fmap (+) :: (Functor f, Num a) => f a -> f (a -> a)
Prelude> :t  id      
id :: a -> a
Prelude> :t  fmap (+) id
fmap (+) id :: Num a => a -> a -> a       ## why no error ?
Prelude>

Answer 1

Numerical literals can fit any type, provided it is a numeric type (in class Num).

GHC works under an open-world assumption, where even if a type does not belong to an instance right now, it might be in the future. This is because it is possible to write a new module and declare an instance there, and we want separate compilation.

For numeric types, this means that even if a type is not numeric right now, it might still be later on.

Suppose we write reverse 1. It looks wrong, since reverse expects a list, and 1 is not a list. Or is it? Even if [a] is not numeric now, it might be in the future, hence the type of reverse 1 is Num [a] => [a], and not a type error. Of course, under normal circumstances we won't have a Num [a] instance, but GHC can not assume that.

In your specific example, fmap wants an f a and you pass (1), which is the same as 1. Here, this numeric literal gets instantiated as Num (f a) => f a, so that type checking works.

fmap (+) (1) :: (Functor f, Num a, Num (f a)) => f (a -> a)

The above constraint Num (f a) is required to allow 1 to be interpreted in the type f a. Then f must be a functor because fmap requires it, and we must have Num a since (+) requires its argument to be numeric (the argument of (+) has type a and its result has type a -> a, where a must be numeric). We get f (a -> a) as a result again because of the return type of (+).

---

About fmap (+) id, this is simpler. Here id :: (->) a a, that is id :: f a where f = (->) a, which happens to be a functor. For this functor we have that fmap = (.), the functional composition operator. Hence, fmap (+) id means (.) (+) id, or (+) . id which is simply (+).

Answer 2

It's a simple consequence of the fact that number literals such as 1 are polymorphic - their type is (Num a) => a. In addition, there is no fixed list of numeric types, as Haskell allows you to make your own instances for any class - including Num - anywhere.

As a result, in applying this:

Prelude> :t  fmap (+)
fmap (+) :: (Functor f, Num a) => f a -> f (a -> a)

to the literal 1, the type checker only needs to check if it's possible to unify the type of 1 with the input type f a. Given the polymorphic type of 1 as above, this is clearly possible provided there is an instance of Num available for f a - as then f a is a valid type for 1. And this explains the final type.

As for fmap (+) id, this is rather different. Here GHC needs to unify f a (for a functor f and numeric a) with a -> a, which results in the only possible choice for f, the "function functor" ((->) a) (where fmap is just composition). That is f b here means a -> b, and so f (a -> a) is a -> a -> a.