문제

I'm trying to understand why the function

map (filter fst)

has the type

[[(Bool, a)]] -> [[(Bool, a)]]

How can "filter fst" work if filter must receive a function which returns a Bool-Type and fst just returns the first element of a tuple?

filter :: (a -> Bool) -> [a] -> [a]
fst :: (a, b) -> a

Can anyone explains me? Thanks ;)

도움이 되었습니까?

해결책

How can "filter fst" work if filter must receive a function which returns a Bool-Type and fst just returns the first element of a tuple?

In a sense, you've answered your own question! Let's break it down:

filter must receive a function which returns a Bool-Type

OK, so let's look at what you're passing it: fst. Is fst a function? Yes, it is, so we've got the first part down. Does it return a Bool? Well, let's look at what it does:

fst just returns the first element of a tuple

So if the first element of a tuple is a Bool, then yes, it does return a bool! If the first element of a tuple is anything other than a Bool, though, it doesn't and will fail the typecheck.

Let's have another look at the types you put up. I'm going to change the names of the type variables just to make things clearer:

filter :: (a -> Bool) -> [a] -> [a]
fst :: (b, c) -> b

fst takes an (b, c) and returns an b, and filter is expecting a function which takes an a and returns a Bool. We are passing in fst, so the a above must be (b, c) as that's the first parameter of fst. The return value of the function we pass into filter must be a Bool, so b above must therefore be a Bool. And c can be anything, because it's not used by filter at all. Substituting the values for a and b gives us a final type for filter fst of:

filter fst :: [(Bool, c)] -> [(Bool, c)]

Finally, the type of map is:

map :: (d -> e) -> [d] -> [e]

(Again, I've renamed the type variables here, just to differentiate them from the ones we've used above, but remember it doesn't actually matter what they're called so long as they're consistent within the scope of the type annotation)

map (filter fst) passes the filter fst we defined above as the first parameter to map. Substituting the parameter for d and the result for e we can see this function must be [(Bool, c)] -> [(Bool, c)], in other words both d and e are (Bool, c). Plugging those into the function we arrive at the final type:

map (filter fst) :: [[(Bool, c)]] -> [[(Bool, c)]]

다른 팁

fst is a function that returns a boolean as long as you restrict the tuples to have a Boolean as their first element (the second element can be anything, hence the (Bool, a)

:t filter    -- (a -> Bool) -> [a] -> [a]
:t fst       -- (a,b) -> a

But, we could also exchange type variables for fst to get:

:t fst       -- (c,b) -> c

So, the first argument of filter has type a -> Bool, while fst itself is (c,b) -> c. Now we try to combine this (I think this is called unification):

1st arg of filter:  a     -> Bool
fst:                (c,b) -> c

From this, we can infer that c must be Bool (since the right hand side has to be equal) and obtain:

1st arg of filter:  a        -> Bool
fst:                (Bool,b) -> Bool

From the above, we infer that a must be (Bool,b), and obtain:

1st arg of filter:  (Bool,b) -> Bool
fst:                (Bool,b) -> Bool

And we are done.

Since I already wrote this down before danielpwright's answer was posted, I post it anyway. I'm just going through my thought process for the type of filter fst here.

First, write down the type signatures (change fst so that its type variable names don't clash with those of filter):

filter :: (a -> Bool) -> [a] -> [a]
fst :: (b, c) -> b

Match (a -> Bool) with ((b, c) -> b) :

b has to be Bool, which means that a has to be (Bool,c)

By specializing filter with this information it becomes:

filter :: ((Bool,c) -> Bool) -> [(Bool,c)] -> [(Bool,c)]

which leads to

filter fst :: [(Bool, c)] -> [(Bool, c)]

You really just have to solve some type equations. Let's start:

 filter :: (a -> Bool) -> [a] -> [a]
 fst    :: (b, c) -> b

Therefore, filter fst :: [a] -> [a] where a is the solution of the following type equation:

 a -> Bool = (b, c) -> b

which implies

 a    = (b, c)
 Bool = b

which implies

 a = (Bool, c)

Therefore, filter fst :: [(Bool, c)] -> [(Bool, c)].

Now we have:

map        :: (a -> b) -> [a] -> [b]
filter fst :: [(Bool, c)] -> [(Bool, c)]

So, map (filter fst) :: [a] -> [b] where a and b are given by the following type equation:

a -> b = [(Bool, c)] -> [(Bool, c)]

which implies

a = [(Bool, c)]
b = [(Bool, c)]

Therefore, map (filter fst) :: [[(Bool, c)]] -> [[(Bool, c)]].

As others have done, I want to solve the type equations here; but I want to write them down in a more visual way, so the derivation can be performed in a more automatic way. Let's see.

filter :: (  a   -> Bool) -> [a] -> [a]
fst    ::  (c,d) -> c              -- always use unique type var names, 
------------------------           --   rename freely but consistently
filter fst :: [a] -> [a],    a -> Bool  ~  (c,d) -> c
                             a ~ (c,d)  ,  Bool ~ c
                             a ~ (Bool,d)
           ---------------------------
           :: [(Bool,d)] -> [(Bool,d)]

Purely mechanical stuff. :) With this,

map        :: (     a     ->     b     ) -> [a] -> [b]
filter fst ::  [(Bool,d)] -> [(Bool,d)]
------------------------------
map (filter fst) :: [a] -> [b],     a ~ [(Bool,d)]  ,  b ~ [(Bool,d)]
                 -------------------------------
                 :: [[(Bool,d)]] -> [[(Bool,d)]]

The type variables in the final type can be freely renamed for readability (in a consistent manner of course).

The only thing that my answer adds to what was already shown in other answers here, is this advice (which I think important): if you follow this simple discipline of writing down one thing below the other, it becomes very easy to perform these type unifications in very mechanical, automatic manner (thus reducing possibility of error).

For another example of this, including an actual type-deriving Prolog program, see Haskell: how to infer the type of an expression manually.

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 StackOverflow
scroll top