Полиморфные типы в Хаскеле

Question

Я наткнулся на эту функцию

iter p f x = if (p x) then x else (iter p f (f x))

и я решил попробовать определить полиморфные типы самостоятельно, чтобы понять концепцию.

Моя мысль была следующей:

Функция принимает 3 параметра, поэтому мы имеем t1 -> t2 -> t3 -> T

1. p используется внутри условия if, поэтому он должен возвращать bool, следовательно t1 = a -> Bool

2. f также тот же тип, что и p потому что он передается в качестве аргумента в блоке else, поэтому t2 = a -> Bool

3. x используется внутри условия if, поэтому он должен возвращать bool, поэтому t1 = a -> Bool

Но когда я проверил тип в ghci, мне дали тип

iter :: (t -> Bool) -> (t -> t) -> t -> t

Может кто-нибудь, пожалуйста, объясните причину этого.

Спасибо

Answer 1

Функция принимает 3 параметра, поэтому мы имеем t1 -> t2 -> t3 -> T

Это правильно в качестве отправной точки.

p используется внутри условия if, поэтому он должен возвращать bool, поэтому t1 = a -> Bool

Правильный.

f также тот же тип, что и p, поскольку он передается в качестве аргумента в блоке else, поэтому t2 = a -> Bool

Неправильно. f никогда не используется так же, как p, В блоке else f применяется к x и результат передан в качестве последнего аргумента iter, Из того, что мы знаем f x должен быть того же типа, что и x так f :: a -> a,

x используется внутри условия if, поэтому он должен возвращать bool, поэтому t1 = a -> Bool

Неправильно. В случае если x используется только в качестве аргумента p, Вы установили выше p :: a -> Bool, Следовательно x :: a,

Но когда я проверил тип в ghci, мне дали тип

iter:: (t -> Bool) -> (t -> t) -> t -> t

Правильный. Вы также можете написать эту замену t с a чтобы быть последовательным в обозначениях - мы использовали a выше:

iter :: (a -> Bool) -> (a -> a) -> a -> a

Answer 2

Давайте оценим это снова:

iter p f x = if (p x) then x else (iter p f (f x))

iter принимает три параметра (технически говоря, каждая функция принимает один параметр, но давайте пропустим детали). Так что это действительно имеет тип t1 -> t2 -> t3 -> t,

Сейчас в if - then - else Заявление, мы видим (p x) это означает, что p x должен оценить до логического. Так что это означает, что:

t1 ~ t3 -> Bool

Далее мы видим x в then заявление. Это может показаться несущественным, но это так: это означает, что тип вывода t такой же, как у t3, так:

t3 ~ t

Теперь это означает, что мы уже получили, что iter имеет тип:

iter :: (t3 -> Bool) -> t2 -> t3 -> t3

Теперь мы видим в else Скажите звонок:

iter p f (f x)

Так что это означает, что f это функция f :: t4 -> t5, Так как это занимает x в качестве ввода его тип ввода должен быть t3 и так как результат (f x) передается iter функция (которая сама по себе не является той же "заземленной" iter функция). Итак, мы должны проверить звонок:

iter :: (u3 -> Bool) -> u2 -> u3 -> u3  -- call

Теперь, так как мы называем это с iter p f (f x) мы определенно знаем, что u3 ~ t3: так как p имеет тип t3 -> Bool, Таким образом, это основание в дальнейшем:

iter :: (t3 -> Bool) -> u2 -> t3 -> t3  -- call

Синус (f x) используется в качестве третьего аргумента, мы знаем, что тип результата f x должно быть t3 также. Так f имеет тип f :: t3 -> t3, Итак, мы заключаем, что iter имеет тип:

iter :: (t3 -> Bool) -> (t3 -> t3) -> t3 -> t3