Семейство закрытых типов и тип вывода в Haskell
В GHC-7.7 (и 7.8) были введены семейства замкнутого типа:
Семейство замкнутого типа имеет все свои уравнения, определенные в одном месте и не может быть продлен, тогда как у открытого семейства могут быть случаи распространения через модули. Преимущество замкнутого семейства состоит в том, что его уравнения в порядке, аналогично определению функции уровня термина
Я хочу спросить вас, почему следующий код не компилируется? GHC должен иметь возможность выводить все типы - GetTheType определяется только для типа X, и если мы закомментируем выделенную строку, компиляция кода.
Является ли это ошибкой в GHC или семействах закрытого типа, не имеет такой оптимизации YET?
код:
{-# LANGUAGE TypeFamilies #-}
data X = X
type family GetTheType a where
GetTheType X = X
class TC a where
tc :: GetTheType a -> Int
instance TC X where
tc X = 5
main = do
-- if we comment out the following line, the code compiles
let x = tc X
print "hello"
И ошибка:
Couldn't match expected type ‛GetTheType a0’ with actual type ‛X’
The type variable ‛a0’ is ambiguous
In the first argument of ‛tc’, namely ‛X’
In the expression: tc X
Ответы
Ответ 1
Нет ничего плохого в закрытых типах семейств. Проблема в том, что функции типа не являются инъективными.
Скажем, вы могли бы иметь эту закрытую функцию типа:
data X = X
data Y = Y
type family GetTheType a where
GetTheType X = X
GetTheType Y = X
вы не можете вывести тип аргумента из типа результата X.
Семейства данных являются инъективными, но не закрытыми:
{-# LANGUAGE TypeFamilies #-}
data X = X
data family GetTheType a
data instance GetTheType X = RX
class TC a where
tc :: (GetTheType a) -> Int
instance TC X where
tc RX = 5
main = do
let x = tc RX
print "hello"
