Полиморфный тип функций как параметр в haskell?

Question

Я пытаюсь определить полиморфный тип следующей функции:

flip f x y = f y x

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

1. 1-й параметр flip, f принимает два аргумента так (t1 -> t2 -> t3)

2. 2-й параметр flip, x имеет тип t1 из-за параметра t1 внутри f функция.

3. 3-й параметр flip, y который имеет тип t3 из-за параметра t3 внутри f функция.

4. Я не знаю полиморфный тип общего возврата.

Но когда я проверил тип в ghci, я получил:

flip :: (t2 -> t1 -> t) -> t1 -> t2 -> t

Может кто-нибудь, пожалуйста, помогите пройти через этот пример к тому, что здесь происходит?

Спасибо

Answer 1

Ваше второе предположение неверно:

2-й параметр переворота, x имеет тип t1 из-за параметра t1 внутри функции f.

Давайте сначала проанализируем функцию:

flip f x y = f y x

Мы видим, что flip имеет три аргумента в голову. Итак, мы сначала делаем тип:

flip :: a -> (b -> (c -> d))

Теперь мы, конечно, стремимся заполнить типы. С:

f :: a
x :: b
y :: c
flip f x y :: d

Мы видим с правой стороны:

(f y) x

Так что это означает, что f это функция, которая принимает в качестве входных данных y, Так что это означает, что a тот же тип, что и c -> e (или короче a ~ c -> e).

А сейчас:

flip :: (c -> e) -> (b -> (c -> d))
f :: (c -> e)
x :: b
y :: c

Кроме того, мы видим, что:

(f x) y

Итак, результат (f x) это другая функция, с вводом y, Так что это означает, что e ~ b -> f, Таким образом:

flip :: (c -> (b -> f)) -> (b -> (c -> d))
f :: c -> (b -> f)
x :: b
y :: c

Наконец мы видим, что (f y) x является результатом flip f x y, Так что это означает, что тип результата (f y) x тот же тип, что и d, Так что это означает, что f ~ d, Что означает, что:

flip :: (c -> (b -> d)) -> (b -> (c -> d))

Или если мы уберем несколько лишних скобок:

flip :: (c -> b -> d) -> b -> c -> d

Answer 2

Это просто вопрос решения системы уравнений. Сначала назначьте неизвестные типы:

f : a1
x : a2
y : a3

Следующий, f применяется к y, Так, f должен быть типом функции с аргументом того же типа, что и у, то есть

f : a1 = a3 -> a4
f y : a4

, подобным образом, f y применяется к x, так

f y : a4 = a2 -> a5
f y x : a5

Подставляя это обратно, получаем

f : a3 -> a2 -> a5
x : a2
y : a3

Мы можем переименовать эти типы

t2 = a3
t1 = a2
t  = a5

и получить

f : t2 -> t1 -> t
x : t1
y : t2

Тело функции f y x, который имеет тип t = a5,