Влияние ограничения мономорфизма на ограничения класса типов - PullRequest
Новая
       41

Влияние ограничения мономорфизма на ограничения класса типов

17 голосов
/ 25 ноября 2011

Этот код прерывается при добавлении объявления типа для baz: 

baz (x:y:_) = x == y
baz [_] = baz []
baz [] = False

Общее объяснение (см. Почему я не могу объявить предполагаемый тип? для примера) из-за полиморфной рекурсии.

Но это объяснение не объясняет, почему эффект исчезает, с другим полиморфно-рекурсивным примером: 

foo f (x:y:_) = f x y
foo f [_] = foo f []
foo f [] = False

Также не объясняется, почему GHC думаетрекурсия мономорфна без объявления типа.

Можно ли применить объяснение примера с reads в http://www.haskell.org/onlinereport/decls.html#sect4.5.5 к моему baz случаю?

Т.е. добавление подписиустраняет ограничение мономорфизма, и без ограничения появляется двусмысленность правой стороны [] с типом «по сути неоднозначным» forall a . Eq a => [a]?

Ответы [ 2 ]

13 голосов
/ 25 ноября 2011

Уравнения для baz находятся в одной группе связывания, обобщение выполняется после того, как была напечатана вся группа. Без сигнатуры типа это означает, что baz предполагается, что имеет монотип, поэтому тип [] в рекурсивном вызове задается этим (посмотрите на вывод -hddump-simp ghc). С сигнатурой типа компилятору явно говорят, что функция полиморфна, поэтому он не может предположить, что тип [] в рекурсивном вызове будет таким же, следовательно, он неоднозначен.

Как сказал Джон Л., в foo тип фиксируется появлением f - до тех пор, пока f имеет монотип. Вы можете создать ту же неоднозначность, задав f того же типа, что и (==) (для этого требуется Rank2Types), 

{-# LANGUAGE Rank2Types #-}
foo :: Eq b => (forall a. Eq a => a -> a -> Bool) -> [b] -> Bool
foo f (x:y:_) = f x y
foo f[_] = foo f []
foo _ [] = False

Это дает 

Ambiguous type variable `b0' in the constraint:
  (Eq b0) arising from a use of `foo'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: foo f []
In an equation for `foo': foo f [_] = foo f []
11 голосов
/ 25 ноября 2011

Ваш второй пример не является полиморфно рекурсивным. Это связано с тем, что функция f отображается как на LHS, так и на RHS рекурсивного определения. Также рассмотрим тип foo, (a -> a -> Bool) -> [a] -> Bool. Это исправляет тип элемента списка, идентичный типу аргументов f. В результате GHC может определить, что пустой список в RHS должен иметь тот же тип, что и список ввода.

Я не думаю, что пример reads применим к случаю baz, потому что GHC может компилировать baz без сигнатуры типа и ограничения мономорфизма. Поэтому я ожидаю, что алгоритм типа GHC имеет какой-то другой механизм, с помощью которого он устраняет неоднозначность.

...