Инструмент или метод сопоставления параметров универсального типа Haskell [дубликат]

Question

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

: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сопоставляются с конкретными типами.

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

Answer 1

Я думаю , что 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в командной строке.

Если вы ожидаете , аналогичный вывод с concerete типов , когда вы печатаете :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)

сообщает вам, что traversein traverse (:[])был "создан" с помощью f === []and a === b.