Вывод типа в GHCi против ручной подписи - PullRequest
4 голосов
/ 14 декабря 2011

когда я печатаю

:t map length . sum

в GHCi, он говорит, что тип будет:

map length . sum :: Num [[a]] => [[[a]]] -> [Int]

Однако, если я создаю файл type-test.hs, содержащий

x :: Num [[a]] => [[[a]]] -> [Int]
x = map length . sum

и ghc, и ghci жалуются:

type-test.hs:1:1:
    Non type-variable argument in the constraint: Num [[a]]
    (Use -XFlexibleContexts to permit this)
    In the type signature for `x': x :: Num [[a]] => [[[a]]] -> [Int]

Почему ghci позволяет мне выводить тип для этого (используя: t), когда FlexibleContexts не включены?

Ответы [ 5 ]

10 голосов
/ 14 декабря 2011

Во-первых, давайте уточним одну вещь.Что произойдет, если мы определим функцию в GHCi, а не запрашиваем тип?

> let x = map length . sum :: (Num [[a]]) => [[[a]]] -> [Int]
<interactive>:0:9:
    Non type-variable argument in the constraint: Num [[a]]
    (Use -XFlexibleContexts to permit this)
    In an expression type signature: Num [[a]] => [[[a]]] -> [Int]

И так далее.Другими словами, то же самое.Что если мы позволим GHCi определить тип определения?

> let x = map length . sum
<interactive>:0:22:
    No instance for (Num [[a0]])
      arising from a use of `sum'
    Possible fix: add an instance declaration for (Num [[a0]])
    In the second argument of `(.)', namely `sum'
    In the expression: map length . sum

Это примерно та же ошибка, которая возникает при загрузке файла, содержащего определение, без сигнатуры типа.

Каков результатвсего этого?Хорошо, подумайте о том, что сообщает , какое расширение необходимо.GHC способен распознавать, что тип означает , даже если он отклоняет тип по умолчанию.Я вряд ли ожидал, что GHC будет использовать совершенно другую программу проверки типов в зависимости от комбинации используемых расширений, поэтому, кажется, легко сделать вывод, что тип-нарушитель отклоняется ни по какой причине, кроме того, что отключено соответствующее расширение.

Команда :t в GHCi не является частью процесса компиляции - это горячая линия для системы проверки типов и логического вывода, позволяющая задать тип гипотетического кода.У него нет очевидной причины произвольно ограничивать себя на основе расширений, когда более общий тип все еще может быть информативным, по той же причине, по которой в приведенных выше сообщениях об ошибках сообщается use -XFlexibleContexts to permit this, а не просто syntax error in type constraint.


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

Например, отключение ограничения мономорфизма позволит вашему примеру выводить его тип (в соответствии с тем, что говорит :t), несмотря на то, что этот тип требует расширения для записи вручную.

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

variables Переменные типа из подписи родителя могут быть введены в область видимости с расширением ScopedTypeVariables и явным forall, если это необходимо.

7 голосов
/ 14 декабря 2011

(Это не отвечает на ваш первоначальный вопрос, но вместо этого решает проблему с кодом)

Эти ошибки намекают на то, что написанный вами код, вероятно, не тот, который вы имели в виду.Этот код:

map length . sum

означает «Возьмите мой список чисел и суммируйте его, затем вычислите длину каждого элемента (??) полученного числа».Это не имеет смысла.

Вы, вероятно, имели в виду:

sum . map length

, что означает "Возьмите мой список списков, вычислите длину каждого элемента и сложите длины."

Само сообщение об ошибке означает, что, поскольку sum возвращает число, то есть тип sum равен Num n => [n] -> n, и вы затем пытаетесь использовать map length для того, который имеет тип Num m => [[a]] -> [m],компилятор пытается сказать, что n == [[a]] чтобы типы соответствовали друг другу, и оттуда все идет вниз.

5 голосов
/ 14 декабря 2011

Другой способ взглянуть на это:

Haskell говорит вам, что ваше выражение имеет допустимый тип, а именно [[[a]]] -> [Int], если только [[a]] будет экземпляром Num.

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

1 голос
/ 14 декабря 2011

Проблема в том, что функция вполне приемлема, но ее наиболее общий тип не может быть задан грамматикой языка.Что может ghci сделать в таких обстоятельствах?Я могу думать только о двух вариантах: либо указать тип, который можно указать только с включенным расширением, либо указать ошибку.Выдавать ошибку, не упоминая, что ее можно исправить, включив расширение, мне не очень желательно.* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 2 В2 *, чтобы сообщить, что наиболее общий тип выводится проще, и, вполне возможно, когда функция была реализована, никто не думал о подобных ситуациях.

0 голосов
/ 14 декабря 2011
...