Ручной вывод типа в Haskell

Question

Рассмотрим функцию

f g h x y = g (g x) (h y)

Каков ее тип?Очевидно, что я могу просто использовать :t f, чтобы выяснить это, но если мне нужно вывести это вручную, каков наилучший способ сделать это?

Метод, который мне показали, состоит в том, чтобы назначать типы параметрам и выводитьоттуда - например, x :: a, y :: b дает нам, что g :: a -> c и h :: b -> d для некоторых c, d (от g x, h y), а затем мы продолжаем делать выводы оттуда (c = a из g (g x) (h y) и т. Д.).

Однако это иногда просто превращается в огромный беспорядок, и часто я не уверен, как сделать дальнейшие выводы или сработать, когда я закончу.Иногда возникают другие проблемы - например, в этом случае x окажется функцией, но для меня это было неочевидно до обмана и поиска типа.

Есть ли конкретный алгоритм, который будетвсегда работать (и разумно ли для человека выполнить быстро)?Иначе есть какие-то эвристики или советы, которые мне не хватает?

Answer 1

Просто запишите все типы сущностей под ними:

f g h x y = g (g x)   (h y) 
                 x :: x  y :: y
                       h :: y -> a            , h y :: a
               g :: x -> b                    , g x :: b
            g    :: b -> (a -> t)             , x ~ b , b ~ (a -> t)
f :: (x -> b) -> (y -> a) -> x -> y -> t      , x ~ b , b ~ (a -> t)
f :: (b -> b) -> (y -> a) -> b -> y -> t      , b ~ (a -> t)
--       g           h       x    y

Таким образом f :: ((a -> t) -> (a -> t)) -> (y -> a) -> (a -> t) -> y -> t.Вот и все.

Действительно,

~> :t let f g h x y = g (g x) (h y) in f
    :: ((t1 -> t) -> t1 -> t) -> (t2 -> t1) -> (t1 -> t) -> t2 -> t

---

Это выглядит так:

1. x должен иметь некоторый тип, назовем его x: x :: x.
2. y должен иметь некоторый тип, назовем его y: y :: y.
3. h y должен иметь некоторый тип, назовем его a: h y :: a.следовательно, h :: y -> a.
4. g x должен иметь некоторый тип, назовем его b: g x :: b.следовательно, g :: x -> b.
5. g _ _ должен иметь некоторый тип, назовем его t.следовательно, g :: b -> a -> t.
   , что совпадает с g :: b -> (a -> t).
6. двумя типовыми сигнатурами для g, должны унифицировать , т.е. быть такими же при некоторой замене * Включено переменных типа, поскольку две сигнатуры описывают одну и ту же сущность, g.
   , таким образом, мы должны иметь x ~ b, b ~ (a -> t).Это подстановка.
7. Имея все типы аргументов для f, мы знаем, что она производит то, что производит g, то есть t.Таким образом, мы можем записать его тип, (x -> b) -> (y -> a) -> x -> y -> t.
8. Наконец, мы подставляем типы в соответствии с заменой, чтобы уменьшить количество задействованных переменных типа.Таким образом, мы подставляем b сначала x, а затем a -> t вместо b, каждый раз удаляя исключенную переменную типа из подстановки.
9. Когда подстановка пуста, мы ГОТОВЫ.

Конечно, мы могли бы сначала заменить b на x, заканчивая заменой x ~ (a -> t), а затем мы получили бы тот же тип в конце,, если мы всегда заменяем более простые типы на более сложные (например, заменяя b на (a -> t), а не наоборот).

Простые шаги, гарантированные результаты.

Answer 2

Ну, функция:

f g h x y = g (g x) (h y)

или более многословно:

f g h x y = (g (g x)) (h y)

По сути, мы предполагаем, что все четыре параметра (g, h, xи y) имеют разные типы.Мы также вводим тип вывода для нашей функции (здесь t):

g :: a
h :: b
x :: c
y :: d
f g h x y :: t

Но теперь мы собираемся выполнить некоторый вывод.Например, мы видим g x, так что это означает, что есть приложение функции с g функцией и x параметром.Это означает, что g является функцией с типом ввода c, поэтому мы переопределяем тип от g до:

g :: a ~ (c -> e)
h :: b
x :: c
y :: d
f g h x y :: t

(здесь тильда ~ означает, что два типато же самое, поэтому a совпадает с c -> e)).

Так как g имеет тип g :: c -> e, а x имеет тип c, это означает, что результатприложение функции g x имеет тип g x :: e.

Мы видим другое приложение функции, g как функцию и g x как аргумент.Таким образом, это означает, что тип ввода g (который c) должен быть равен типу g x (который e), следовательно, мы знаем, что c ~ e, поэтому типы теперь:

     c ~ e
g :: a ~ (c -> c)
h :: b
x :: c
y :: d
f g h x y :: t

Теперь мы видим приложение функции с h функцией и y аргументом.Это означает, что h является функцией, а тип ввода совпадает с типом y :: d, поэтому h имеет тип d -> f, что означает:

     c ~ e
g :: a ~ (c -> c)
h :: b ~ (d -> f)
x :: c
y :: d
f g h x y :: t

наконецмы видим приложение функции с g (g x) функцией и h y аргументом, так что это означает, что тип выходного значения g (g x) :: c должен быть функцией, с f в качестве типа ввода и t в качестве типа вывода, так что это означает, что c ~ (f -> t), и, следовательно:

     c ~ e
     c ~ (f -> t)
g :: a ~ (c -> c) ~ ((f -> t) -> (f -> t))
h :: b ~ (d -> f)
x :: (f -> t)
y :: d
f g h x y :: t

Так что это означает, что, поскольку f имеет эти параметры g, h, x и y, типиз f это:

f :: ((f -> t) -> (f -> t)) -> (d -> f) -> (f -> t) -> d -> t
--   \_________ __________/    \__ ___/    \__ ___/    |
--             v                  v           v        |
--             g                  h           x        y

Answer 3

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

x :: a
y :: b
g :: a -> b    -- from g x
h :: c -> d    -- from h y
a ~ b          -- from g (g x)

Мы знаем, что a и b одинаковы, потому что мы передали g x, b, g, что предполагает a.Итак, теперь мы заменяем все b на a и продолжаем, пока не рассмотрим все подвыражения ...

Что касается вашего комментария "огромного беспорядка", у меня есть пара слов, которые нужно сказать:

1. Это способ сделать это.Если это слишком сложно, вам просто нужно попрактиковаться , и это станет легче.Вы начнете развивать интуицию, и это станет легче.
2. Эта конкретная функция не из легких.Я программирую на Haskell в течение 12 лет, и мне все еще нужно пройти алгоритм объединения на бумаге для этого.Тот факт, что это настолько абстрактно, не помогает - если бы я знал, для чего предназначалась эта функция, это было бы намного проще.

Answer 4

Давайте проверим функцию на верхнем уровне:

f g h x y = g (g x) (h y)

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

Во-первых, давайте назначим тип верхнему выражению.Давайте назовем это a:

g (g x) (h y) :: a

Давайте возьмем первый аргумент и назначим типы соответственно:

-- 'expanding'  (g (g x)) (h y) :: a
h y :: b
g (g x) :: b -> a

И снова

-- 'expanding' g (g x) :: b -> a
g x :: c
g :: c -> b -> a

И снова

-- 'expanding' g x :: c
x :: d
g :: d -> c

Но держись: теперь у нас есть это g :: c -> b -> a и это g :: d -> c.Итак, в результате проверки мы знаем, что c и d эквивалентны (написано c ~ d), а также что c ~ b -> a.

Это можно сделать, просто сравнив два типа для g, которыемы сделали выводОбратите внимание, что это , а не противоречие типа, поскольку переменные типа достаточно общие, чтобы соответствовать их эквивалентам.Это было бы противоречием, если бы мы, например, предположили, что Int ~ Bool где-то.

Таким образом, теперь мы имеем в общей сложности следующую информацию: (небольшая работа опущена)

y :: e
h :: e -> b
x :: b -> a             -- Originally d, applied d ~ b -> a.
g :: (b -> a) -> b -> a -- Originally c -> b -> a, applied c ~ b -> a

Это было сделано путем замены наиболее определенной формы каждой переменной типа, то есть замены c и d на более конкретные b -> a.

Итак, просто проверяя, какие аргументыиди туда, мы видим, что

f :: ((b -> a) -> b -> a) -> (e -> b) -> (b -> a) -> e -> a

Это подтверждается GHC.