We can process given expressions in a top-down manner. This way there's no need to guess what goes where, the derivation happens purely mechanically, with minimal room for error:
f1 x xs = (filter . (<)) x xs
f1 x xs :: c (filter . (<)) x xs :: c
f1 x :: b -> c xs :: b
f1 :: a -> b -> c x :: a
(filter . (<)) x xs :: c
filter ((<) x) :: b -> c c ~ [d] , b ~ [d]
filter :: (d->Bool) -> [d] -> [d] (<) x :: d -> Bool
(<) :: (Ord a) => a -> a -> Bool
(<) x :: d -> Bool a ~ d , (Ord a)
f1 :: (Ord a) => a -> [a] -> [a]
Another way to tackle this is to notice that eta reduction can be performed there in the definition of f1
:
f1 x xs = (filter . (<)) x xs
f1 = (.) filter (<)
(.) :: ( b -> c ) -> ( a -> b ) -> (a->c)
(.) filter (<) :: t1
(.) :: ((d->Bool) -> ([d]->[d])) -> ((Ord a) => a -> (a->Bool)) -> t1
b ~ d -> Bool , c ~ [d] -> [d] , t1 ~ a -> c , (Ord a)
b ~ a -> Bool
-------------
d ~ a
f1 :: t1 ~ (Ord a) => a -> c
~ (Ord a) => a -> [d] -> [d]
~ (Ord a) => a -> [a] -> [a]
Of course we use the right associativity of arrows in types: a -> b -> c
is actually a -> (b -> c)
.
We also use a general scheme for type derivations
f x y z :: d
f x y :: c -> d , z :: c
f x :: b -> c -> d , y :: b
f :: a -> b -> c -> d , x :: a