Выводящий тип лямбда-выражения - PullRequest
Новая
       61

Выводящий тип лямбда-выражения

0 голосов
/ 13 мая 2018

Дана функция a следующего типа:
a :: x -> Bool
и другая функция b следующего типа:
b :: Bool -> y
Я пытаюсь выяснить шаги, чтобы вывести тип следующей функции:
c = \d -> d a b
Может ли кто-нибудь помочь с объяснением, как это сделать, а не просто с помощью функции ghc's: type? Спасибо

Ответы [ 2 ]

0 голосов
/ 13 мая 2018

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

В этом случае x неограниченно. 

idFunction = \x -> x

Если мы хотим ограничиться определенным типом, мы можем аннотировать x напрямую.(Для этого требуется :set -XScopedTypeVariables в GHCi или {-# LANGUAGE ScopedTypeVariables #-} в файле). 

idFunction = \(x :: Int) -> x

или мы можем добавить сигнатуру типа 

idFunction :: Int -> Int
idFunction = \x -> x

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

a :: Int -> Bool
a x = x > 0

b :: Bool -> String
b y = show y

c :: ((Bool -> Bool) -> (Bool -> Bool) -> t) -> t
c = \d -> d a b

Компилятор найдет некоторые ошибки в c: 

<interactive>:10:17: error:
    • Couldn't match type ‘Bool’ with ‘Int’
      Expected type: Bool -> Bool
        Actual type: Int -> Bool
    • In the first argument of ‘d’, namely ‘a’
      In the expression: d a b
      In the expression: \ d -> d a b

<interactive>:10:19: error:
    • Couldn't match type ‘[Char]’ with ‘Bool’
      Expected type: Bool -> Bool
        Actual type: Bool -> String
    • In the second argument of ‘d’, namely ‘b’
      In the expression: d a b
      In the expression: \ d -> d a b

Теперь, если мы дадим c правильную подпись типа, тоскомпилирует 

c :: ((Int -> Bool) -> (Bool -> String) -> t) -> t
c = \d -> d a b

Как правило, нет причин избегать :t.Это очень хороший инструмент, когда вы работаете в GHCi, но когда вы создаете сложные функции в библиотеке, вам не обязательно иметь доступ к :t, поэтому альтернативой является тестирование сигнатур разных типов и просмотр реакции компилятора..

0 голосов
/ 13 мая 2018

тип c = \d -> d a b будет c :: ((x -> Bool) -> (Bool -> y) -> t) -> t

Где d - это функция, которая принимает (x -> Bool) и (Bool -> y) и возвращает значение типа t.

Итак, c - это функция, которая принимает функцию типа d и возвращает значение типа t

Если вы имеете в виду c = \d -> d (a b), тип будет c :: (Bool -> y) -> y

Некоторое дополнительное объяснение.

Чтобы узнать c, мы должны сначала узнать, что d делает, поэтому мы смотрим на c = \d -> d a b

Мы видим\d -> d a b поэтому мы знаем, что d первый аргумент - это функция a с типом (x -> Bool).Нам также известен второй аргумент d, это функция b с типом (Bool -> y).Но мы не знаем, что он возвращает, поскольку это Haskell, он должен что-то возвращать, поэтому я просто напишу t как неизвестный тип.Так что d равно d :: a -> b -> t.

Замените на тип a и b, и мы получим d :: (x -> Bool) -> (Bool -> y) -> t.

Теперь для c, c равнолямбда, которая принимает значение, которое мы можем вывести, имеет тип d и возвращает свой вывод.Таким образом, мы получаем c :: d -> (d's output).

Заменить в типе d, и мы получаем c :: ((x -> Bool) -> (Bool -> y) -> t) -> t

...