Тип веселья g x = ys, где ys = [x] ++ filter (curry g x) ys?

Question

Я пытаюсь понять, почему тип fun g x = ys where ys = [x] ++ filter (curry g x) ys является ((a, a) -> Bool) -> a -> [a],

Я это понимаю:

filter :: (a -> Bool) -> [a] -> [a] и это curry :: ((a, b) -> c) -> a -> b -> c

Но я не понимаю, как продолжить.

Answer 1

Подход, приведенный ниже, не обязательно самый простой или быстрый, но он относительно систематический.

---

Строго говоря, вы ищете тип

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

(let а также where эквивалентны, но иногда немного проще рассуждать, используя let), учитывая типы

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

Не забывайте, что вы также используете

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

Давайте сначала посмотрим на "самую глубокую" часть синтаксического дерева:

curry g x

У нас есть g а также xкоторого мы еще не видели, поэтому предположим, что они имеют некоторый тип:

g :: t1
x :: t2

У нас также есть curry, В каждой точке, где эти функции встречаются, переменные типа (a, b, c) могут быть специализированы по-разному, поэтому рекомендуется заменять их новым именем каждый раз, когда вы используете эти функции. С этой точки зрения, curry имеет следующий тип:

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

Тогда мы можем только сказать curry g x если следующие типы могут быть объединены:

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

Тогда также можно предположить, что

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

Давай продолжим:

filter (curry g x) ys

Мы видим ys в первый раз, так что давайте держать его на ys :: t3 теперь. Мы также должны создать экземпляр filter, Итак, на данный момент мы знаем

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

Теперь мы должны соответствовать типам filterаргументы:

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

Первое ограничение может быть разбито на

b1  ~  a2
c1  ~  Bool

Теперь мы знаем следующее:

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

Давай продолжим.

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

Я не буду тратить слишком много времени на объяснения [x] :: [a1]давайте посмотрим тип (++):

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

Мы получаем следующие ограничения:

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

Поскольку эти ограничения могут быть уменьшены до

a1  ~  a3
a2  ~  a2

мы просто назовем все это a"s a1:

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

Сейчас я буду игнорировать это ysтип становится обобщенным, и сосредоточиться на

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

Мы знаем, какой тип нам нужен xи мы знаем тип ysИтак, теперь мы знаем

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

Аналогичным образом, мы можем сделать вывод, что

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

На этом этапе вам нужно только переименовать (на самом деле, обобщить, потому что вы хотите связать его с fun) переменные типа, и у вас есть свой ответ.

Answer 2

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

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                              

это означает, что, например,

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

влечет за собой

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

и т. д. С помощью этих простых трюков вывод типов станет для вас тривиальным. Здесь, с

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

мы просто записываем материал, тщательно выстроенный в линию, обрабатывая его сверху вниз, последовательно переименовывая и подставляя переменные типа, и записывая эквивалентности типов на стороне:

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 gx) ys
с

(++) [x] (фильтр (карри gx) ys):: c    
(++):: [a1] -> [a1] -> [a1]   
-----------------------------------------------
(++):: [b] -> [b] -> [b], a1 ~ b, c ~ [b]

фильтр (карри gx) ys:: [b] 
фильтр:: (a2 -> Bool) -> [a2] -> [a2], a2 ~ b
--------------------------------------
фильтр:: (b -> Bool) -> [b] -> [b]

карри г х:: б -> Bool
карри:: ((a3, b) -> c3) -> a3 -> b -> c3, c3 ~ Bool, a3 ~ b
-------------------------------------------
карри:: ((b, b) -> Bool) -> b -> b -> Bool, a ~ ((b, b) -> Bool) 

так что мы имеем a ~ ((b,b) -> Bool) а также c ~ [b], и поэтому

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

который так же, как ((a,a) -> Bool) -> a -> [a], вплоть до согласованного переименования переменных типа.