Инструмент или метод разрешения параметров универсального типа Haskell

Давайте посмотрим на типы этих функций, например:

:t traverse
traverse
  :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)

:t id
id :: a -> a

У них нет конкретных типов, но есть параметры универсального типа: a, f, b, t (поправьте меня, если они назвали не параметры универсального типа, пожалуйста)

Если я таким образом объединим id и traverse,

:t traverse id [Just 1, Just 2, Nothing] 
traverse id [Just 1, Just 2, Nothing] :: Num b => Maybe [b]

Haskell теперь может связывать некоторые конкретные типы для переменных типов a, f, b, t.

t = []
a = Maybe bb
f = Maybe
b = Num bb => bb

Ниже я вывожу типы и сопоставления с параметрами вручную, есть ли какой-либо способ или инструмент в Haskell, чтобы сделать это автоматически, чтобы он брал некоторые составные части (id и traverse) в примере, извлекал их сигнатуры типов в целом и далее вывод производит сопоставление имен параметров универсального типа с конкретными выводимыми типами?

См. также первый пример здесь: https://wiki.haskell.org/Type_inference для выражения map ord на как Haskell находит привязки реальных типов к именам.

Поэтому, когда мы рассматриваем функции по отдельности, у нас есть только имена a, f, b, t. Но затем мы объединяем функции и предоставляем некоторую дополнительную информацию, например [Just 1, Just 2, Nothing], а имена a, f, b, t сопоставляются с конкретными типами.

Я хочу поймать и показать это сопоставление автоматически.


types type-inference parametric-polymorphism haskell
person Evg    schedule 11.12.2020    source источник
comment
Я проголосовал за повторное открытие этого вопроса. Я не знаю, получите ли вы удовлетворительный ответ, но мне ясно, о чем вы просите: автоматически распечатать подстановку переменных типа, которые компилятор выводит во время проверки типов при создании экземпляра типа полиморфного определения. То есть, учитывая f :: forall x1…xn. t с переменными типа x1…xn и типом t, а также выражение, содержащее f, это напечатает все значения (типа Type), выбранные для x1…xn. Вы можете найти нужную информацию в выводе флагов GHC -ddump-tc, -ddump-tc-ast или -ddump-tc-trace.   -  person Jon Purdy    schedule 12.12.2020
comment
Если я ошибся при закрытии, поправьте меня.   -  person Will Ness    schedule 12.12.2020
comment
@JonPurdy, я по ошибке проголосовал за повторное открытие этого вопроса, не увидев, что ваш комментарий был сделан 13 часов назад, в то время как Уилл Несс закрыл этот вопрос всего несколько минут назад, так что, вероятно, вы согласны (как и я) с обманом, который отметил Уилл.   -  person Enlico    schedule 12.12.2020
comment
@WillNess, я думаю, вы не ошибаетесь, даже если я предвзят, поскольку я задал этот вопрос именно для того, чтобы обмануть это (жаль, что нет золотого значка за создание более нового вопроса, который является старым вопросом помечается как дубликат :P). Но Джон, вероятно, видит в этом вопросе другое значение, которого не вижу я.   -  person Enlico    schedule 12.12.2020
comment
@Enlico: Ваш вопрос показывает, как получить тип подвыражения; чтобы ответить на этот вопрос, вы берете этот результат и вручную объединяете его с исходным полиморфным типом, чтобы получить желаемый результат, замену вроде {f ↦ Maybe, t ↦ [], a ↦ Maybe b0, b ↦ b0}. Это хорошо работает для функций, но не очень для более сложных подтерминов. Это, безусловно, способ добиться этого, просто не совсем то, о чем, как мне кажется, просили, а именно замена.   -  person Jon Purdy    schedule 14.12.2020
comment
@JonPurdy, тогда хорошо. Я уже проголосовал за открытие.   -  person Enlico    schedule 14.12.2020

Ответы (1)


arrow_upward
0
arrow_downward

Я думаю, что f и t являются более общими параметрами конструктора типа, поскольку они воздействуют на тип, чтобы дать вам тип (они вид равен * -> *, где * означает конкретный тип).

traverse id — это не композиция, это приложение функции, так как вы передаете id в качестве аргумента в traverse. this . that — это композиция функций между this и that в математическом смысле, когда вы создаете функцию, которая передает свой (первый) аргумент в качестве входных данных для that и передает результат этого приложения в this.

Вы ссылаетесь на пример на этой странице, где дано это

map :: (a -> b) -> [a] -> [b]
Char.ord :: (Char -> Int)

компилятор может сделать вывод, что тип map ord равен [Char] -> [Int], в чем вы можете убедиться сами, написав :t map ord в командной строке.

Если вы ожидаете аналогичный вывод с конкретными типами при вводе :t traverse id, вы его не получите по той простой причине, что traverse id по-прежнему является полиморфной функцией, как в аргументах конкретного типа, так и в аргументах конструктора типа. .

Просто чтобы привести немного другой пример, если вы наберете :t traverse (:[]), где (:[]) имеет тип a -> [a], что является частным случаем (Applicative f) => a -> f b, которое ожидает traverse, вы получите этот вывод,

traverse (:[]) :: Traversable t => t b -> [t b]

что, по сравнению с :t traverse,

traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)

говорит вам, что traverse в traverse (:[]) был создан с f === [] и a === b.

person Enlico    schedule 11.12.2020
comment
Я имею в виду не композицию функций, я имею в виду, что я объединяю две вещи (функции) вместе, и это объединение определяет, как соотносить имена с фактическими типами. - person Evg; 11.12.2020
comment
@Evg, объединяющее две вещи, — это приложение-функция. Однако насчет того, что вы хотите, я так и не понял, извините (а раз вопрос закрыт, то со мной согласны как минимум еще два человека). Может быть, вы можете написать в вопросе пример вывода, который вы ожидаете от какой-то команды-подражателя или чего-то в этом роде. - person Enlico; 11.12.2020
comment
Пожалуйста, посмотрите на первый пример здесь: wiki.haskell.org/Type_inference для карты выражений или как Haskell находит привязки фактических типов к именам. Я также обновляю вопрос. - person Evg; 11.12.2020
comment
@Evg, пожалуйста, взгляните на мой обновленный ответ. Я настоятельно рекомендую вам отредактировать свой вопрос, чтобы уточнить с кодом, что вы имеете в виду. Вопрос по-прежнему закрыт, а это значит, что кто проходит мимо, не хочет открывать его снова, потому что не находит его ясным, как и я. - person Enlico; 11.12.2020
comment
@Evg, пожалуйста, также взгляните на этот вопрос я только что задал. Это, случайно, то, что вы действительно пытались здесь спросить? - person Enlico; 11.12.2020