Как GHCi выбирает имена для переменных типа?

При использовании интерактивного интерпретатора GHC можно запросить предполагаемый тип выражения:

Prelude> :t map
map :: (a -> b) -> [a] -> [b]

Кажется, что он берет имена переменных типа из подписи, поскольку map - это определено как

map :: (a -> b) -> [a] -> [b]
map _ []     = []
map f (x:xs) = f x : map f xs

в Прелюдии. В этом есть большой смысл! Мой вопрос: как выбираются имена переменных типа, если нет подписи?

Примером может быть

Prelude> :t map fst
map fst :: [(b, b1)] -> [b]

где он выбрал имена b и b1. Понятно, что переименование должно происходить, но простое начало с a, b, ... дало бы

map fst :: [(a, b)] -> [a]

вместо этого, что я считаю немного более читаемым.


type-inference haskell ghc type-variables ghci
person Martin Geisler    schedule 15.12.2011    source источник

Ответы (1)


arrow_upward
14
arrow_downward

Насколько я понимаю, ghci выбирает имена в том же порядке, что и типы. Он использует схему именования, как вы упомянули, чтобы определить имя типа результата, которым является [b], потому что это имя типа, указанное в определении map. Затем он решает, что функция, которая является первым параметром map, также должна возвращать что-то типа b.

Оставшаяся переменная типа, которую нужно назвать, является, таким образом, переменной типа для второго элемента в кортеже аргументов fst, и снова он смотрит на определение fst, чтобы решить, какое имя использовать. Определение fst :: (a, b) -> a, поэтому b было бы предпочтительным именем здесь, но поскольку b уже занят, он добавляет 1, так что он становится b1.

Я думаю, что эта система имеет преимущества в ситуациях, когда вы не имеете дело с произвольными типами, как здесь. Если результирующий тип выглядит примерно так, например:

castAdd :: (Num n, Num n1, Num n2) => n -> n1 -> n2

... это, возможно, более читабельно, чем:

castAdd :: (Num a, Num b, Num c) => a -> b -> c

... потому что вы в основном можете полагаться на то, что n# означает числовой тип, поскольку определение класса для Num - class Num n where ....

РЕДАКТИРОВАТЬ: Да, я знаю, что castAdd невозможно реализовать, но это всего лишь типовой пример.

person dflemstr    schedule 15.12.2011
comment
Спасибо, хорошее объяснение! Я не думал о случае, когда вы хотите, чтобы несколько n были переименованы, но оставались связанными. - person Martin Geisler; 15.12.2011
comment
Это не невозможно. (unSafeCoerce или просто старый добрый _|_) - person PyRulez; 02.07.2014