Определение типа функции в функциональном программировании

Question

Следующие уравнения записаны в синтаксисе Miranda, но из-за сходства между Miranda и Haskell я ожидаю, что программисты на Haskell должны это понять!

Если вы определяете следующие функции:

rc v g i = g (v:i)
rn x = x
rh g = hd (g [])


f [] y = y 
f (x:xs) y = f xs (rc x y)

g [] y = y
g (x:xs) y = g xs (x:y)

Как вы определяете тип функций? Я думаю, что понимаю, как это сделать для f, g и rn, но я запутался в части частичного применения.

рн будет * -> * ( или что-нибудь -> что-нибудь, я думаю, что это -> a в Haskell? )

Для f и g оба типа функций являются [*] -> * -> *?

Я не уверен, как подходить к поиску типов для rc и rh. В rc g частично применяется к переменной i - так что я предполагаю, что это ограничивает тип i как [*]. В каком порядке rc и g применяются в определении rc? Применяется ли g к i, а затем результирующая функция используется в качестве аргумента для rc? Или rc принимает 3 отдельных параметра v, g и i? Я действительно смущен .. любая помощь будет оценена! Спасибо, ребята.

Извините, забыл добавить, что hd является стандартной функцией заголовка для списка и определяется как:

hd :: [*] -> *
hd (a:x) = a
hd [] = error "hd []"

Answer 1

Я собираюсь использовать синтаксис haskell для записи типов.

rc v g i = g (v:i)

Здесь rc принимает три параметра, поэтому его тип будет примерно таким: a -> b -> c -> d. v:i должен быть списком элементов того же типа, что и v и i, поэтому v :: a и i :: [a]. g применяется к этому списку, так что g :: [a] -> d. Если вы сложите все вместе, вы получите rc :: a -> ([a] -> d) -> [a] -> d.

Как вы уже поняли rn :: a -> a, потому что это просто личность.

Я понятия не имею о типе функции hd, которую вы используете в rh, поэтому я пропущу это.

f [] y = y 
f (x:xs) y = f xs (rc x y)

Здесь f принимает два параметра, поэтому его тип будет примерно таким: a -> b -> c. Из первого случая мы можем вывести это b == c, так как мы возвращаем y, и что первый аргумент является списком. Пока мы знаем, что f :: [a'] -> b -> b. Во втором случае обратите внимание, как x и y вводятся во входные данные для rc: y должно быть функцией [a'] -> d и rc x y :: a' -> d (это также должен быть тип y, поскольку он передается как второй аргумент f). Наконец, мы можем сказать, что f :: [a'] -> ([a'] -> d) -> ([a'] -> d). Поскольку -> является ассоциативным справа, это эквивалентно [a'] -> ([a'] -> d) -> [a'] -> d.

Вы можете рассуждать таким же образом и для остальных.

Answer 2

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

Давайте начнем с верха,

rc v g i = g (v : i)

так rc :: a -> b -> c -> d и мы должны увидеть, что можно узнать о a, b, c и d. С правой стороны появляется (v : i), поэтому с v :: a мы видим, что i :: [a], c = [a]. Затем g применяется к v : i, поэтому g :: [a] -> d, в целом,

rc :: a -> ([a] -> d) -> [a] -> d

rn x = x означает, что нет никаких ограничений на тип аргумента rn, и его тип возврата такой же, rn :: a -> a.

rh g = hd (g [])

Поскольку аргумент rh g применяется к пустому списку в RHS, он должен иметь тип [a] -> b, возможно, дополнительная информация о a или b приведена ниже. Действительно, g [] является аргументом hd на RHS, поэтому g [] :: [c] и g :: [a] -> [c], следовательно,

rh :: ([a] -> [c]) -> c

Далее

f [] y = y 
f (x:xs) y = f xs (rc x y)

Первый аргумент является списком, и если он пуст, результатом является второй аргумент, поэтому f :: [a] -> b -> b следует из первого уравнения. Теперь во втором уравнении RHS второй аргумент f равен rc x y, следовательно, rc x y должен иметь тот же тип, что и y, мы назвали его b. Но

rc :: a -> ([a] -> d) -> [a] -> d

, значит b = [a] -> d. Следовательно

f :: [a] -> ([a] -> d) -> [a] -> d

Наконец

g [] y = y
g (x:xs) y = g xs (x:y)

из первого уравнения мы выводим g :: [a] -> b -> b. Из второго мы выводим b = [a], так как мы берем голову первого аргумента g и выводим его во второй, таким образом

g :: [a] -> [a] -> [a]