Нюансы системы типа Haskell

Я вникал в мельчайшие детали системы типов 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.

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

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

Спасибо


types class system haskell
person TheIronKnuckle    schedule 16.08.2011    source источник
comment
Кровавый ад! Первый пост на SO, и я получаю три отличных и проницательных ответа менее чем за 24 часа. Это удивительное место. Спасибо ребята   -  person TheIronKnuckle    schedule 17.08.2011

Ответы (3)


arrow_upward
21
arrow_downward

Здесь в дело вступает забавная игрушка. Рассмотрим стандартную функцию Prelude 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 необходимо знать, какой тип вы имеете в виду, чтобы сгенерировать код.

person Carl    schedule 16.08.2011

arrow_upward
21
arrow_downward

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

read :: Read a => String -> a
show :: Show a => a -> 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 является вариантом Read, за исключением того, что он декодирует Int вместо чтения String, но проблема, по сути, та же самая.

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

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

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

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

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

> roo "magoo"
""

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

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

person pigworker    schedule 16.08.2011

arrow_upward
16
arrow_downward

In

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 (или любыми экземплярами, определенными в других модулях, поэтому удаление этих экземпляров не приведет к компиляции программы).

person Alexey Romanov    schedule 16.08.2011