Understanding the Haskell type system in the context of applicatives

4
votes

I am playing with Control.Applicative and I am realizing I don't understand everything with the Haskell type system.

Here is my experiment in Ghci:

λ :t (<*>)
(<*>) :: Applicative f => f (a -> b) -> f a -> f b

λ :t (<*>) (pure 2)
(<*>) (pure 2) :: (Num (a -> b), Applicative f) => f a -> f b

The type of the first argument of <*> is f (a -> b).

  • Why is this expression correct?
  • How can it be unified with (pure 2) since the constant 2 is not of type a -> b?
  • What does Num (a -> b) mean? How can a function having a a -> b type be an instance of Num?
1
haskelltype-systemsapplicative
Num (a -> b) in the context doesn't mean there is a Num instance for a -> b. It means "if there were" a Num instance for a -> b then the expression would have this type. – Tom Ellis
In addition, the "constant" is a literal, and therefore has type 2 :: Num a => a. – Zeta
try next: :t (<*>) (pure (2 :: Int)) – viorior

1 Answers

7
votes

The first argument of <*> is supposed to be f (a -> b). So given (<*>) (pure x), this is well-typed provided that x is some kind of function.

The type of 2 is Num a => a. In other words, 2 can be any possible type, so long as it's an instance of Num.

So in your expression (<*>) (pure 2), this is well-typed provided that the type of 2 is a function type, and that function type has a Num instance.

Of course, there is almost no reason why you would ever want a function to have a Num instance. But the compiler doesn't know that. All it's saying is that if there was such an instance, then the expression would become well-typed.

(This is similar to the error you sometimes see where the compiler wants some type to be an instance of Integral and Fractional simultaneously. To a human, this is a nonsensical combination. To a machine, they're just two ordinary classes...)