Type of fun g x = ys where ys = [x] ++ filter (cur

问题:

I'm trying to understand why the type of fun g x = ys where ys = [x] ++ filter (curry g x) ys is ((a, a) -> Bool) -> a -> [a].

I understand that:

filter :: (a -> Bool) -> [a] -> [a] and that curry :: ((a, b) -> c) -> a -> b -> c

But I don't understand how to continue.

回答1:

The approach below is not necessarily the easiest or fastest, but it's relatively systematic.

---

Strictly speaking, you're looking for the type of

\g -> (\ x -> let ys = (++) [x] (filter (curry g x) ys) in ys)

(let and where are equivalent, but it's sometimes a little easier to reason using let), given the types

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

Don't forget that you're also using

(++) :: [a] -> [a] -> [a]

Let's first look at the 'deepest' part of the syntax tree:

curry g x

We have g and x, of which we haven't seen before yet, so we'll assume that they have some type:

g :: t1
x :: t2

We also have curry. At every point where these functions occur, the type variables (a, b, c) can be specialized differently, so it's a good idea to replace them with a fresh name every time you use these functions. At this point, curry has the following type:

curry :: ((a1, b1) -> c1) -> a1 -> b1 -> c1

We can then only say curry g x if the following types can be unified:

t1  ~  ((a1, b1) -> c1)       -- because we apply curry to g
t2  ~  a1                     -- because we apply (curry g) to x

It's then also safe to assume that

g :: ((a1, b1) -> c1)
x :: a1
---
curry g x :: b1 -> c1

Let's continue:

filter (curry g x) ys

We see ys for the first time, so let's keep it at ys :: t3 for now. We also have to instantiate filter. So at this point, we know

filter :: (a2 -> Bool) -> [a2] -> [a2]
ys :: t3

Now we must match the types of filter's arguments:

b1 -> c1  ~  a2 -> Bool
t3        ~  [a2]

The first constraint can be broken down to

b1  ~  a2
c1  ~  Bool

We now know the following:

g :: ((a1, a2) -> Bool)
x :: a1
ys :: [a2]
---
filter (curry g x) ys :: [a2]

Let's continue.

(++) [x] (filter (curry g x) ys)

I won't spend too much time on explaining [x] :: [a1], let's see the type of (++):

(++) :: [a3] -> [a3] -> [a3]

We get the following constraints:

[a1]  ~  [a3]           -- [x]
[a2]  ~  [a3]           -- filter (curry g x) ys

Since these constraints can be reduced to

a1  ~  a3
a2  ~  a2

we'll just call all these a's a1:

g :: ((a1, a1) -> Bool)
x :: a1
ys :: [a1]
---
(++) [x] (filter (curry g x) ys) :: [a1]

For now, I'll ignore that ys' type gets generalized, and focus on

\x -> let { {- ... -} } in ys

We know what type we need for x, and we know the type of ys, so we now know

g :: ((a1, a1) -> Bool)
ys :: [a1]
---
(\x -> let { {- ... -} } in ys) :: a1 -> [a1]

In a similar fashion, we can conclude that

(\g -> (\x -> let { {- ... -} } in ys)) :: ((a1, a1) -> Bool) -> a1 -> [a1]

At this point, you only have to rename (actually, generalize, because you want to bind it to fun) the type variables and you have your answer.

回答2:

We can derive types in Haskell in a more or less mechanical manner, using the general scheme of

foo      x =  y                              -- is the same as
foo   = \x -> y                              -- so the types are
foo   :: a -> b          , x :: a , y :: b   -- so that
foo      x :: b                              

which means that e.g.

f    x    y    z :: d    , x :: a , y :: b, z :: c

entails

f    x    y :: c -> d
f    x :: b -> c -> d
f :: a -> b -> c -> d

etc. With these simple tricks type derivation will become trivial for you. Here, with

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

we simply write down the stuff carefully lined up, processing it in a top-down manner, consistently renaming and substituting the type variables, and recording the type equivalences on the side:

fun    g    x = ys   where   ys = [x] ++ filter (curry g x) ys 
fun    g    x :: c              , ys :: c
fun    g :: b -> c              , x  :: b 
fun :: a -> b -> c              , g  :: a 

ys = [x] ++ filter (curry g x) ys
c  ~  c

(++)    [x]     (filter (curry g x) ys) :: c    
(++) :: [a1] -> [a1]                    -> [a1]   
-----------------------------------------------
(++) :: [b]  -> [b]                     -> [b]    , a1 ~ b , c ~ [b]

filter    (curry g x )     ys  :: [b] 
filter :: (a2 -> Bool) -> [a2] -> [a2]            , a2 ~ b
--------------------------------------
filter :: (b  -> Bool) -> [b]  -> [b]

curry     g                   x  :: b -> Bool
curry :: ((a3, b) -> c3  ) -> a3 -> b -> c3       , c3 ~ Bool , a3 ~ b
-------------------------------------------
curry :: ((b , b) -> Bool) -> b  -> b -> Bool     , a ~ ((b,b) -> Bool)

so we have that a ~ ((b,b) -> Bool) and c ~ [b], and thus

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

which is the same as ((a,a) -> Bool) -> a -> [a], up to a consistent renaming of type variables.