I am doing Nicta course exercises and there I ran into an example that I don't understand. I have two functions and their types are as follows:
filtering :: Applicative f => (a -> f Bool) -> List a -> f (List a)
(>) :: Ord a => a -> a -> Bool
Then I apply filtering to (>) and check the type is GHCi. the resulting type is :
filtering (>) :: Ord a => List a -> a -> List a
I don't understand how this result came about.
To understand what the expression filtering (>) means, you should know which instance of Applicative is used here.
Actually, the instance Applicative ((->) a) is used here, which specializes the function filtering to the following type (notice that we use (b ->) instead of ((->) a) below, which is the same)
filtering :: (a -> (b -> Bool)) -> List a -> (b -> (List a))
And when applied (>), to unify (a -> (b -> Bool)) and (a -> (a -> Bool)), we know that b must equal to a, so filtering is specialized to
filtering :: (a -> (a -> Bool)) -> List a -> (a -> (List a))
And so we get the type of filtering (>) directly
filtering (>) :: (Ord a) => List a -> (a -> (List a))
which is just same as what GHCi is given.
The compiler tries unify two types: a -> (a -> Bool) with b -> f Bool. It sees that lhs and rhs are functions. So, it tries unify a = b and a -> Bool = f Bool. The a = b is unified. The a -> Bool equivalent with (->) a Bool. So, from (->) a Bool = f Bool it gets that f = (->) a. And if we apply the substitute f = (->) a to type expression List a -> f (List a) we'll get: List a -> (->) a (List a) which equivalent with List a -> a -> List a
