Generic type of (map . filter)-CodePudding

I don't understand why map . filter generic type is map . filter :: (a -> Bool) -> [[a]] -> [[a]].

I know that map and filter types are map :: (a -> b) -> [a] -> [b] and filter :: (a -> Bool) -> [a] -> [a]. And also (.) :: (b -> c) -> (a -> b) -> a -> c.

So my guess was that a = (a -> Bool) -> [a], b = [a] and since the output of filter is not a function, I thought that map . filter would return a function that expect a function (a -> b).

I don't understand why the type is a list of lists of a, since neither map nor filter has a list of lists. I also don't understand why it works with just one function since both need one.

Can someone explain how does it work, please?

CodePudding user response：

First, lets use different letters for the types in the functions. That way we won't get confused.

map :: (a -> b) -> [a] -> [b]
filter :: (c -> Bool) -> [c] -> [c]
(.) :: (e -> f) -> (d -> e) -> d -> f

So now we consider map . filter. Doing the substitution we get the following (~ is used for type equality):

d ~ (c -> Bool)
e ~ ([c] -> [c])   -- Result of 'filter'
e ~ (a -> b)       -- Argument of 'map'
f ~ ([a] -> [b])

Notice how we get two types for e. By substitution,

a ~ b ~ [c]

So therefore

f ~ ([[c]] -> [[c])

And so we can substitute for d and f in the definition of (.) and get

(c -> Bool) -> [[c]] -> [[c]]

Which is what GHCi was telling us.

What this function actually does is apply the filter to each sublist; the function argument taken by map is the filter. So in GHCi,

Prelude> import Data.Char
Prelude Data.Char> (map.filter) isDigit ["foo123", "456bar"]
["123","456"]

CodePudding user response：

The type of (.),

(.) :: (b -> c) -> (a -> b) -> a -> c
 --       f     .     g     :: a -> c    when g :: a->b, f :: b->c

means that

    g :: a -> b
f     ::      t -> c
--------------------   , b ~ t
f . g :: a ->      c

Then following this same schema we get right away that

      filter :: (a->Bool) -> ([a] -> [a])
map          ::              ( s  ->  t ) -> [ s ] -> [ t ]
----------------------------------------------------------- 
                           s ~ [a]   t ~ [a]
----------------------------------------------------------- 
map . filter :: (a->Bool) ->                 [[a]] -> [[a]]

It makes sense, too. (map . filter) p = map (filter p), so this map applies filter p to each element of a list (as maps do).

Since p :: a -> Bool, then filter p :: [a] -> [a].

Since this function is applied to each element of a list, this means that each element of that list has the type [a], and is transformed to another [a].

Thus the whole list was [[a]], and the result of the transformation is also [[a]].