Системные нюансы типа Хаскеля

Question

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

Используя эти определения классов и экземпляров:

class Show a => C a where
  f :: Int -> a

instance C Integer where
  f x = 1

instance C Char where
  f x = if x < 10 then 'c' else 'd'

Почему это проходитпроверка типа:

g :: C a => a -> Int -> a
g x y = f y

yes :: C a => a -> Int -> String
yes x y = show (g x y)

но это не так?

g :: C a => a -> Int -> String
g x y = show(f y)

Я считаю, что второй вариант гораздо более читабелен, и кажется, что это лишь незначительная разница (обратите внимание на сигнатуры типов)).Тем не менее, попытка обойти эту проверку типов приводит к:

*Main> :l typetests.hs
[1 of 1] Compiling Main             ( typetests.hs, interpreted )

typetests.hs:11:14:
    Ambiguous type variable `a0' in the constraints:
      (C a0) arising from a use of `f' at typetests.hs:11:14
      (Show a0) arising from a use of `show' at typetests.hs:11:9-12
    Probable fix: add a type signature that fixes these type variable(s)
    In the first argument of `show', namely `(f y)'
    In the expression: show (f y)
    In an equation for `g': g x y = show (f y)
Failed, modules loaded: none.

И я не понимаю, почему.

Примечание: Пожалуйста, не спрашивайте: «Что вы пытаетесь сделать?"Я надеюсь, что очевидно, что я просто возлюсь в абстрактном контексте, чтобы выяснить, как работает этот язык.У меня нет другой цели, кроме изучения чего-то нового.

Спасибо

Answer 1

Здесь в игру вступает забавная игрушка. Рассмотрим стандартную функцию прелюдии asTypeOf.

asTypeOf :: a -> a -> a
asTypeOf = const

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

g :: C a => a -> Int -> String
g x y = show (f y `asTypeOf` x)

Теперь GHC знает, что типа f y. Это так же, как тип первого аргумента для g. Без этой информации, вы получите сообщение об ошибке, которое вы видели. Просто не было достаточно информации, чтобы определить тип f y. А поскольку тип важен (он используется для определения того, какой экземпляр использовать для show), GHC необходимо знать, какой тип вы имеете в виду для генерации кода.

Answer 2

Это вариант пресловутой проблемы show . read.Классическая версия использует

read :: Read a => String -> a
show :: Show a => a -> String

, поэтому композиция может показаться простым старым преобразователем String

moo :: String -> String
moo = show . read

за исключением того, что в программе нет информации для определения типа в серединеследовательно, что до read, а затем show.

Ambiguous type variable `b' in the constraints:
  `Read b' arising from a use of `read' at ...
  `Show b' arising from a use of `show' at ...
Probable fix: add a type signature that fixes these type variable(s)

Пожалуйста, обратите внимание, что ghci делает кучу сумасшедших лишних настроек по умолчанию, решая неоднозначность произвольно.

> (show . read) "()"
"()"

Ваш C class является вариантом Read, за исключением того, что он декодирует Int вместо чтения String, но проблема, по сути, та же.не само по себе большое дело.Это неоднозначный вывод экземпляра , вот в чем проблема.Рассмотрим

poo :: String -> a -> a
poo _ = id

qoo :: (a -> a) -> String
qoo _ = ""

roo :: String -> String
roo = qoo . poo

При построении roo никогда не определяется, каким должен быть тип в середине, и не является roo полиморфным в этом типе.Вывод типа не решает и не обобщает переменную!Тем не менее,

> roo "magoo"
""

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

Но неизвестные экземпляры явно имеют значение.Результат полноты для вывода типа Хиндли-Милнера опирается на параметричность и, таким образом, теряется при добавлении перегрузки.Давайте не будем плакать об этом.

Answer 3

В

g :: C a => a -> Int -> a
g x y = f y

тип возврата f y фиксируется сигнатурой типа, поэтому при вызове, например, g 'a' 3, instance C Char будет использоваться.Но в

g :: C a => a -> Int -> String
g x y = show(f y)

есть два ограничения на тип возвращаемого значения f: это должен быть экземпляр C (чтобы можно было использовать f) и Show (чтобыshow можно использовать).И это все!Совпадение имен переменных типа a в определениях f и g ничего не значит.Таким образом, компилятор не может выбирать между instance C Char и instance C Integer (или любыми экземплярами, определенными в других модулях, поэтому удаление этих экземпляров не приведет к компиляции программы).