Type fun gx = ys, where ys = [x] ++ filter (curry gx) ys?

Question

I am trying to understand why the type fun gx = ys where ys = [x] ++ filter (curry gx) 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 do not understand how to proceed.

Answer 1

The approach below is not always the easiest or fastest, but it is relatively systematic.

---

Strictly speaking, you are looking for type

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

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

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

Do not forget that you also use

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

First, consider the “deepest” part of the syntax tree:

 curry gx 

We have g and x , which we have not yet seen, so suppose they are of some type:

 g :: t1 x :: t2 

We also have curry . At each point where these functions occur, variables of type ( a , b , c ) can be specialized in different ways, so it is recommended that you replace them with a new name each time you use these functions. At this point, curry is of the following type:

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

We can then say only curry gx 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 

Then it can also be safely assumed that

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

Continue:

 filter (curry gx) ys 

We see ys for the first time, so let's save it to ys :: t3 . We also need to create a filter instance. So, at the moment, we know

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

Now we must match the filter argument types:

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

The first restriction can be broken down into

 b1 ~ a2 c1 ~ Bool 

Now we know the following:

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

Let's continue.

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

I will not spend too much time explaining [x] :: [a1] by looking at type (++) :

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

We get the following restrictions:

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

Since these restrictions can be reduced to

 a1 ~ a3 a2 ~ a2 

we just call it all a a1 :

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

For the time being, I will ignore that ys ' type is generalized and focuses 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] 

Similarly, we can conclude that

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

At this point, you only need to rename (in fact, generalize, because you want to bind it to fun ) type variables, and you have your own answer.

Answer 2

We can derive types in Haskell more or less mechanically, using a common scheme

 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 for example

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

entails

 fxy :: c -> d fx :: b -> c -> d f :: a -> b -> c -> d 

etc .. With these simple tricks, the type of derivation will become trivial for you. Here at

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

we simply write down the material, carefully arranged, processing it from top to bottom, sequentially renaming and replacing type variables and writing type equivalents to the side:

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

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

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

 filter (curry gx) 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) 

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

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

which coincides with ((a,a) -> Bool) -> a -> [a] , right up to the sequential renaming of type variables.