Ручной вывод типа для `f1 x xs = (filter . (<)) X xs`

Question

Я хочу вручную получить тип:

f1 x xs = (filter . (<)) x xs

Первый раз мы видим x, так:

x :: t1

затем (<) имеет этот тип:

(<) :: Ord a1 => a1 -> a1 -> Bool

Мы можем только сказать (< x) если следующие типы могут быть объединены:

t1  ~  a1

затем

x :: a1

Так

(<x) :: Ord a1 => a1 -> Bool

Фильтр имеет этот тип

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

Первый раз, чтобы увидеть хз, так:

xs :: t2

Мы можем только сказать (filter . (<)) x xs если следующие типы могут быть объединены:

a1 -> Bool ~ a2 -> Bool
t2  ~ [a2]

Итак, я понял f1 :: (a2 -> Bool) -> [a2] -> [a2]того же типа, что и filterкогда правильный тип Ord a => a -> [a] -> [a] (спрашивая GHCi).

Любая помощь?

Answer 1

Ограничение

a1 -> Bool ~ a2 -> Bool

может быть разбит на

a1 ~ a2

и, очевидно, правда

Bool ~ Bool

Так что у тебя есть a1 ~ a2, Вы уже знаете, что x является a1, xs является [a2] и, благодаря filterтип результата [a2], Таким образом, вы в конечном итоге:

f1 :: Ord a2 => a2 -> [a2] -> [a2]

(Не забывайте ограничение класса a1 получил от (<).)

Answer 2

Мы можем обрабатывать данные выражения сверху вниз. Таким образом, нет необходимости угадывать, что и где происходит, деривация происходит чисто механически, с минимальным количеством ошибок:

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]

Еще один способ решения этой проблемы состоит в том, чтобы заметить, что сокращение eta может быть выполнено там в определении 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]

Конечно, мы используем правильную ассоциативность стрелок в типах: a -> b -> c на самом деле a -> (b -> c),

Мы также используем общую схему для вывода типов

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