Как определить тип функций Haskell?

Ответ 1

h1 f g x y = f (g x y) x

Итак, беря список аргументов слева направо:

• f - это функция, применяемая к двум аргументам: первая - результат (g x y), а вторая - x
  • мы не знаем, какой тип первый аргумент, так что позвольте ему a
  • мы также не знаем второй тип, поэтому позвольте называть b
  • мы также не знаем тип результата (поэтому мы будем называть это c), но мы знаем, что это должен быть тип, возвращаемый h1
    • now f - это отображение функции a -> b -> c
• g - это функция, применяемая к двум аргументам: первая - x, а вторая y
  • мы знаем, что первый аргумент g совпадает с вторым аргументом f, поэтому он должен быть одного и того же типа: мы уже обозначили, что b
  • второй аргумент g - y, который еще не присвоен тип-заполнитель, так что он будет следующим следующим: d
  • g результат - это первый аргумент f, и мы уже отметили, что a
    • так что теперь g является отображением функции b -> d -> a
• Третий аргумент x, и как второй аргумент f, мы уже обозначили его тип b
• четвертый аргумент y, который является вторым аргументом g, поэтому мы уже отметили его тип d
• результат h1 является результатом применения f к (g x y) x, как мы говорили ранее, поэтому он имеет тот же тип, уже помеченный c

Хотя мы работали по списку аргументов по порядку, фактический процесс маркировки, выведения и объединения типов для каждого из этих аргументов был сделан путем просмотра тела h1.

Итак, моя первая пуля может быть разработана как:

• f - первый аргумент, который следует учитывать, поэтому рассмотрим тело h1 (все после =), чтобы увидеть, как он используется
  • f (g x y) x означает, что f применяется к (g x y) x, поэтому f должна быть функцией
  • (g x y) находится в скобках, что означает, что все, что находится внутри этих круглых скобок, оценивается, и результат этой оценки является аргументом f
  • x - просто простой аргумент f, переданный прямо из h1 списка собственных аргументов
  • поэтому f - это функция, принимающая два аргумента

Если это помогает прочитать f (g x y) x, вы можете считать эквивалентное выражение в C-like нотации f(g(x,y), x). Здесь вы можете сразу увидеть, что f и g - это функции, принимающие два аргумента, что f первый аргумент - это то, что возвращает g и т.д.

Заметим, что левая часть выражения h1 f g x y дает только один фрагмент информации о типе: h1 является функцией по четырем аргументам. Имена аргументов сами по себе являются просто заполнителями, используемыми в правой части выражения (тело h1). Относительный порядок аргументов здесь просто говорит нам, как вызвать h1, но ничего о том, как h1 использует внутренние аргументы.

Опять же, здесь эквивалент процедурного стиля (я буду использовать Python, поэтому мне не нужно заполнять какие-либо типы):

def h1(f, g, x, y):
    return f(g(x,y),x)

это означает то же самое, что и

h1 f g x y = f (g x y) x

(с одним предостережением - частичное приложение, которое, как я подозреваю, только путают дело здесь).

В обоих случаях объявление (слева от = в Haskell и до : в Python) сообщает нам только имя функции и количество аргументов.

В обоих случаях мы можем заключить из определения (правая часть в Haskell, отложенный блок после : в Python), что f и g являются обеими функциями по двум аргументам, что g first аргумент такой же, как f second и т.д. В Haskell компилятор делает это для нас; Python будет жаловаться только во время выполнения, если мы вызываем g с неправильным числом аргументов или возвращаем что-то f не может использовать в качестве первого аргумента.

Ответ 2

Если вам нечего делать, вы шаг за шагом вынимаете типы из того, как используются вещи, объединяя выведенные части. Имеем определение

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

Итак, мы видим, что h принимает четыре аргумента до сих пор совершенно неизвестных типов, назовем их a, b, c, d, а тип результата должен называться r. Таким образом, тип h должен быть унифицированным с

a -> b -> c -> d -> r

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

f (g x y) x

поэтому f применяется к двум аргументам, второй из которых является третьим аргументом h, поэтому мы знаем, что его тип c. Мы еще ничего не знаем о типе первого аргумента f. Результатом применения f является результат применения h, поэтому f тип результата r.

f :: u -> c -> r
a = u -> c -> r

Первый аргумент f с правой стороны - g x y. Таким образом, мы можем вывести

g :: c -> d -> u
b = c -> d -> u

поскольку аргументы g являются третьим и четвертым аргументами h, поэтому их типы известны, и результат является первым аргументом f.

Завершение,

f :: u -> c -> r
g :: c -> d -> u
x :: c
y :: d
h :: (u -> c -> r) -> (c -> d -> u) -> c -> d -> r

переименуйте переменные типа, как вам нравится.

Ответ 3

Если вы хотите сделать это формально, вы можете следовать правилам вывода системы типов. Если все, что у вас есть, это приложения, то будут выполняться правила просто типизированного лямбда-исчисления (см. Раздел 2.3 этих лекций по лямбда-исчислению).

Алгоритм состоит из построения дерева дедукции с использованием правил типизации системы типов, а затем вычисления окончательного типа члена путем объединения.

Ответ 4

Определение типа функции зависит от используемой системы типов. Большинство функциональных языков программирования основаны на системе типа Hindley-Milner, для которой существует тип вывода (называемый также Hindley-Milner). Для данного выражения алгоритм выводит так называемый принципиальный тип, который в основном является наиболее общим типом, который функция может иметь или терпеть неудачу, если выражение не поддается описанию. Это то, что использует GHCi при вводе :t expression.

Система типа Хиндли-Милнера допускает полиморфные функции, но все универсальные кванторы должны быть вне этого типа. (Обычно вы не видите кванторы при работе с типами, квантификаторы опущены, и они предполагаются только.) Например, const имеет тип a -> (b -> a), который может быть записан с помощью кванторов как (∀a)(∀b)(a -> (b -> a)). Однако H-M не разрешает такие типы, как (∀a)(a -> (((∀b)b) -> a))

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

Например: В H-M функция xx = \f -> f f не поддается описанию (попробуйте в GHCi). Но в системе типов, которая везде использует универсальные кванторы типов, она имеет тип. В Haskell с надлежащим расширением GHC вы можете написать:

{-# LANGUAGE RankNTypes #-}

xx :: (forall a. a -> a) -> (forall b. b -> b)
xx = \f -> f f

(Обратите внимание, что RankNTypes позволяет писать такие количественные типы, но не может дать вам тип вывода для таких функций - вам нужно указать тип самостоятельно.)

Система типа Hindley-Milner является хорошим компромиссом: она позволяет полиморфным функциям вместе с выводами типа.

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