Haskell: как вывести тип выражения вручную

Ответ 1

Типы выводятся с использованием процесса, который обычно называется unification. Haskell принадлежит семье Hindley-Milner, которая является объединением алгоритм, используемый для определения типа выражения.

Если унификация терпит неудачу, выражение является ошибкой типа.

Выражение

head . filter fst

проходит. Давайте сделаем унификацию вручную, чтобы узнать, почему мы получаем что мы получаем.

Начнем с filter fst:

filter :: (a -> Bool) -> [a] -> [a]
fst :: (a' , b') -> a'                -- using a', b' to prevent confusion

filter принимает a (a -> Bool), затем a [a], чтобы дать еще один [a]. В выражении filter fst, мы переходим к filter аргументу fst, тип которого (a', b') -> a'. Чтобы это сработало, тип fst должен объединиться с типом filter первого аргумента:

(a -> Bool)  UNIFY?  ((a', b') -> a')

Алгоритм объединяет два выражения типа и пытается связать столько переменных типа (например, a или a') с фактическими типами (например, Bool).

Только тогда filter fst приведет к допустимому типизированному выражению:

filter fst :: [a] -> [a]

a' явно Bool. Таким образом, переменная типа a' разрешает a Bool. И (a', b') может объединяться в a. Так что если a (a', b') и a' есть Bool, Тогда a является просто (Bool, b').

Если мы передали несовместимый аргумент filter, например 42 (a Num), объединение Num a => a с a -> Bool потерпело бы неудачу, поскольку два выражения никогда не может объединяться в правильное выражение типа.

Возвращаясь к

filter fst :: [a] -> [a]

Это то же самое a, о котором мы говорим, поэтому мы подставляем в него место результат предыдущей унификации:

filter fst :: [(Bool, b')] -> [(Bool, b')]

Следующий бит,

head . (filter fst)

Может быть записано как

(.) head (filter fst)

Итак, возьмите (.)

(.) :: (b -> c) -> (a -> b) -> a -> c

Итак, для успеха объединения,

• head :: [a] -> a должен объединить (b -> c)
• filter fst :: [(Bool, b')] -> [(Bool, b')] должен объединить (a -> b)

Из (2) получаем, что a IS b в выражении (.) :: (b -> c) -> (a -> b) -> a -> c) `

Итак, значения переменных типа a и c в выражение (.) head (filter fst) :: a -> c легко сказать, поскольку (1) дает нам соотношение между b и c, что: b - это список c. И поскольку мы знаем, что a будет [(Bool, b')], c может объединяться только в (Bool, b')

Итак head . filter fst успешно выполняет проверку типа:

head . filter fst ::  [(Bool, b')] -> (Bool, b')

UPDATE

Интересно посмотреть, как вы можете объединить процесс с разных точек. Сначала я выбрал filter fst, затем перешел к (.) и head, но в качестве других примеров показать, объединение может быть выполнено несколькими способами, в отличие от способа математического доказательство или вывод теоремы можно сделать более чем одним способом!

Ответ 2

filter :: (a -> Bool) -> [a] -> [a] принимает функцию (a -> Bool), список того же типа a, а также возвращает список этого типа a.

В вашей defintion вы используете filter fst с fst :: (a,b) -> a, чтобы тип

filter (fst :: (Bool,b) -> Bool) :: [(Bool,b)] -> [(Bool,b)]

. Затем вы создаете свой результат [(Bool,b)] с помощью head :: [a] -> a.

(.) :: (b -> c) -> (a -> b) -> a -> c представляет собой композицию из двух функций, func2 :: (b -> c) и func1 :: (a -> b). В вашем случае у вас есть

func2 = head       ::               [ a      ]  -> a

и

func1 = filter fst :: [(Bool,b)] -> [(Bool,b)]

поэтому head здесь принимает [(Bool,b)] как аргумент и возвращает (Bool,b) за определение. В итоге у вас есть:

head . filter fst :: [(Bool,b)] -> (Bool,b)

Ответ 3

Начнем с (.). Его подпись типа

(.) :: (b -> c) -> (a -> b) -> a -> c

в котором говорится "заданная функция от b до c и функция от a до b, и a, я могу дать вам b ". Мы хотим использовать это с head и filter fst, поэтому `:

(.) :: (b -> c) -> (a -> b) -> a -> c
       ^^^^^^^^    ^^^^^^^^
         head     filter fst

Теперь head, который является функцией из массива чего-то в что-то одно. Итак, теперь мы знаем, что b будет массивом, и c будет элементом этого массива. Поэтому для целей наше выражение, мы можем думать, что (.) имеет подпись:

(.) :: ([d] -> d) -> (a -> [d]) -> a -> d -- Equation (1)
                     ^^^^^^^^^^
                     filter fst

Подписи для filter:

filter :: (e -> Bool) -> [e] -> [e] -- Equation (2)
          ^^^^^^^^^^^
              fst

(Обратите внимание, что я изменил имя переменной типа, чтобы избежать путаницы с помощью a s что у нас уже есть!) Это говорит: "Учитывая функцию от e до Bool, и список e s, я могу дать вам список e s. Функция fst имеет подпись:

fst :: (f, g) -> f

говорит: "Если у вас есть пара, содержащая f и a g, я могу дать вам f". Сравнивая это с уравнением 2, мы знаем, что e будет парой значений, первый элемент который должен быть Bool. Итак, в нашем выражении мы можем думать о filter как имеющие подпись:

filter :: ((Bool, g) -> Bool) -> [(Bool, g)] -> [(Bool, g)]

(Все, что я сделал здесь, это заменить e на (Bool, g) в уравнении 2.) И выражение filter fst имеет тип:

filter fst :: [(Bool, g)] -> [(Bool, g)]

Возвращаясь к уравнению 1, мы можем видеть, что (a -> [d]) теперь должно быть [(Bool, g)] -> [(Bool, g)], поэтому a должно быть [(Bool, g)] и d должен быть (Bool, g). Итак, в нашем выражении мы можем думать о (.) как имеющий подпись:

(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)

Подводя итог:

(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                head                         filter fst
head :: [(Bool, g)] -> (Bool, g)
filter fst :: [(Bool, g)] -> [(Bool, g)]

Объединяя все это:

head . filter fst :: [(Bool, g)] -> (Bool, g)

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

Это, наверное, все звучит очень сложно, потому что я описал это подробно. Однако такое рассуждение быстро становится второй натурой, и вы можете сделать это в своей голове.

Ответ 4

_{^{(страница вниз для ручного вывода)}} Найдите тип head . filter fst == ((.) head) (filter fst), указанный

head   :: [a] -> a
(.)    :: (b -> c) -> ((a -> b) -> (a -> c))
filter :: (a -> Bool) -> ([a] -> [a])
fst    :: (a, b) -> a

Это достигается чисто механическим способом с помощью небольшой программы Prolog:

type(head,    arrow(list(A)       , A)).                 %% -- known facts
type(compose, arrow(arrow(B, C)   , arrow(arrow(A, B), arrow(A, C)))).
type(filter,  arrow(arrow(A, bool), arrow(list(A)    , list(A)))).
type(fst,     arrow(pair(A, B)    , A)).

type([F, X], T):- type(F, arrow(A, T)), type(X, A).      %% -- application rule

который автоматически генерируется при запуске в интерпретаторе Prolog,

3 ?- type([[compose, head], [filter, fst]], T).
T = arrow(list(pair(bool, A)), pair(bool, A))       %% -- [(Bool,a)] -> (Bool,a)

где типы представлены как составные термины данных, чисто синтаксическим образом. Например. тип [a] -> a представлен arrow(list(A), A), с возможным эквивалентом Haskell Arrow (List (Logvar "a")) (Logvar "a"), с учетом соответствующих определений data.

Было использовано только одно правило вывода, приложение, а также структурная унификация Prolog, где составные термины совпадают, если они имеют одинаковую форму и их составляющие соответствуют: f (a ₁, a ₂,... a _n) и g (b ₁, b ₂,... b _m) соответствует iff f то же, что и g, n == m и _i соответствует b _i, причем логические переменные могут принимать любое значение по мере необходимости, но только один раз (не может быть изменено).

4 ?- type([compose, head], T1).     %% -- (.) head   :: (a -> [b]) -> (a -> b)
T1 = arrow(arrow(A, list(B)), arrow(A, B))

5 ?- type([filter, fst], T2).       %% -- filter fst :: [(Bool,a)] -> [(Bool,a)]
T2 = arrow(list(pair(bool, A)), list(pair(bool, A)))

Чтобы выполнить вывод типа вручную механически, необходимо записывать вещи под другим, отмечая эквивалентность на стороне и выполняя замены, таким образом имитируя действия Prolog. Мы можем рассматривать любые ->, (_,_), [] и т.д. Чисто как синтаксические маркеры, не понимая их значения вообще, и выполнять процесс механически с помощью структурного объединения, и здесь здесь только один правило вывода типа, а именно: правило применения: (a -> b) c ⊢ b {a ~ c} (замените сопоставление (a -> b) и c, с b, при эквивалентности a и c). Важно переименовывать логические переменные, чтобы избежать столкновений имен:

(.)  :: (b    -> c ) -> ((a -> b  ) -> (a -> c ))           b ~ [a1], 
head ::  [a1] -> a1                                         c ~ a1
(.) head ::              (a ->[a1]) -> (a -> c ) 
                         (a ->[c] ) -> (a -> c ) 
---------------------------------------------------------
filter :: (   a    -> Bool) -> ([a]        -> [a])          a ~ (a1,b), 
fst    ::  (a1, b) -> a1                                    Bool ~ a1
filter fst ::                   [(a1,b)]   -> [(a1,b)]  
                                [(Bool,b)] -> [(Bool,b)] 
---------------------------------------------------------
(.) head   :: (      a    -> [     c  ]) -> (a -> c)        a ~ [(Bool,b)]
filter fst ::  [(Bool,b)] -> [(Bool,b)]                     c ~ (Bool,b)
((.) head) (filter fst) ::                   a -> c      
                                    [(Bool,b)] -> (Bool,b)

Ответ 5

Вы можете сделать это "техническим" способом, с множеством сложных шагов унификации. Или вы можете сделать это "интуитивно понятным" способом, просто взглянув на это и подумав: "Хорошо, что у меня здесь? Что это такое?" и т.д.

Ну, filter ожидает функцию и список и возвращает список. filter fst указывает функцию, но нет списка, поэтому мы все еще ожидаем ввода списка. Поэтому filter fst берет список и возвращает другой список. (Это довольно распространенная фраза Хаскелла, между прочим.)

Затем оператор . "выводит" вывод на head, который ожидает список и возвращает один из элементов из этого списка. (Первый, как это бывает.) Итак, что бы filter не придумал, head дает вам первый элемент. На этом мы можем заключить, что

head . filter foobar :: [x] -> x

Но что такое x? Ну, filter fst применяет fst к каждому элементу списка (чтобы решить, следует ли его сохранить или выбросить). Поэтому fst должен быть применим к элементам списка. И fst ожидает 2-элементный кортеж и возвращает первый элемент этого кортежа. Теперь filter ожидает, что fst вернет Bool, поэтому означает, что первый элемент кортежа должен быть Bool.

Объединяя все это, заключаем

голова. filter fst:: [(Bool, y)] → (Bool, y)

Что такое y? Мы не знаем. На самом деле нас это не волнует! Вышеупомянутые функции будут работать независимо от того, что это. Так что наша подпись типа.

В более сложных примерах может быть сложнее выяснить, что происходит. (Особенно, когда задействованы странные экземпляры классов!) Но для маленьких, подобных этому, с использованием общих функций, вы обычно можете просто подумать "ОК, что здесь происходит? Что происходит там? Что ожидает эта функция?" и идти прямо до ответа без слишком большого ручного алгоритма-чеканки.